summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt4
-rw-r--r--test/regress/regress0/cvc-rerror-print.cvc2
-rw-r--r--test/regress/regress2/proofs/sat-proof-reloaded-reason.smt231
-rw-r--r--test/regress/regress2/strings/proof-fail-083021-delta.smt212
-rw-r--r--test/unit/api/solver_black.cpp41
-rw-r--r--test/unit/theory/theory_bags_rewriter_white.cpp9
6 files changed, 93 insertions, 6 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0d8ec19dc..d1208ad0f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2110,7 +2110,7 @@ set(regress_1_tests
regress1/strings/bug686dd.smt2
regress1/strings/bug768.smt2
regress1/strings/bug799-min.smt2
- regress1/strings/cee-norn-aes-trivially.smt2
+ regress1/strings/cee-norn-aes-trivially.smt2
regress1/strings/chapman150408.smt2
regress1/strings/cmu-2db2-extf-reg.smt2
regress1/strings/cmu-5042-0707-2.smt2
@@ -2509,6 +2509,7 @@ set(regress_2_tests
regress2/ooo.rf6.smt2
regress2/ooo.tag10.smt2
regress2/piVC_5581bd.smt2
+ regress2/proofs/sat-proof-reloaded-reason.smt2
regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -2539,6 +2540,7 @@ set(regress_2_tests
regress2/strings/issue6639-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
+ regress2/strings/proof-fail-083021-delta.smt2
regress2/strings/range-perf.smt2
regress2/strings/repl-repl-i-no-push.smt2
regress2/strings/repl-repl.smt2
diff --git a/test/regress/regress0/cvc-rerror-print.cvc b/test/regress/regress0/cvc-rerror-print.cvc
index e134b5666..728db28d8 100644
--- a/test/regress/regress0/cvc-rerror-print.cvc
+++ b/test/regress/regress0/cvc-rerror-print.cvc
@@ -1,5 +1,5 @@
% EXPECT: entailed
-% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response.
+% EXPECT: Cannot get model unless after a SAT or unknown response.
OPTION "logic" "ALL";
OPTION "produce-models" true;
x : INT;
diff --git a/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2 b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2
new file mode 100644
index 000000000..8bc990b8b
--- /dev/null
+++ b/test/regress/regress2/proofs/sat-proof-reloaded-reason.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-proofs
+; EXPECT: sat
+;
+; This is a benchmark exercising a dangerous behavior in SAT proofs
+; where while eliminating redundant literals new clauses are added to
+; the SAT solver and the reference to the reason of a literal could be
+; lost.
+
+(set-logic QF_SLIA)
+(declare-const x Int)
+(declare-const x2 Int)
+(declare-const x22 Int)
+(declare-const x1 Int)
+(declare-fun s () String)
+(assert (not (= "0" (str.substr s (+ 1 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1) (+ 1 1))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))) (and (> (str.len (str.substr s (+ 1 1 1) (str.len s))) 1) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1 1 1 1) (- (str.len s) 1)) 1 1))) false true)) (= 1 (str.to_int (str.substr s x22 1)))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) false true) (= 0 (str.to_int (str.substr s (+ 1 1) (+ 1 1))))))
+(assert (<= (ite (str.prefixof "-" (str.substr s 0 1)) (str.to_int (str.substr (str.substr s (+ 1 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s (+ 1 1 1) (+ 1 1 1))) 1))) (str.to_int (str.substr s 0 x2))) 0))
+(assert (ite (str.prefixof "-" (str.substr s 0 1)) (and (> (str.len (str.substr s 0 (+ 1 1))) 1) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1))))) true))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1)))) true (= 1 (str.to_int (str.substr s (+ 1 1 1 1) 1)))))
+(assert (= 1 (str.len (str.substr s (+ 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s 1 (+ 1 1 1))))))
+(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0))
+(assert (= "0" (str.substr s 1 1)))
+(assert (not (<= (str.to_int (str.substr s x x1)) 0)))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1) 1))))))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) 1)) (- (str.to_int (str.substr (str.substr s (+ 1 1 1 1) (+ 1 1)) 1 (- (str.len (str.substr s (+ 1 1) (+ 1 1))) 1)))) (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))) 1)))
+(check-sat)
diff --git a/test/regress/regress2/strings/proof-fail-083021-delta.smt2 b/test/regress/regress2/strings/proof-fail-083021-delta.smt2
new file mode 100644
index 000000000..981102b7c
--- /dev/null
+++ b/test/regress/regress2/strings/proof-fail-083021-delta.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x Bool)
+(declare-const x1 Int)
+(declare-fun s () String)
+(assert (ite (str.prefixof "-" (str.substr s 0 1)) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) true))
+(assert (not (<= (- (str.len s) 1 (+ 1 1) 1) 3)))
+(assert (ite x true (> 1 (str.len (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (= 0 (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s 1 x1)) 1)))) true))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (<= (str.to_int (str.substr s 0 (+ 1 1))) 255)))
+(check-sat)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 1daa3fba4..5ca96f035 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1571,6 +1571,47 @@ TEST_F(TestApiBlackSolver, isModelCoreSymbol)
ASSERT_THROW(d_solver.isModelCoreSymbol(zero), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, getModel)
+{
+ d_solver.setOption("produce-models", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkConst(uSort, "x");
+ Term y = d_solver.mkConst(uSort, "y");
+ Term z = d_solver.mkConst(uSort, "z");
+ Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y));
+ d_solver.assertFormula(f);
+ d_solver.checkSat();
+ std::vector<Sort> sorts;
+ sorts.push_back(uSort);
+ std::vector<Term> terms;
+ terms.push_back(x);
+ terms.push_back(y);
+ ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
+ Term null;
+ terms.push_back(null);
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, getModel2)
+{
+ d_solver.setOption("produce-models", "true");
+ std::vector<Sort> sorts;
+ std::vector<Term> terms;
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, getModel3)
+{
+ d_solver.setOption("produce-models", "true");
+ std::vector<Sort> sorts;
+ std::vector<Term> terms;
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
+ Sort integer = d_solver.getIntegerSort();
+ sorts.push_back(integer);
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
TEST_F(TestApiBlackSolver, getQuantifierElimination)
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index e63fb3b20..a05d76437 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -697,8 +697,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set)
TEST_F(TestTheoryWhiteBagsRewriter, map)
{
- Node emptybagString =
- d_nodeManager->mkConst(EmptyBag(d_nodeManager->stringType()));
+ TypeNode bagStringType =
+ d_nodeManager->mkBagType(d_nodeManager->stringType());
+ Node emptybagString = d_nodeManager->mkConst(EmptyBag(bagStringType));
Node one = d_nodeManager->mkConst(Rational(1));
Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
@@ -710,8 +711,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
// (bag.map (lambda ((x U)) t) emptybag) = emptybag
Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
- TypeNode type = d_nodeManager->mkBagType(d_nodeManager->integerType());
- Node emptybagInteger = d_nodeManager->mkConst(EmptyBag(type));
+ TypeNode bagIntType = d_nodeManager->mkBagType(d_nodeManager->integerType());
+ Node emptybagInteger = d_nodeManager->mkConst(EmptyBag(bagIntType));
ASSERT_TRUE(response1.d_node == emptybagInteger
&& response1.d_status == REWRITE_AGAIN_FULL);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback