Do not expand definitions of extended arithmetic operators (#5433)

This PR makes it so that extended arithmetic operators are not expanded during expand definitions. Instead they are eliminated at theory preprocessing, which occurs as the last step of preprocessing.

The motivation for this is three fold:
(1) Some quantified LIA benchmarks lead to CVC4 failing to eliminate div functions from quantifier instantiation, this leads to spurious logic failures. A regression is included, which now is correctly solved.
(2) We should allow better rewriting and preprocessing for extended arithmetic functions, especially for div/mod which is important for many users of QF_NIA.
(3) More generally,Theory::expandDefinitions will be deleted. All functionalities in expandDefinitions should move to Theory::ppRewrite.

This changes impacts many benchmarks that involve non-linear and quantifiers:

Many benchmarks (as expected) give a warning during check-models since (/ n 0) cannot be evaluated. I've added -q to disable these warnings. Fully addressing this is part of an agenda to improve our support for --check-models.
Several fuzzing benchmarks involving NL+quantifiers now time out. However, several can be solved by --sygus-inst, which is now the preferred instantiation strategy for NL+quantifiers.
2 other non-linear regressions time out, which are disabled in this PR.
one sygus-inference benchmark (regress1/sygus/issue3498.smt2), now correctly times out (previously it did not timeout since the preprocessor was unable to apply sygus-inference and resorted to normal methods, now sygus-inference can apply but as expected times out).
Fixes #5237.

13 files changed, 32 insertions, 7 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 34f5fdcba..c7810e90b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1447,7 +1447,6 @@ set(regress_1_tests
   regress1/nl/issue3617.smt2
   regress1/nl/issue3647.smt2
   regress1/nl/issue3656.smt2
-  regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
   regress1/nl/metitarski-1025.smt2
@@ -1613,11 +1612,11 @@ set(regress_1_tests
   regress1/quantifiers/issue5019-cegqi-i.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
+  regress1/quantifiers/lia-witness-div-pp.smt2
   regress1/quantifiers/lra-vts-inf.smt2
   regress1/quantifiers/mix-coeff.smt2
   regress1/quantifiers/mutualrec2.cvc
   regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
-  regress1/quantifiers/nl-pow-trick.smt2
   regress1/quantifiers/nra-interleave-inst.smt2
   regress1/quantifiers/opisavailable-12.smt2
   regress1/quantifiers/parametric-lists.smt2
@@ -1997,7 +1996,6 @@ set(regress_1_tests
   regress1/sygus/issue3247.smt2
   regress1/sygus/issue3320-quant.sy
   regress1/sygus/issue3461.sy
-  regress1/sygus/issue3498.smt2
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
   regress1/sygus/issue3633.smt2
@@ -2536,6 +2534,8 @@ set(regression_disabled_tests
   regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   # issue1048-arrays-int-real.smt2 -- different errors on debug and production.
   regress1/issue1048-arrays-int-real.smt2
+  # times out after no expand definitions for arithmetic
+  regress1/nl/issue3803-nl-check-model.smt2
   # times out after update to tangent planes
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds
@@ -2546,6 +2546,8 @@ set(regression_disabled_tests
   regress1/quantifiers/macro-subtype-param.smt2
   # times out with competition build:
   regress1/quantifiers/model_6_1_bv.smt2
+  # times out after change to arithmetic expand definitions
+  regress1/quantifiers/nl-pow-trick.smt2
   # timeout after changes to nonlinear on PR #5351
   regress1/quantifiers/rel-trigger-unusable.smt2
   # ajreynol: different error messages on production and debug:
@@ -2572,6 +2574,8 @@ set(regression_disabled_tests
   regress1/sygus/array_search_2.sy
   regress1/sygus/array_sum_2_5.sy
   regress1/sygus/crcy-si-rcons.sy
+  # previously sygus inference did not apply, now (correctly) times out
+  regress1/sygus/issue3498.smt2
   # currently slow at c9fd28a
   regress1/sygus/issue3580.sy
   regress2/arith/arith-int-098.cvc
diff --git a/test/regress/regress0/arith/div.02.smt2 b/test/regress/regress0/arith/div.02.smt2
index 328ed0cc6..37dfcbbc1 100644
--- a/test/regress/regress0/arith/div.02.smt2
+++ b/test/regress/regress0/arith/div.02.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/nl/issue3475.smt2 b/test/regress/regress0/nl/issue3475.smt2
index 128d08a18..092e8513f 100644
--- a/test/regress/regress0/nl/issue3475.smt2
+++ b/test/regress/regress0/nl/issue3475.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (declare-fun x () Real)
 (assert (< x 0))
diff --git a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
index c54254e67..8f1d8285d 100644
--- a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
+++ b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sygus-inst --no-check-models
+; EXPECT: sat
 (set-logic NRA)
 (set-info :status sat)
 (set-option :ext-rewrite-quant true)
diff --git a/test/regress/regress1/arith/div.06.smt2 b/test/regress/regress1/arith/div.06.smt2
index 6e72433ac..45d687cab 100644
--- a/test/regress/regress1/arith/div.06.smt2
+++ b/test/regress/regress1/arith/div.06.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress1/arith/mod.03.smt2 b/test/regress/regress1/arith/mod.03.smt2
index 8a6ac51d7..583c72a93 100644
--- a/test/regress/regress1/arith/mod.03.smt2
+++ b/test/regress/regress1/arith/mod.03.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress1/nl/div-mod-partial.smt2 b/test/regress/regress1/nl/div-mod-partial.smt2
index fa75ee594..c94acf770 100644
--- a/test/regress/regress1/nl/div-mod-partial.smt2
+++ b/test/regress/regress1/nl/div-mod-partial.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes -q
 ; EXPECT: sat
 (set-logic QF_UFNIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2
index 28e999604..0120f0e8a 100644
--- a/test/regress/regress1/quantifiers/issue3664.smt2
+++ b/test/regress/regress1/quantifiers/issue3664.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun-rlv --sygus-inference
+; COMMAND-LINE: --fmf-fun-rlv --sygus-inference -q
 ; EXPECT: sat
 (set-logic QF_NRA)
 (declare-fun a () Real)
diff --git a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
index 0296c978c..eaf4a3427 100644
--- a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
+++ b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models
+; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models --sygus-inst
 ; EXPECT: sat
 (set-logic NIA)
 (set-option :arith-rewrite-equalities true)
diff --git a/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2 b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
index d88faa441..fa9691578 100644
--- a/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
+++ b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sygus-inst --no-check-models
+; EXPECT: sat
 (set-logic NIRA)
 (set-info :status sat)
 (assert (forall ((a Int) (b Int)) (or (> a 0) (<= a (/ 0 (+ 0.5 b))))))
diff --git a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2
new file mode 100644
index 000000000..bd42e3596
--- /dev/null
+++ b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2
@@ -0,0 +1,10 @@
+(set-info :smt-lib-version 2.6)
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun c_main_~x~0 () Int)
+(declare-fun c_main_~y~0 () Int)
+(declare-fun c_main_~z~0 () Int)
+(assert (forall ((|main_#t~nondet0| Int) (|main_#t~nondet1| Int) (|main_#t~nondet2| Int) (v_subst_6 Int) (v_subst_5 Int) (v_subst_4 Int) (v_subst_3 Int) (v_subst_2 Int) (v_subst_1 Int)) (not (= (mod (+ (* 4194304 |main_#t~nondet0|) (* 4 c_main_~x~0) (* 4294967294 c_main_~y~0) c_main_~z~0 (* 4290772992 |main_#t~nondet1|) (* 4194304 |main_#t~nondet2|) (* 4194304 v_subst_6) (* 4290772992 v_subst_5) (* 4194304 v_subst_4) (* 4194304 v_subst_3) (* 4290772992 v_subst_2) (* 4194304 v_subst_1)) 4294967296) 1048576))))
+(assert (not (forall ((|main_#t~nondet0| Int) (|main_#t~nondet1| Int) (|main_#t~nondet2| Int)) (not (= (mod (+ (* 4194304 |main_#t~nondet0|) (* 4 c_main_~x~0) (* 4294967294 c_main_~y~0) c_main_~z~0 (* 4290772992 |main_#t~nondet1|) (* 4194304 |main_#t~nondet2|)) 4294967296) 1048576)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2
index 871d758f3..a8a0cb62d 100644
--- a/test/regress/regress1/sets/issue4391-card-lasso.smt2
+++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun d () Int)
diff --git a/test/regress/regress1/sygus/issue3634.smt2 b/test/regress/regress1/sygus/issue3634.smt2
index c7d5f9126..ad6910773 100644
--- a/test/regress/regress1/sygus/issue3634.smt2
+++ b/test/regress/regress1/sygus/issue3634.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
 (set-logic ALL)
 (declare-fun a () Int)
 (declare-fun b () Real)