summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/process_assertions.cpp5
-rw-r--r--src/theory/arith/theory_arith.cpp6
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arith/theory_arith_private.cpp5
-rw-r--r--test/regress/CMakeLists.txt10
-rw-r--r--test/regress/regress0/arith/div.02.smt21
-rw-r--r--test/regress/regress0/nl/issue3475.smt22
-rw-r--r--test/regress/regress0/quantifiers/issue4476-ext-rew.smt22
-rw-r--r--test/regress/regress1/arith/div.06.smt21
-rw-r--r--test/regress/regress1/arith/mod.03.smt21
-rw-r--r--test/regress/regress1/nl/div-mod-partial.smt22
-rw-r--r--test/regress/regress1/quantifiers/issue3664.smt22
-rw-r--r--test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt22
-rw-r--r--test/regress/regress1/quantifiers/issue4685-wrewrite.smt22
-rw-r--r--test/regress/regress1/quantifiers/lia-witness-div-pp.smt210
-rw-r--r--test/regress/regress1/sets/issue4391-card-lasso.smt22
-rw-r--r--test/regress/regress1/sygus/issue3634.smt22
17 files changed, 40 insertions, 17 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback