diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 9 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-2var.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex1.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex2.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex3.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex4.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex5-dd.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-ex5.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-nemp.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/seq/seq-rewrites.smt2 | 44 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 23 | ||||
-rw-r--r-- | test/unit/api/sort_black.h | 11 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 27 |
13 files changed, 190 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 10e2f414e..5f82aedf1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,15 @@ set(regress_0_tests regress0/sep/skolem_emp.smt2 regress0/sep/trees-1.smt2 regress0/sep/wand-crash.smt2 + regress0/seq/seq-2var.smt2 + regress0/seq/seq-ex1.smt2 + regress0/seq/seq-ex2.smt2 + regress0/seq/seq-ex3.smt2 + regress0/seq/seq-ex4.smt2 + regress0/seq/seq-ex5-dd.smt2 + regress0/seq/seq-ex5.smt2 + regress0/seq/seq-nemp.smt2 + regress0/seq/seq-rewrites.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 regress0/sets/abt-te-exh2.smt2 diff --git a/test/regress/regress0/seq/seq-2var.smt2 b/test/regress/regress0/seq/seq-2var.smt2 new file mode 100644 index 000000000..3a0d8934f --- /dev/null +++ b/test/regress/regress0/seq/seq-2var.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) + +(assert (not (= x y))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex1.smt2 b/test/regress/regress0/seq/seq-ex1.smt2 new file mode 100644 index 000000000..817ee5f8e --- /dev/null +++ b/test/regress/regress0/seq/seq-ex1.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_UFSLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun f ((Seq Int)) (Seq Bool)) + +(assert (not (= x y))) +(assert (not (= (f x) (f y)))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex2.smt2 b/test/regress/regress0/seq/seq-ex2.smt2 new file mode 100644 index 000000000..89b9d3100 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex2.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) +(assert (> z 10)) +(assert (= (seq.len x) (seq.len y))) +(assert (= (seq.++ x (seq.unit z)) (seq.++ y (seq.unit 5)))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2 new file mode 100644 index 000000000..abafdeddf --- /dev/null +++ b/test/regress/regress0/seq/seq-ex3.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq (Seq Int))) +(declare-fun xp () (Seq (Seq Int))) +(declare-fun y () (Seq (Seq Int))) +(declare-fun yp () (Seq (Seq Int))) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun n () Int) +(assert (> i j)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (= (seq.extract w n 1) (seq.unit j))) +(assert (= x (seq.++ (seq.unit z) xp))) +(assert (= y (seq.++ (seq.unit w) yp))) +(assert (= x y)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2 new file mode 100644 index 000000000..93fed72c7 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex4.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (< (seq.len z) n)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2 new file mode 100644 index 000000000..d9ef5c8ba --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5-dd.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (> i 777)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5.smt2 b/test/regress/regress0/seq/seq-ex5.smt2 new file mode 100644 index 000000000..9fa72bc6b --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(assert (> i 777)) +(assert (not (= (seq.replace z (seq.unit i) w) z))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-nemp.smt2 b/test/regress/regress0/seq/seq-nemp.smt2 new file mode 100644 index 000000000..4eaee062f --- /dev/null +++ b/test/regress/regress0/seq/seq-nemp.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(assert (not (= x (as seq.empty (Seq Int))))) +(assert (= (seq.len x) 16)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-rewrites.smt2 b/test/regress/regress0/seq/seq-rewrites.smt2 new file mode 100644 index 000000000..a8bd7c1f2 --- /dev/null +++ b/test/regress/regress0/seq/seq-rewrites.smt2 @@ -0,0 +1,44 @@ +(set-logic QF_UFSLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) + +(assert +(or + +(not (= +(seq.replace (seq.++ (seq.unit 0) x) (seq.unit 1) (seq.unit 2)) +(seq.++ (seq.unit 0) (seq.replace x (seq.unit 1) (seq.unit 2))) +)) + +(not (= +(seq.at (seq.++ x (seq.unit 14)) (seq.len x)) +(seq.unit 14) +)) + +(not (= +(seq.at x z) +(seq.extract x z 1) +)) + +(not (= +(seq.contains (seq.++ x y) y) +true +)) + +(not (= +(seq.prefixof (seq.unit z) (seq.unit 4)) +(seq.suffixof (seq.unit z) (seq.unit 4)) +)) + +(not (= +(seq.rev (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +(seq.++ (seq.unit 3) (seq.unit 2) (seq.unit 1)) +)) + +)) + + + +(check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index ddff63352..4a7b74c8e 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -46,6 +46,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPredicateSort(); void testMkRecordSort(); void testMkSetSort(); + void testMkSequenceSort(); void testMkSortConstructorSort(); void testMkTupleSort(); void testMkUninterpretedSort(); @@ -56,6 +57,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkConst(); void testMkConstArray(); void testMkEmptySet(); + void testMkEmptySequence(); void testMkFalse(); void testMkFloatingPoint(); void testMkNaN(); @@ -388,6 +390,17 @@ void SolverBlack::testMkSetSort() CVC4ApiException&); } +void SolverBlack::testMkSequenceSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver->mkSequenceSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort( + d_solver->mkSequenceSort(d_solver->getIntegerSort()))); + Solver slv; + TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()), + CVC4ApiException&); +} + void SolverBlack::testMkUninterpretedSort() { TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u")); @@ -540,6 +553,16 @@ void SolverBlack::testMkEmptySet() TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } +void SolverBlack::testMkEmptySequence() +{ + Solver slv; + Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s)); + TS_ASSERT_THROWS_NOTHING( + d_solver->mkEmptySequence(d_solver->getBooleanSort())); + TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&); +} + void SolverBlack::testMkFalse() { TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 944b9309f..abaded5a1 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -35,6 +35,7 @@ class SortBlack : public CxxTest::TestSuite void testGetArrayIndexSort(); void testGetArrayElementSort(); void testGetSetElementSort(); + void testGetSequenceElementSort(); void testGetUninterpretedSortName(); void testIsUninterpretedSortParameterized(); void testGetUninterpretedSortParamSorts(); @@ -196,6 +197,16 @@ void SortBlack::testGetSetElementSort() TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); } +void SortBlack::testGetSequenceElementSort() +{ + Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); + TS_ASSERT(seqSort.isSequence()); + TS_ASSERT_THROWS_NOTHING(seqSort.getSequenceElementSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT(!bvSort.isSequence()); + TS_ASSERT_THROWS(bvSort.getSequenceElementSort(), CVC4ApiException&); +} + void SortBlack::testGetUninterpretedSortName() { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index d23f560ae..6ca02c9f1 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -44,6 +44,7 @@ class TermBlack : public CxxTest::TestSuite void testSubstitute(); void testIsConst(); void testConstArray(); + void testConstSequenceElements(); private: Solver d_solver; @@ -110,6 +111,13 @@ void TermBlack::testGetKind() TS_ASSERT_THROWS_NOTHING(p_0.getKind()); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); TS_ASSERT_THROWS_NOTHING(p_f_y.getKind()); + + // Sequence kinds do not exist internally, test that the API properly + // converts them back. + Sort seqSort = d_solver.mkSequenceSort(intSort); + Term s = d_solver.mkConst(seqSort, "s"); + Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); + TS_ASSERT(ss.getKind() == SEQ_CONCAT); } void TermBlack::testGetSort() @@ -769,3 +777,22 @@ void TermBlack::testConstArray() TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one); TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&); } + +void TermBlack::testConstSequenceElements() +{ + Sort realsort = d_solver.getRealSort(); + Sort seqsort = d_solver.mkSequenceSort(realsort); + Term s = d_solver.mkEmptySequence(seqsort); + + TS_ASSERT(s.isConst()); + + TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE); + // empty sequence has zero elements + std::vector<Term> cs = s.getConstSequenceElements(); + TS_ASSERT(cs.empty()); + + // A seq.unit app is not a constant sequence (regardless of whether it is + // applied to a constant). + Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); + TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&); +} |