From 52082c72d78eee219e3049285d5df559dacac8b5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 May 2020 22:39:16 -0500 Subject: Refactor operator elimination in arithmetic (#4519) This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong: (1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers. (2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental. The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way. As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR. This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts. Also notice that --rewrite-divk is effectively now enabled by default always. Fixes #4484, fixes #4486, fixes #4481. --- test/regress/regress1/arith/bug547.1.smt2 | 2 +- test/regress/regress1/bv/bv-int-collapse2-sat.smt2 | 2 -- test/regress/regress1/bv/cmu-rdk-3.smt2 | 2 -- test/regress/regress1/bv/issue3776.smt2 | 3 +-- test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 | 2 +- test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 | 2 +- test/regress/regress1/fmf/issue3626.smt2 | 2 +- test/regress/regress1/nl/issue3441.smt2 | 2 ++ test/regress/regress1/nl/issue3955-ee-double-notify.smt2 | 2 ++ test/regress/regress1/push-pop/model-unsound-ania.smt2 | 11 +++++++++++ test/regress/regress1/strings/chapman150408.smt2 | 1 - test/regress/regress1/strings/cmu-substr-rw.smt2 | 2 -- test/regress/regress1/strings/crash-1019.smt2 | 1 - 13 files changed, 20 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress1/push-pop/model-unsound-ania.smt2 (limited to 'test/regress/regress1') diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2 index 38d1dfcb1..75894eb60 100644 --- a/test/regress/regress1/arith/bug547.1.smt2 +++ b/test/regress/regress1/arith/bug547.1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --rewrite-divk --nl-ext-tplanes +; COMMAND-LINE: --nl-ext-tplanes --quiet ; EXPECT: sat (set-logic QF_NIA) (declare-fun x () Int) diff --git a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 index 3d932a076..07f2dae6a 100644 --- a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 +++ b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun t () Int) diff --git a/test/regress/regress1/bv/cmu-rdk-3.smt2 b/test/regress/regress1/bv/cmu-rdk-3.smt2 index 9e7733889..742dd593b 100644 --- a/test/regress/regress1/bv/cmu-rdk-3.smt2 +++ b/test/regress/regress1/bv/cmu-rdk-3.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2 index 30c034c70..3e86a4974 100644 --- a/test/regress/regress1/bv/issue3776.smt2 +++ b/test/regress/regress1/bv/issue3776.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: sat (set-logic QF_BVLIA) +(set-info :status sat) (declare-fun t () Int) (assert (= t (bv2nat ((_ int2bv 1) t)))) (check-sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 index 0618e28cb..dd9cb6886 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 index 07f1e6674..ea5a5e4b7 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk +; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2 index 9f27dee01..25dc80223 100644 --- a/test/regress/regress1/fmf/issue3626.smt2 +++ b/test/regress/regress1/fmf/issue3626.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound +; COMMAND-LINE: --fmf-bound --no-cegqi ; EXPECT: sat (set-logic ALL) (assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0)))) diff --git a/test/regress/regress1/nl/issue3441.smt2 b/test/regress/regress1/nl/issue3441.smt2 index 19fe98bc5..6be4e7d7e 100644 --- a/test/regress/regress1/nl/issue3441.smt2 +++ b/test/regress/regress1/nl/issue3441.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) (declare-fun a () Int) diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 index 8aa8793df..21f26df2d 100644 --- a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 +++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat (set-logic QF_UFNRA) (set-option :snorm-infer-eq true) (set-info :status sat) diff --git a/test/regress/regress1/push-pop/model-unsound-ania.smt2 b/test/regress/regress1/push-pop/model-unsound-ania.smt2 new file mode 100644 index 000000000..6f7f2752a --- /dev/null +++ b/test/regress/regress1/push-pop/model-unsound-ania.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_ANIA) +(declare-fun _substvar_16_ () Int) +(push 1) +(assert (not (= (mod _substvar_16_ 2) 0))) +(check-sat) +(pop 1) +(assert (= (- (mod _substvar_16_ 2) 2) 0)) +(check-sat) diff --git a/test/regress/regress1/strings/chapman150408.smt2 b/test/regress/regress1/strings/chapman150408.smt2 index f03718556..e6047498e 100644 --- a/test/regress/regress1/strings/chapman150408.smt2 +++ b/test/regress/regress1/strings/chapman150408.smt2 @@ -1,7 +1,6 @@ (set-logic SLIA) (set-info :status sat) (set-option :strings-exp true) -(set-option :rewrite-divk true) (declare-fun string () String) (assert (and (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0) diff --git a/test/regress/regress1/strings/cmu-substr-rw.smt2 b/test/regress/regress1/strings/cmu-substr-rw.smt2 index 20bf979dd..a4d649d7f 100644 --- a/test/regress/regress1/strings/cmu-substr-rw.smt2 +++ b/test/regress/regress1/strings/cmu-substr-rw.smt2 @@ -1,8 +1,6 @@ (set-logic ALL_SUPPORTED) (set-info :status sat) (set-option :strings-exp true) -;(set-option :produce-models true) -;(set-option :rewrite-divk true) (declare-fun uri () String) diff --git a/test/regress/regress1/strings/crash-1019.smt2 b/test/regress/regress1/strings/crash-1019.smt2 index 9f2e99b02..317840ddb 100644 --- a/test/regress/regress1/strings/crash-1019.smt2 +++ b/test/regress/regress1/strings/crash-1019.smt2 @@ -1,6 +1,5 @@ (set-logic ALL_SUPPORTED) (set-option :strings-exp true) -(set-option :rewrite-divk true) (set-info :status unsat) (declare-fun s () String) -- cgit v1.2.3