From: Andrew Reynolds Date: Wed, 18 Nov 2020 15:07:08 +0000 (-0600) Subject: Do not expand definitions of extended arithmetic operators (#5433) X-Git-Tag: cvc5-1.0.0~2587 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=639540664a763a2a552d659eb594b04fb2656f5b;p=cvc5.git 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 f8af72c3a..387085de8 100644 --- 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 532aaf55c..c77e64221 100644 --- 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 0055273e4..e6029faef 100644 --- 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 ac9ec7e77..2f758e621 100644 --- 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 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)