summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt5
-rw-r--r--test/regress/regress0/bv/ackermann1.smt22
-rw-r--r--test/regress/regress0/bv/ackermann2.smt22
-rw-r--r--test/regress/regress0/bv/bool-to-bv-all.smt2 (renamed from test/regress/regress0/bv/bool-to-bv.smt2)2
-rw-r--r--test/regress/regress0/bv/bool-to-bv-ite.smt213
-rw-r--r--test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt2
-rw-r--r--test/regress/regress0/fmf/QEpres-uf.855035.smt2
-rw-r--r--test/regress/regress0/sets/sets-extr.smt215
-rw-r--r--test/regress/regress1/bv/bug787.smt22
-rw-r--r--test/regress/regress1/fmf/nlp042+1.smt22
-rw-r--r--test/regress/regress2/strings/extf_d_perf.smt219
-rw-r--r--test/unit/api/CMakeLists.txt1
-rw-r--r--test/unit/api/opterm_black.h57
-rw-r--r--test/unit/api/solver_black.h117
14 files changed, 233 insertions, 8 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e0e57acf9..95e4b8875 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -159,7 +159,8 @@ set(regress_0_tests
regress0/bv/ackermann2.smt2
regress0/bv/ackermann3.smt2
regress0/bv/ackermann4.smt2
- regress0/bv/bool-to-bv.smt2
+ regress0/bv/bool-to-bv-all.smt2
+ regress0/bv/bool-to-bv-ite.smt2
regress0/bv/bug260a.smt
regress0/bv/bug260b.smt
regress0/bv/bug440.smt
@@ -775,6 +776,7 @@ set(regress_0_tests
regress0/sets/pre-proc-univ.smt2
regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
regress0/sets/sets-equal.smt2
+ regress0/sets/sets-extr.smt2
regress0/sets/sets-inter.smt2
regress0/sets/sets-of-sets-subtypes.smt2
regress0/sets/sets-poly-int-real.smt2
@@ -1729,6 +1731,7 @@ set(regress_2_tests
regress2/strings/cmu-disagree-0707-dd.smt2
regress2/strings/cmu-prereg-fmf.smt2
regress2/strings/cmu-repl-len-nterm.smt2
+ regress2/strings/extf_d_perf.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
regress2/strings/norn-dis-0707-3.smt2
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index 9b96b38c4..218fd746b 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
; EXPECT: sat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index eeca505fe..b1aaa7d64 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv-all.smt2
index 8706c51a8..5947699d9 100644
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ b/test/regress/regress0/bv/bool-to-bv-all.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bool-to-bv
+; COMMAND-LINE: --bool-to-bv=all
; EXPECT: sat
(set-logic QF_BV)
(declare-fun x2 () (_ BitVec 3))
diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2
new file mode 100644
index 000000000..e1be3ea10
--- /dev/null
+++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --bool-to-bv=ite
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(assert (=> b1 b2))
+(assert (= x2 (ite (bvugt x0 x1) (bvadd x0 (_ bv1 3)) (bvadd x1 (_ bv1 3)))))
+(check-sat)
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
index e8c7949dc..bb2630b93 100644
--- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
+++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
(benchmark Isabelle
:status sat
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt
index 4fe592638..97a585090 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smt
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(benchmark Isabelle
:status sat
diff --git a/test/regress/regress0/sets/sets-extr.smt2 b/test/regress/regress0/sets/sets-extr.smt2
new file mode 100644
index 000000000..c497ff189
--- /dev/null
+++ b/test/regress/regress0/sets/sets-extr.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun a () Atom)
+(declare-fun b () Atom)
+(declare-fun c () Atom)
+(declare-fun S () (Set Atom))
+
+
+(assert (= S (union (singleton a) (union (singleton c) (singleton b)))))
+
+(check-sat)
+
diff --git a/test/regress/regress1/bv/bug787.smt2 b/test/regress/regress1/bv/bug787.smt2
index 8e0ba0016..d732b9ff0 100644
--- a/test/regress/regress1/bv/bug787.smt2
+++ b/test/regress/regress1/bv/bug787.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-proofs
+; COMMAND-LINE: --bitblast=eager
; EXPECT: unsat
(set-logic QF_BV)
(set-info :status unsat)
diff --git a/test/regress/regress1/fmf/nlp042+1.smt2 b/test/regress/regress1/fmf/nlp042+1.smt2
index 567a3c0b7..6159f0b41 100644
--- a/test/regress/regress1/fmf/nlp042+1.smt2
+++ b/test/regress/regress1/fmf/nlp042+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=abs --no-check-models
+; COMMAND-LINE: --finite-model-find --no-check-models
; EXPECT: sat
(set-logic UF)
(set-info :status sat)
diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2
new file mode 100644
index 000000000..7ad094dcb
--- /dev/null
+++ b/test/regress/regress2/strings/extf_d_perf.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun _substvar_140_ () String)
+(declare-fun _substvar_195_ () Int)
+(declare-fun _substvar_201_ () Int)
+(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3)))))
+ (and
+ (str.contains _substvar_140_ "://")
+ (str.contains _let_3 "@")
+ (str.contains _let_5 ",")
+ (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
+ (not (= (str.len _let_4) 0))
+ (not (str.contains _let_0 ".sock"))
+ (not (str.contains _let_4 "@"))
+ (not (= (str.len _let_5) 0))
+ (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
+(check-sat)
+
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index eeab46f99..8a6be70b9 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -4,3 +4,4 @@
cvc4_add_unit_test_black(solver_black api)
cvc4_add_unit_test_black(sort_black api)
cvc4_add_unit_test_black(term_black api)
+cvc4_add_unit_test_black(opterm_black api)
diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h
new file mode 100644
index 000000000..637301dd3
--- /dev/null
+++ b/test/unit/api/opterm_black.h
@@ -0,0 +1,57 @@
+/********************* */
+/*! \file opterm_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the Term class
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class OpTermBlack : public CxxTest::TestSuite
+{
+ public:
+ void setUp() override {}
+ void tearDown() override {}
+
+ void testGetKind();
+ void testGetSort();
+ void testIsNull();
+
+ private:
+ Solver d_solver;
+};
+
+void OpTermBlack::testGetKind()
+{
+ OpTerm x;
+ TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
+ x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ TS_ASSERT_THROWS_NOTHING(x.getKind());
+}
+
+void OpTermBlack::testGetSort()
+{
+ OpTerm x;
+ TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
+ x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ TS_ASSERT_THROWS_NOTHING(x.getSort());
+}
+
+void OpTermBlack::testIsNull()
+{
+ OpTerm x;
+ TS_ASSERT(x.isNull());
+ x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ TS_ASSERT(!x.isNull());
+}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 538899a0f..b0249b8a0 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -26,17 +26,34 @@ class SolverBlack : public CxxTest::TestSuite
void setUp() override;
void tearDown() override;
+ void testGetBooleanSort();
+ void testGetIntegerSort();
+ void testGetRealSort();
+ void testGetRegExpSort();
+ void testGetStringSort();
+ void testGetRoundingmodeSort();
+
+ void testMkArraySort();
void testMkBitVectorSort();
void testMkFloatingPointSort();
void testMkDatatypeSort();
void testMkFunctionSort();
+ void testMkParamSort();
void testMkPredicateSort();
+ void testMkRecordSort();
+ void testMkSetSort();
+ void testMkSortConstructorSort();
+ void testMkUninterpretedSort();
void testMkTupleSort();
+
void testDeclareFun();
void testDefineFun();
void testDefineFunRec();
void testDefineFunsRec();
+ void testMkRegexpEmpty();
+ void testMkRegexpSigma();
+
private:
Solver d_solver;
};
@@ -45,6 +62,53 @@ void SolverBlack::setUp() {}
void SolverBlack::tearDown() {}
+void SolverBlack::testGetBooleanSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getBooleanSort());
+}
+
+void SolverBlack::testGetIntegerSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort());
+}
+
+void SolverBlack::testGetRealSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort());
+}
+
+void SolverBlack::testGetRegExpSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getRegExpSort());
+}
+
+void SolverBlack::testGetStringSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getStringSort());
+}
+
+void SolverBlack::testGetRoundingmodeSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.getRoundingmodeSort());
+}
+
+void SolverBlack::testMkArraySort()
+{
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort intSort = d_solver.getIntegerSort();
+ Sort realSort = d_solver.getRealSort();
+ Sort bvSort = d_solver.mkBitVectorSort(32);
+ Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, boolSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(intSort, intSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, realSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, bvSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(fpSort, fpSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, intSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, bvSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, fpSort));
+}
+
void SolverBlack::testMkBitVectorSort()
{
TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
@@ -97,6 +161,12 @@ void SolverBlack::testMkFunctionSort()
CVC4ApiException&);
}
+void SolverBlack::testMkParamSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("T"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort(""));
+}
+
void SolverBlack::testMkPredicateSort()
{
TS_ASSERT_THROWS_NOTHING(
@@ -109,6 +179,37 @@ void SolverBlack::testMkPredicateSort()
CVC4ApiException&);
}
+void SolverBlack::testMkRecordSort()
+{
+ std::vector<std::pair<std::string, Sort>> fields = {
+ std::make_pair("b", d_solver.getBooleanSort()),
+ std::make_pair("bv", d_solver.mkBitVectorSort(8)),
+ std::make_pair("i", d_solver.getIntegerSort())};
+ std::vector<std::pair<std::string, Sort>> empty;
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(fields));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(empty));
+}
+
+void SolverBlack::testMkSetSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getBooleanSort()));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getIntegerSort()));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
+}
+
+void SolverBlack::testMkUninterpretedSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("u"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort(""));
+}
+
+void SolverBlack::testMkSortConstructorSort()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("s", 2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("", 2));
+ TS_ASSERT_THROWS(d_solver.mkSortConstructorSort("", 0), CVC4ApiException&);
+}
+
void SolverBlack::testMkTupleSort()
{
TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
@@ -228,3 +329,19 @@ void SolverBlack::testDefineFunsRec()
d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
CVC4ApiException&);
}
+
+void SolverBlack::testMkRegexpEmpty()
+{
+ Sort strSort = d_solver.getStringSort();
+ Term s = d_solver.mkVar("s", strSort);
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+}
+
+void SolverBlack::testMkRegexpSigma()
+{
+ Sort strSort = d_solver.getStringSort();
+ Term s = d_solver.mkVar("s", strSort);
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback