summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/fp/word-blast.smt215
-rw-r--r--test/regress/regress1/minimal_unsat_core.smt212
-rw-r--r--test/regress/regress1/quantifiers/symmetric_unsat_7.smt24
-rw-r--r--test/regress/regress1/strings/stoi-400million.smt22
-rw-r--r--test/regress/regress2/strings/issue6639-replace-re-all.smt26
-rw-r--r--test/unit/api/op_black.cpp62
-rw-r--r--test/unit/node/node_black.cpp3
-rw-r--r--test/unit/theory/theory_black.cpp3
9 files changed, 106 insertions, 4 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index db6a7ae48..151e01088 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -604,6 +604,7 @@ set(regress_0_tests
regress0/fp/issue6164.smt2
regress0/fp/rti_3_5_bug.smt2
regress0/fp/simple.smt2
+ regress0/fp/word-blast.smt2
regress0/fp/wrong-model.smt2
regress0/fuzz_1.smtv1.smt2
regress0/fuzz_3.smtv1.smt2
@@ -1649,6 +1650,7 @@ set(regress_1_tests
regress1/issue5739-rtf-processed.smt2
regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
regress1/lemmas/pursuit-safety-8.smtv1.smt2
+ regress1/minimal_unsat_core.smt2
regress1/model-blocker-simple.smt2
regress1/model-blocker-values.smt2
regress1/nl/approx-sqrt.smt2
@@ -2504,6 +2506,7 @@ set(regress_2_tests
regress2/strings/issue6057-replace-re-all-simplified.smt2
regress2/strings/issue6636-replace-re-all.smt2
regress2/strings/issue6637-replace-re-all.smt2
+ regress2/strings/issue6639-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
regress2/strings/range-perf.smt2
diff --git a/test/regress/regress0/fp/word-blast.smt2 b/test/regress/regress0/fp/word-blast.smt2
new file mode 100644
index 000000000..65290a3b3
--- /dev/null
+++ b/test/regress/regress0/fp/word-blast.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fp-lazy-wb
+; EXPECT: unsat
+(set-logic QF_BVFP)
+(declare-fun meters_ackermann!0 () (_ BitVec 64))
+(assert
+ (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0)))
+ (fp.geq ?x8 ((_ to_fp 11 53) (_ bv0 64)))))
+(assert
+ (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0)))
+ (fp.leq ?x8 ((_ to_fp 11 53) (_ bv4652007308841189376 64)))))
+(assert
+ (let ((?x19 ((_ sign_extend 32) ((_ fp.to_sbv 32) roundTowardZero (fp.abs ((_ to_fp 11 53) meters_ackermann!0))))))
+(not (not (bvult (_ bv9223372036854775807 64) ?x19)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/minimal_unsat_core.smt2 b/test/regress/regress1/minimal_unsat_core.smt2
new file mode 100644
index 000000000..ef1d3ceef
--- /dev/null
+++ b/test/regress/regress1/minimal_unsat_core.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --minimal-unsat-cores
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+(assert (= n 0))
+(assert (= (div (div n n) n)
+ (div (div (div n n) n) n)))
+(assert (distinct (div (div n n) n)
+ (div (div (div (div (div n n) n) n) n) n)))
+
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 68748d4a5..7249e87aa 100644
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,8 @@
; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs
+; EXPECT: unsat
+
+; Note we require disabling proofs/unsat cores due to timeouts in nightlies
+
(set-logic AUFLIRA)
(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2
index 1b1fca2ac..42dfb1bfc 100644
--- a/test/regress/regress1/strings/stoi-400million.smt2
+++ b/test/regress/regress1/strings/stoi-400million.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-produce-proofs --no-jh-rlv-order
+; COMMAND-LINE: --strings-exp --no-jh-rlv-order
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic ALL)
diff --git a/test/regress/regress2/strings/issue6639-replace-re-all.smt2 b/test/regress/regress2/strings/issue6639-replace-re-all.smt2
new file mode 100644
index 000000000..2384f82ef
--- /dev/null
+++ b/test/regress/regress2/strings/issue6639-replace-re-all.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(assert (= a ""))
+(assert (not (str.in_re (str.replace_re_all "b" (re.comp (str.to_re a)) "a") (str.to_re "a"))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 8c4e31c22..fd45b1c22 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -92,6 +92,52 @@ TEST_F(TestApiBlackOp, getNumIndices)
ASSERT_EQ(2, regexp_loop.getNumIndices());
}
+TEST_F(TestApiBlackOp, subscriptOperator)
+{
+ Op plus = d_solver.mkOp(PLUS);
+ Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+ Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4);
+ Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4);
+ Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 4);
+ Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 4);
+ Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 4);
+ Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 4);
+ Op iand = d_solver.mkOp(IAND, 4);
+ Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 4);
+ Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 4);
+ Op floatingpoint_to_fp_ieee_bitvector =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 5);
+ Op floatingpoint_to_fp_floatingpoint =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 5);
+ Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 5);
+ Op floatingpoint_to_fp_signed_bitvector =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 5);
+ Op floatingpoint_to_fp_unsigned_bitvector =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 5);
+ Op floatingpoint_to_fp_generic =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 5);
+ Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 4, 5);
+
+ ASSERT_THROW(plus[0], CVC5ApiException);
+ ASSERT_EQ(4, divisible[0].getUInt32Value());
+ ASSERT_EQ(4, bitvector_repeat[0].getUInt32Value());
+ ASSERT_EQ(4, bitvector_zero_extend[0].getUInt32Value());
+ ASSERT_EQ(4, bitvector_sign_extend[0].getUInt32Value());
+ ASSERT_EQ(4, bitvector_rotate_left[0].getUInt32Value());
+ ASSERT_EQ(4, bitvector_rotate_right[0].getUInt32Value());
+ ASSERT_EQ(4, int_to_bitvector[0].getUInt32Value());
+ ASSERT_EQ(4, iand[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_ubv[0].getUInt32Value());
+ ASSERT_EQ(4, floatingopint_to_sbv[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_ieee_bitvector[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_floatingpoint[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_real[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_signed_bitvector[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_unsigned_bitvector[0].getUInt32Value());
+ ASSERT_EQ(4, floatingpoint_to_fp_generic[0].getUInt32Value());
+ ASSERT_EQ(4, regexp_loop[0].getUInt32Value());
+}
+
TEST_F(TestApiBlackOp, getIndicesString)
{
Op x;
@@ -207,6 +253,22 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
CVC5ApiException);
}
+TEST_F(TestApiBlackOp, getIndicesVector)
+{
+ std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
+ Op tuple_project_op = d_solver.mkOp(TUPLE_PROJECT, indices);
+
+ ASSERT_TRUE(tuple_project_op.isIndexed());
+ std::vector<Term> tuple_project_extract_indices =
+ tuple_project_op.getIndices<std::vector<Term>>();
+ ASSERT_THROW(tuple_project_op.getIndices<std::string>(), CVC5ApiException);
+ for (size_t i = 0; i < indices.size(); i++)
+ {
+ ASSERT_EQ(indices[i], tuple_project_extract_indices[i].getUInt32Value());
+ ASSERT_EQ(indices[i], tuple_project_op[i].getUInt32Value());
+ }
+}
+
TEST_F(TestApiBlackOp, opScopingToString)
{
Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 522270de4..787dd77ca 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -27,6 +27,7 @@
#include "expr/node_manager.h"
#include "expr/node_value.h"
#include "expr/skolem_manager.h"
+#include "options/options_public.h"
#include "smt/smt_engine.h"
#include "test_node.h"
#include "theory/rewriter.h"
@@ -68,7 +69,7 @@ class TestNodeBlackNode : public TestNode
argv[0] = strdup("");
argv[1] = strdup("--output-lang=ast");
std::string progName;
- Options::parseOptions(&opts, 2, argv, progName);
+ options::parse(opts, 2, argv, progName);
free(argv[0]);
free(argv[1]);
d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index 766d696a1..d8ae8e468 100644
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -53,13 +53,12 @@ TEST_F(TestTheoryBlack, array_const)
arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
ASSERT_TRUE(arr.isConst());
Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
- ASSERT_FALSE(arr2.isConst());
arr2 = Rewriter::rewrite(arr2);
ASSERT_TRUE(arr2.isConst());
arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+ arr2 = Rewriter::rewrite(arr2);
ASSERT_TRUE(arr2.isConst());
arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
- ASSERT_FALSE(arr2.isConst());
arr2 = Rewriter::rewrite(arr2);
ASSERT_TRUE(arr2.isConst());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback