Do not expand theory definitions at the beginning of preprocessing (#5544)

This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.

This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.

This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.

The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).

32 files changed, 46 insertions, 21 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 09ce71577..5298a2ca9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1689,7 +1689,6 @@ set(regress_1_tests
   regress1/quantifiers/smtlib46f14a.smt2
   regress1/quantifiers/smtlibe99bbe.smt2
   regress1/quantifiers/smtlibf957ea.smt2
-  regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   regress1/quantifiers/sygus-infer-nested.smt2
   regress1/quantifiers/symmetric_unsat_7.smt2
   regress1/quantifiers/var-eq-trigger.smt2
@@ -2159,7 +2158,6 @@ set(regress_2_tests
   regress2/bv_to_int_5095_2.smt2
   regress2/bv_to_int_ashr.smt2
   regress2/bv_to_int_bitwise.smt2
-  regress2/bv_to_int_bvmul1.smt2
   regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
@@ -2586,6 +2584,8 @@ set(regression_disabled_tests
   regress1/quantifiers/nl-pow-trick.smt2
   # timeout after changes to nonlinear on PR #5351
   regress1/quantifiers/rel-trigger-unusable.smt2
+  # changes to expand definitions, related to trigger selection for selectors
+  regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/subtype-param-unk.smt2
   regress1/quantifiers/subtype-param.smt2
@@ -2620,6 +2620,8 @@ set(regression_disabled_tests
   # timeout on debug
   regress2/arith/real2int-test.smt2
   regress2/bug396.smt2
+  # due to bv2int not handling unsigned/signed division
+  regress2/bv_to_int_bvmul1.smt2
   regress2/nl/dumortier-050317.smt2
   regress2/nl/nt-lemmas-bad.smt2
   regress2/quantifiers/ForElimination-scala-9.smt2
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 76bc4095f..c7771d5c9 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_LIA)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2
index 290850d1a..c871226ce 100644
--- a/test/regress/regress0/arith/issue3413.smt2
+++ b/test/regress/regress0/arith/issue3413.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_NIA)
 (declare-fun a () Int)
 (declare-fun e () Int)
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
index 3b84b7aff..e4bac6a0a 100644
--- a/test/regress/regress0/bug484.smt2
+++ b/test/regress/regress0/bug484.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 
 ; Preamble  --------------
diff --git a/test/regress/regress0/datatypes/issue2838.cvc b/test/regress/regress0/datatypes/issue2838.cvc
index 95e1c898a..9fab5f423 100644
--- a/test/regress/regress0/datatypes/issue2838.cvc
+++ b/test/regress/regress0/datatypes/issue2838.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 Ints_0 : ARRAY INT OF INT;
 C : TYPE = [# i : INT #];
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
index e4e1f65b4..5d0d8f6e6 100644
--- a/test/regress/regress0/fmf/fmc_unsound_model.smt2
+++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 ; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
index d951e6c50..890e765aa 100644
--- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2
index 794eefb37..0249462ee 100644
--- a/test/regress/regress1/arith/issue4985-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985-model-success.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
 (declare-const arr0 (Array Real Real))
diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2
index eae8d369d..22b55c87f 100644
--- a/test/regress/regress1/arith/issue4985b-model-success.smt2
+++ b/test/regress/regress1/arith/issue4985b-model-success.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_AUFNRA)
 (set-info :status sat)
 (declare-const a (Array Real Real))
diff --git a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
index f1d20befc..33c1796f9 100644
--- a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
+++ b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2
index c4a40ccc1..4bf21d533 100644
--- a/test/regress/regress1/fmf/german169.smt2
+++ b/test/regress/regress1/fmf/german169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2
index 25dc80223..6162b4cfe 100644
--- a/test/regress/regress1/fmf/issue3626.smt2
+++ b/test/regress/regress1/fmf/issue3626.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound --no-cegqi
+; COMMAND-LINE: --fmf-bound --no-cegqi -q
 ; EXPECT: sat
 (set-logic ALL)
 (assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
index 7f3a5b28f..8c72672cd 100644
--- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
+++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2
index 378380779..d32c1730e 100644
--- a/test/regress/regress1/fmf/loopy_coda.smt2
+++ b/test/regress/regress1/fmf/loopy_coda.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
index b2c42d7c5..3d30ae058 100644
--- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
index 5d1289997..7577e3966 100644
--- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
+++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 OPTION "produce-models";
 OPTION "fmf-bound";
diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2
index 25851f6e0..73de1a36f 100644
--- a/test/regress/regress1/fmf/nun-0208-to.smt2
+++ b/test/regress/regress1/fmf/nun-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort b__ 0)
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
index 841d050a7..25662d6eb 100644
--- a/test/regress/regress1/ho/issue4065-no-rep.smt2
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic AUFBV)
 (set-info :status sat)
 (set-option :bv-div-zero-const false)
diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
index 500ef6d4c..8846fe7fa 100644
--- a/test/regress/regress1/quantifiers/issue5470-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic NIA)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
index 9e8cd6586..d45d72253 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
index e9883297e..c7ef2d053 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
index 2c42744ac..17028065c 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
index f24aa6b1b..95608c150 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
index dbb653351..151499d78 100644
--- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2
index 01b633d8e..f985961df 100644
--- a/test/regress/regress1/sets/is_singleton1.smt2
+++ b/test/regress/regress1/sets/is_singleton1.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun S () (Set Int))
@@ -6,4 +8,4 @@
 (assert (= (singleton x) S))
 (assert (is_singleton S))
 (assert (is_singleton (singleton 3)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2
index ba8180b5e..75ac15817 100644
--- a/test/regress/regress1/sets/issue5271.smt2
+++ b/test/regress/regress1/sets/issue5271.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun s () (Set Int))
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc
index 4cac9a24e..194129518 100644
--- a/test/regress/regress1/sets/sets-tuple-poly.cvc
+++ b/test/regress/regress1/sets/sets-tuple-poly.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 OPTION "sets-ext";
 OPTION "logic" "ALL_SUPPORTED";
diff --git a/test/regress/regress1/sets/univ-set-uf-elim.smt2 b/test/regress/regress1/sets/univ-set-uf-elim.smt2
index a22f2a44f..f02788a72 100644
--- a/test/regress/regress1/sets/univ-set-uf-elim.smt2
+++ b/test/regress/regress1/sets/univ-set-uf-elim.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --produce-models
 ; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
 ; EXIT: 1
 (set-logic ALL)
diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
index 78035790b..fd2060942 100644
--- a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
+++ b/test/regress/regress1/sygus/issue3944-div-rewrite.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 () Int)
diff --git a/test/regress/regress1/trim.cvc b/test/regress/regress1/trim.cvc
index 8bdbde79a..019b7702f 100644
--- a/test/regress/regress1/trim.cvc
+++ b/test/regress/regress1/trim.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find -q
 % EXPECT: sat
 DATATYPE
 	myType = A | B
diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2
index 54dfa0946..234e82229 100644
--- a/test/regress/regress2/bv_to_int_5095_2.smt2
+++ b/test/regress/regress2/bv_to_int_5095_2.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
-; COMMAND --solve-bv-as-int=sum
+; COMMAND-LINE: --solve-bv-as-int=sum -q
 (set-logic BV)
 (declare-const bv_42-0 (_ BitVec 42))
 (assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 938aa01ea..b688d3fcf 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)
 (set-option :finite-model-find true)