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.

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index f8af72c3a075c05cde4798161ff229e91983a5f4..387085de89b31aa26d97f73fc456012f48b3ac51 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -411,6 +411,11 @@ bool ProcessAssertions::apply(Assertions& as)
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
   d_passes["theory-preprocess"]->apply(&assertions);
+  // Must remove ITEs again since theory preprocessing may introduce them.
+  // Notice that we alternatively could ensure that the theory-preprocess
+  // pass above calls TheoryPreprocess::preprocess instead of
+  // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal.
+  d_passes["ite-removal"]->apply(&assertions);
 
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 532aaf55c328c539cbbe53deb70c64b6bc7a75c3..c77e64221b54aa85e4ac58b9cf00f1d032fb7da9 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -97,12 +97,6 @@ void TheoryArith::preRegisterTerm(TNode n)
   d_internal->preRegisterTerm(n);
 }
 
-TrustNode TheoryArith::expandDefinition(Node node)
-{
-  // call eliminate operators
-  return d_arithPreproc.eliminate(node);
-}
-
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 
 TrustNode TheoryArith::ppRewrite(TNode atom)

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0055273e421b491d8121dda0cb33b3836c92a158..e6029faef82c61d00033304295773b37a9e9cf7c 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -74,8 +74,6 @@ class TheoryArith : public Theory {
    */
   void preRegisterTerm(TNode n) override;
 
-  TrustNode expandDefinition(Node node) override;
-
   //--------------------------------- standard check
   /** Pre-check, called before the fact queue of the theory is processed. */
   bool preCheck(Effort level) override;

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ac9ec7e77a36a107590382c988fcef2cef00cb37..2f758e62160f0dd5df13ea0d747549df358b44a0 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1473,8 +1473,9 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){
   Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal);
   if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
     stringstream ss;
-    ss << "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: " << x << endl
-       << "if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.";
+    ss << "A non-linear fact (involving div/mod/divisibility) was asserted to "
+          "arithmetic in a linear logic: "
+       << x << std::endl;
     throw LogicException(ss.str());
   }
   Assert(!d_partialModel.hasArithVar(x));

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 34f5fdcba6da3455e64b6ea6fb9f0b41e2c8846c..c7810e90b9c386798d1f3dd473210a739eb6089d 100644 (file)
--- 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 328ed0cc6b93588bc5bf2a7ef3009ac30a166054..37dfcbbc14bc48f53fd17584d163a5dc8851bbd5 100644 (file)
--- 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 128d08a18910c34843b924cd9e37f6e85441a1a7..092e8513f107437405652697c37da2c78c8c41e8 100644 (file)
--- 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 c54254e676e4bff5b1693074139e904bc3b27e9b..8f1d8285d9947eb6a300e85498dd4cc3af0d67b6 100644 (file)
--- 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 6e72433ac30adaa842590e7685d5c7d223b6606c..45d687cab0a391bbdcf55f08c692336bde2a539a 100644 (file)
--- 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 8a6ac51d7a74373f4650c30236a01f293ed487e7..583c72a93553290ca162522000e6af78014435ea 100644 (file)
--- 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 fa75ee59419c276253be68404f029a59673e1199..c94acf77069054aea4713e65b4bb7fdb9ee5587a 100644 (file)
--- 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 28e9996045d7f49eb3c965aba03bac6e678943a8..0120f0e8a4cbbd8ae6f8d541ecf04621e0568eb9 100644 (file)
--- 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 0296c978cd68f96f83853c1dd3691d924d6debb2..eaf4a3427815327be05ef2daa9c5cf020143dca0 100644 (file)
--- 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 d88faa441c47cf447ba8e8220a98e5c656659f24..fa9691578d047157fd4e86cca343715808b72c91 100644 (file)
--- 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 (file)
index 0000000..bd42e35
--- /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 871d758f370029240a011a83fc6ae9dd8e366182..a8a0cb62d7535902fa121e493c91fa3e55a2855f 100644 (file)
--- 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 c7d5f9126d2716f17f98c47ec93a9ce0e5c7b492..ad691077356bf2509aa2c33ddc74e5b111aea27e 100644 (file)
--- 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)