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.

24 files changed, 55 insertions, 24 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2df07db5a..5a59f2f54 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1121,6 +1121,9 @@ set(regress_0_tests
   regress0/uflra/simple.02.cvc
   regress0/uflra/simple.03.cvc
   regress0/uflra/simple.04.cvc
+  regress0/unconstrained/4481.smt2
+  regress0/unconstrained/4484.smt2
+  regress0/unconstrained/4486.smt2
   regress0/unconstrained/arith.smt2
   regress0/unconstrained/arith3.smt2
   regress0/unconstrained/arith4.smt2
@@ -1472,6 +1475,7 @@ set(regress_1_tests
   regress1/push-pop/fuzz_7.smt2
   regress1/push-pop/fuzz_8.smt2
   regress1/push-pop/fuzz_9.smt2
+  regress1/push-pop/model-unsound-ania.smt2
   regress1/push-pop/quant-fun-proc-unmacro.smt2
   regress1/push-pop/quant-fun-proc.smt2
   regress1/quantifiers/006-cbqi-ite.smt2
diff --git a/test/regress/regress0/arith/bug547.2.smt2 b/test/regress/regress0/arith/bug547.2.smt2
index b7d114eb3..7ff2a538a 100644
--- a/test/regress/regress0/arith/bug547.2.smt2
+++ b/test/regress/regress0/arith/bug547.2.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
 (set-logic QF_NIA)
+(set-info :status sat)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun z () Int)
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 9ddc80e98..76bc4095f 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
 (set-logic QF_LIA)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
index 7294cd863..1a9c50590 100644
--- a/test/regress/regress0/arith/mod-simp.smt2
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: unsat
 (set-logic QF_LIA)
 (set-info :status unsat)
 
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
index 75d82d98f..581c34f2d 100644
--- a/test/regress/regress0/bug548a.smt2
+++ b/test/regress/regress0/bug548a.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --rewrite-divk --tlimit 1000
+; COMMAND-LINE: --tlimit 1000
 ; EXPECT: unknown
 (set-logic AUFLIA)
 (declare-fun f (Int) Int)
diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2
index c6ac3b56f..fbf996a0a 100644
--- a/test/regress/regress0/quantifiers/mix-match.smt2
+++ b/test/regress/regress0/quantifiers/mix-match.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-fun P (Real) Bool)
@@ -7,4 +9,4 @@
 (assert (is_int a))
 (assert (not (P a)))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2
new file mode 100644
index 000000000..028607093
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4481.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Int)
+(assert (= (div a 2) 2))
+(assert (= (div a 3) 0))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2
new file mode 100644
index 000000000..f2f11295b
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4484.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: unsat
+(set-logic QF_NIRA)
+(set-info :status unsat)
+(declare-fun a () Real)
+(assert (= (to_int a) 2))
+(assert (= (to_int (/ a 2.0)) 2))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2
new file mode 100644
index 000000000..01771ce66
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4486.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (is_int x))
+(assert (is_int (+ x 1)))
+(check-sat)
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)
diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2
index 31eaa5aba..cce0c963a 100644
--- a/test/regress/regress2/bug674.smt2
+++ b/test/regress/regress2/bug674.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
+; COMMAND-LINE: --quant-ind --incremental
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 (define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2))))
diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
index e2ae94a27..4782fa7f8 100644
--- a/test/regress/regress2/strings/cmi-split-cm-fail.smt2
+++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --rewrite-divk
+; COMMAND-LINE: --strings-exp
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)