`itauto lia` runs forever on goal with many `const1 <= Y < const2`

This terminates with bb985b0c but this is still awfully slow. There does not seem to be a quick shortcut. More work is needed... This will be a good test-case!

closed with commit 9abb0bb2

I should have explained more why I closed the bug. For this goal, itauto makes a number of calls to lia. The cumulative time is 34s and the itauto total running time is 42s. So, 80% of the time is spent in lia and several lia calls are very slow.

This is hard to explain as lia alone is very fast for the whole goal. This shows that the running time of lia may be very unpredictable.

My assessment is that itauto is not the main culprit; lia is the bootleneck.

Until now, lia has always been fast for me, except in cases where there are many hypotheses containing disjunctions and implications. So I didn't believe the explanation about lia being the bottleneck and made the following experiment:

Require Import Lia ZArith List.
Require Import Cdcl.Itauto.
Open Scope Z_scope.

Unset Lia Cache.

Ltac logging_lia :=
  try (repeat match goal with
              | x: _ |- _ => revert x
              end;
       match goal with
       | |- ?G => idtac "--- lia goal ---"; idtac G
       end;
       fail);
  time lia.

Goal forall Y r0 r q q0 r1 q1 : Z,
  131072 <= r0 < 139264 \/
  268468224 <= r0 < 268500992 \/
  268509184 <= r0 < 268513280 \/
  268513280 <= r0 < 268517376 \/ 268582912 <= r0 < 268587008 ->
  ~
  (131072 <= Y < 139264 \/
   268468224 <= Y < 268500992 \/
   268509184 <= Y < 268513280 \/
   268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008) ->
  r = 0 ->
  0 <= Y < 4294967296 ->
  (4 <> 0 -> r0 = 4 * q + r) ->
  (4294967296 = 0 -> q0 = 0 /\ r0 = 0 /\ q1 = 0 /\ r1 = 0) ->
  (4 < 0 -> 4 < r <= 0 /\ 4294967296 < r0 <= 0 /\ 4294967296 < r1 <= 0) ->
  (0 < 4 -> 0 <= r < 4 /\ 0 <= r0 < 4294967296 /\ 0 <= r1 < 4294967296) ->
  (4294967296 <> 0 -> Y - r1 = 4294967296 * q0 + r0 /\ 3 = 4294967296 * q1 + r1) ->
  (4 = 0 -> q = 0 /\ r = 0) -> False.
Proof.
  intros.
  (* Time logging_lia. (* 0.118 secs *) *)
  Time itauto logging_lia. (* 41.91 secs, making 23 successful and 90 failed calls to lia, 
  where four lia calls (all successful) take more than 1 sec:
  19.225 secs, 9.241 secs, 2.187 secs, 1.314 secs *)

And indeed, to my surprise, lia is the bottleneck. I reported the slowest goal on the Coq issue tracker.

Here are more similar goals from the same file (the first is the same as above).

Each of these four goals is solved immediately by lia, but the first three take a very long time (up to half an hour) with itauto timing_lia, and it seems that all the time is spent in lia. If I filter out all timings that take >= 1 sec, I get

Tactic call lia ran for 2.293 secs (2.281u,0.001s) (success)
Tactic call lia ran for 1.361 secs (1.353u,0.s) (success)
Tactic call lia ran for 19.612 secs (19.494u,0.004s) (success)
Tactic call lia ran for 9.873 secs (9.81u,0.s) (success)
Tactic call itauto timing_lia ran for 43.19 secs (42.856u,0.051s) (success)

Tactic call lia ran for 420.809 secs (418.754u,0.022s) (success)
Tactic call itauto timing_lia ran for 432.577 secs (430.425u,0.027s) (success)

Tactic call lia ran for 1970.801 secs (1962.618u,0.006s) (success)
Tactic call itauto timing_lia ran for 1987.788 secs (1979.465u,0.018s) (success)

Tactic call itauto timing_lia ran for 0.02 secs (0.02u,0.s) (success)

And here are the goals:

Require Import Lia ZArith.
Require Import Cdcl.Itauto.
Open Scope Z_scope.

Unset Lia Cache.

Ltac timing_lia := time "lia" lia.

Goal forall Y r0 : Z,
 131072 <= r0 < 139264 \/
 268468224 <= r0 < 268500992 \/
 268509184 <= r0 < 268513280 \/
 268513280 <= r0 < 268517376 \/ 268582912 <= r0 < 268587008 ->
 ~
 (131072 <= Y < 139264 \/
  268468224 <= Y < 268500992 \/
  268509184 <= Y < 268513280 \/
  268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008) ->
 forall r : Z,
 r = 0 ->
 0 <= Y < 4294967296 ->
 forall q : Z,
 (4 <> 0 -> r0 = 4 * q + r) ->
 forall q0 r1 q1 : Z,
 (4294967296 = 0 -> q0 = 0 /\ r0 = 0 /\ q1 = 0 /\ r1 = 0) ->
 (4 < 0 -> 4 < r <= 0 /\ 4294967296 < r0 <= 0 /\ 4294967296 < r1 <= 0) ->
 (0 < 4 -> 0 <= r < 4 /\ 0 <= r0 < 4294967296 /\ 0 <= r1 < 4294967296) ->
 (4294967296 <> 0 ->
  Y - r1 = 4294967296 * q0 + r0 /\ 3 = 4294967296 * q1 + r1) ->
 (4 = 0 -> q = 0 /\ r = 0) -> False .
Proof.
  intros.
  time "itauto timing_lia" itauto timing_lia.
Qed.

Goal forall Y r0 : Z,
 131072 <= r0 < 139264 \/
 268468224 <= r0 < 268500992 \/
 268509184 <= r0 < 268513280 \/
 268513280 <= r0 < 268517376 \/ 268582912 <= r0 < 268587008 ->
 ~
 (131072 <= Y < 139264 \/
  268468224 <= Y < 268500992 \/
  268509184 <= Y < 268513280 \/
  268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008) ->
 forall r : Z,
 r = 0 ->
 0 <= Y < 4294967296 ->
 forall q : Z,
 (4 <> 0 -> r0 = 4 * q + r) ->
 forall q0 r1 q1 : Z,
 (4294967296 = 0 -> q0 = 0 /\ r0 = 0 /\ q1 = 0 /\ r1 = 0) ->
 (4 < 0 -> 4 < r <= 0 /\ 4294967296 < r0 <= 0 /\ 4294967296 < r1 <= 0) ->
 (0 < 4 -> 0 <= r < 4 /\ 0 <= r0 < 4294967296 /\ 0 <= r1 < 4294967296) ->
 (4294967296 <> 0 ->
  Y - r1 = 4294967296 * q0 + r0 /\ 2 = 4294967296 * q1 + r1) ->
 (4 = 0 -> q = 0 /\ r = 0) -> False.
Proof.
  intros.
  time "itauto timing_lia" itauto timing_lia.
Qed.

Goal forall Y r0 : Z,
 131072 <= r0 < 139264 \/
 268468224 <= r0 < 268500992 \/
 268509184 <= r0 < 268513280 \/
 268513280 <= r0 < 268517376 \/ 268582912 <= r0 < 268587008 ->
 ~
 (131072 <= Y < 139264 \/
  268468224 <= Y < 268500992 \/
  268509184 <= Y < 268513280 \/
  268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008) ->
 forall r : Z,
 r = 0 ->
 0 <= Y < 4294967296 ->
 forall q : Z,
 (4 <> 0 -> r0 = 4 * q + r) ->
 forall q0 r1 q1 : Z,
 (4294967296 = 0 -> q0 = 0 /\ r0 = 0 /\ q1 = 0 /\ r1 = 0) ->
 (4 < 0 -> 4 < r <= 0 /\ 4294967296 < r0 <= 0 /\ 4294967296 < r1 <= 0) ->
 (0 < 4 -> 0 <= r < 4 /\ 0 <= r0 < 4294967296 /\ 0 <= r1 < 4294967296) ->
 (4294967296 <> 0 ->
  Y - r1 = 4294967296 * q0 + r0 /\ 1 = 4294967296 * q1 + r1) ->
 (4 = 0 -> q = 0 /\ r = 0) -> False.
Proof.
  intros.
  time "itauto timing_lia" itauto timing_lia.
Qed.

Goal forall Y : Z,
 131072 <= Y < 139264 \/
 268468224 <= Y < 268500992 \/
 268509184 <= Y < 268513280 \/
 268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008 ->
 ~
 (131072 <= Y < 139264 \/
  268468224 <= Y < 268500992 \/
  268509184 <= Y < 268513280 \/
  268513280 <= Y < 268517376 \/ 268582912 <= Y < 268587008) ->
 forall r : Z,
 r = 0 ->
 0 <= Y < 4294967296 ->
 forall q : Z,
 (4 <> 0 -> Y = 4 * q + r) ->
 (0 < 4 -> 0 <= r < 4) ->
 (4 < 0 -> 4 < r <= 0) -> (4 = 0 -> q = 0 /\ r = 0) -> False.
Proof.
  intros.
  time "itauto timing_lia" itauto timing_lia.
Qed.

mentioned in issue #14 (closed)

mentioned in issue #4

The additional examples I posted above are currently the slowest itauto lia calls of the whole bedrock2 build (but excluding the experiments on more automated program logic proofs scripts that I hope itauto will enable). However, all the time is spent in lia, as the output of Set Itauto Theory Time. shows:

Debug: Theory running time 12.263
Tactic call Assert conflicts ran for 0.006 secs (0.005u,0.s) (success)
Finished transaction in 12.885 secs (12.829u,0.01s) (successful)
Debug: Theory running time 12.449
Tactic call Assert conflicts ran for 0.005 secs (0.005u,0.s) (success)
Finished transaction in 13.097 secs (13.026u,0.007s) (successful)
Debug: Theory running time 11.932
Tactic call Assert conflicts ran for 0.005 secs (0.004u,0.s) (success)
Finished transaction in 12.547 secs (12.49u,0.011s) (successful)
Debug: Theory running time 0.
Tactic call Assert conflicts ran for 0. secs (0.u,0.s) (success)
Finished transaction in 0.022 secs (0.022u,0.s) (successful)

So it's not an itauto issue any more, but I just wanted to note that this thread contains interesting examples to test lia.

The latest commit https://github.com/coq/coq/pull/13228/commits/c78abffccde36fca356586f381125bb587e91c69 seems to work. Both lia and itauto are fast.

`itauto lia` runs forever on goal with many `const1 <= Y < const2`

Designs

Child items ...

Activity

Admin message

`itauto lia` runs forever on goal with many `const1 <= Y < const2`

Activity