diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 5 | ||||
-rw-r--r-- | test/regress/regress0/bv/ackermann1.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/ackermann2.smt2 | 2 | ||||
-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.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-extr.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress1/bv/bug787.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/fmf/nlp042+1.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress2/strings/extf_d_perf.smt2 | 19 | ||||
-rw-r--r-- | test/unit/api/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/api/opterm_black.h | 57 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 117 |
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())); +} |