diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/issue4662-consume-nterm.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/eqrange_ex_1.smt2 | 160 | ||||
-rw-r--r-- | test/system/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/system/boilerplate.cpp | 14 | ||||
-rw-r--r-- | test/system/reset_assertions.cpp | 49 | ||||
-rw-r--r-- | test/system/statistics.cpp | 38 | ||||
-rw-r--r-- | test/system/two_solvers.cpp (renamed from test/system/two_smt_engines.cpp) | 18 | ||||
-rw-r--r-- | test/unit/api/python/test_sort.py | 322 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 6 | ||||
-rw-r--r-- | test/unit/expr/attribute_black.h | 30 | ||||
-rw-r--r-- | test/unit/expr/expr_manager_public.h | 86 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 50 | ||||
-rw-r--r-- | test/unit/expr/node_algorithm_black.h | 17 | ||||
-rw-r--r-- | test/unit/expr/symbol_table_black.h | 14 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 18 | ||||
-rw-r--r-- | test/unit/theory/regexp_operation_black.h | 21 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 16 | ||||
-rw-r--r-- | test/unit/util/array_store_all_black.h | 14 | ||||
-rw-r--r-- | test/unit/util/datatype_black.h | 15 |
20 files changed, 709 insertions, 189 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7863c5ec0..9a58457e6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -966,6 +966,7 @@ set(regress_0_tests regress0/strings/issue3657-evalLeq.smt2 regress0/strings/issue4070.smt2 regress0/strings/issue4376.smt2 + regress0/strings/issue4662-consume-nterm.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 @@ -1526,6 +1527,7 @@ set(regress_1_tests regress1/quantifiers/dump-inst-i.smt2 regress1/quantifiers/dump-inst-proof.smt2 regress1/quantifiers/dump-inst.smt2 + regress1/quantifiers/eqrange_ex_1.smt2 regress1/quantifiers/ext-ex-deq-trigger.smt2 regress1/quantifiers/extract-nproc.smt2 regress1/quantifiers/f993-loss-easy.smt2 diff --git a/test/regress/regress0/strings/issue4662-consume-nterm.smt2 b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 new file mode 100644 index 000000000..a87279b4c --- /dev/null +++ b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(define-fun b () RegLan (str.to_re "A")) +(assert (str.in_re (str.++ "B" a) (re.+ (re.++ (re.opt b) (re.opt b))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/eqrange_ex_1.smt2 b/test/regress/regress1/quantifiers/eqrange_ex_1.smt2 new file mode 100644 index 000000000..ca53d7cf5 --- /dev/null +++ b/test/regress/regress1/quantifiers/eqrange_ex_1.smt2 @@ -0,0 +1,160 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :produce-models true) +(define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0)) +(define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select m (bvadd a (_ bv7 64))) (concat (select m (bvadd a (_ bv6 64))) (concat (select m (bvadd a (_ bv5 64))) (concat (select m (bvadd a (_ bv4 64))) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a))))))))) +(define-fun mem_writebv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64)) (v (_ BitVec 32))) (Array (_ BitVec 64) (_ BitVec 8)) (store (store (store (store m a ((_ extract 7 0) v)) (bvadd a (_ bv1 64)) ((_ extract 15 8) v)) (bvadd a (_ bv2 64)) ((_ extract 23 16) v)) (bvadd a (_ bv3 64)) ((_ extract 31 24) v))) +(define-fun mem_writebv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64)) (v (_ BitVec 64))) (Array (_ BitVec 64) (_ BitVec 8)) (store (store (store (store (store (store (store (store m a ((_ extract 7 0) v)) (bvadd a (_ bv1 64)) ((_ extract 15 8) v)) (bvadd a (_ bv2 64)) ((_ extract 23 16) v)) (bvadd a (_ bv3 64)) ((_ extract 31 24) v)) (bvadd a (_ bv4 64)) ((_ extract 39 32) v)) (bvadd a (_ bv5 64)) ((_ extract 47 40) v)) (bvadd a (_ bv6 64)) ((_ extract 55 48) v)) (bvadd a (_ bv7 64)) ((_ extract 63 56) v))) +(declare-fun fnstart_rcx () (_ BitVec 64)) +(declare-fun fnstart_rdx () (_ BitVec 64)) +(declare-fun fnstart_rbx () (_ BitVec 64)) +(declare-fun fnstart_rsp () (_ BitVec 64)) +(declare-fun fnstart_rbp () (_ BitVec 64)) +(declare-fun fnstart_rsi () (_ BitVec 64)) +(declare-fun fnstart_rdi () (_ BitVec 64)) +(declare-fun fnstart_r8 () (_ BitVec 64)) +(declare-fun fnstart_r9 () (_ BitVec 64)) +(declare-fun fnstart_r12 () (_ BitVec 64)) +(declare-fun fnstart_r13 () (_ BitVec 64)) +(declare-fun fnstart_r14 () (_ BitVec 64)) +(declare-fun fnstart_r15 () (_ BitVec 64)) +(declare-const stack_alloc_min (_ BitVec 64)) +(assert (= (bvand stack_alloc_min #x0000000000000fff) (_ bv0 64))) +(assert (bvult (_ bv4096 64) stack_alloc_min)) +(define-fun stack_guard_min () (_ BitVec 64) (bvsub stack_alloc_min (_ bv4096 64))) +(assert (bvult stack_guard_min stack_alloc_min)) +(declare-const stack_max (_ BitVec 64)) +(assert (= (bvand stack_max #x0000000000000fff) (_ bv0 64))) +(assert (bvult stack_alloc_min stack_max)) +(assert (bvule stack_alloc_min fnstart_rsp)) +(assert (bvule fnstart_rsp (bvsub stack_max (_ bv8 64)))) +(define-fun on_stack ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (and (bvule stack_guard_min a) (bvule a e) (bvule e stack_max)))) +(define-fun not_in_stack_range ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (and (bvule a e) (or (bvule e stack_alloc_min) (bvule stack_max a))))) +(assert (bvult fnstart_rsp (bvsub stack_max (_ bv8 64)))) +(assert (= ((_ extract 3 0) fnstart_rsp) (_ bv8 4))) +(define-fun mc_only_stack_range ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (on_stack a sz))) +(define-fun a201340_rip () (_ BitVec 64) #x0000000000201340) +(declare-fun a201340_rax () (_ BitVec 64)) +(define-fun a201340_rcx () (_ BitVec 64) fnstart_rcx) +(define-fun a201340_rdx () (_ BitVec 64) fnstart_rdx) +(define-fun a201340_rbx () (_ BitVec 64) fnstart_rbx) +(define-fun a201340_rsp () (_ BitVec 64) fnstart_rsp) +(define-fun a201340_rbp () (_ BitVec 64) fnstart_rbp) +(define-fun a201340_rsi () (_ BitVec 64) fnstart_rsi) +(define-fun a201340_rdi () (_ BitVec 64) fnstart_rdi) +(define-fun a201340_r8 () (_ BitVec 64) fnstart_r8) +(define-fun a201340_r9 () (_ BitVec 64) fnstart_r9) +(declare-fun a201340_r10 () (_ BitVec 64)) +(declare-fun a201340_r11 () (_ BitVec 64)) +(define-fun a201340_r12 () (_ BitVec 64) fnstart_r12) +(define-fun a201340_r13 () (_ BitVec 64) fnstart_r13) +(define-fun a201340_r14 () (_ BitVec 64) fnstart_r14) +(define-fun a201340_r15 () (_ BitVec 64) fnstart_r15) +(declare-fun a201340_cf () Bool) +(declare-fun a201340_pf () Bool) +(declare-fun a201340_af () Bool) +(declare-fun a201340_zf () Bool) +(declare-fun a201340_sf () Bool) +(declare-fun a201340_tf () Bool) +(declare-fun a201340_if () Bool) +(define-fun a201340_df () Bool false) +(declare-fun a201340_of () Bool) +(declare-fun a201340_ie () Bool) +(declare-fun a201340_de () Bool) +(declare-fun a201340_ze () Bool) +(declare-fun a201340_oe () Bool) +(declare-fun a201340_ue () Bool) +(declare-fun a201340_pe () Bool) +(declare-fun a201340_ef () Bool) +(declare-fun a201340_es () Bool) +(declare-fun a201340_c0 () Bool) +(declare-fun a201340_c1 () Bool) +(declare-fun a201340_c2 () Bool) +(declare-fun a201340_RESERVED_STATUS_11 () Bool) +(declare-fun a201340_RESERVED_STATUS_12 () Bool) +(declare-fun a201340_RESERVED_STATUS_13 () Bool) +(declare-fun a201340_c3 () Bool) +(declare-fun a201340_RESERVED_STATUS_15 () Bool) +(define-fun a201340_x87top () (_ BitVec 3) (_ bv7 3)) +(declare-fun a201340_tag0 () (_ BitVec 2)) +(declare-fun a201340_tag1 () (_ BitVec 2)) +(declare-fun a201340_tag2 () (_ BitVec 2)) +(declare-fun a201340_tag3 () (_ BitVec 2)) +(declare-fun a201340_tag4 () (_ BitVec 2)) +(declare-fun a201340_tag5 () (_ BitVec 2)) +(declare-fun a201340_tag6 () (_ BitVec 2)) +(declare-fun a201340_tag7 () (_ BitVec 2)) +(declare-fun a201340_mm0 () (_ BitVec 80)) +(declare-fun a201340_mm1 () (_ BitVec 80)) +(declare-fun a201340_mm2 () (_ BitVec 80)) +(declare-fun a201340_mm3 () (_ BitVec 80)) +(declare-fun a201340_mm4 () (_ BitVec 80)) +(declare-fun a201340_mm5 () (_ BitVec 80)) +(declare-fun a201340_mm6 () (_ BitVec 80)) +(declare-fun a201340_mm7 () (_ BitVec 80)) +(declare-fun a201340_zmm0 () (_ BitVec 512)) +(declare-fun a201340_zmm1 () (_ BitVec 512)) +(declare-fun a201340_zmm2 () (_ BitVec 512)) +(declare-fun a201340_zmm3 () (_ BitVec 512)) +(declare-fun a201340_zmm4 () (_ BitVec 512)) +(declare-fun a201340_zmm5 () (_ BitVec 512)) +(declare-fun a201340_zmm6 () (_ BitVec 512)) +(declare-fun a201340_zmm7 () (_ BitVec 512)) +(declare-fun a201340_zmm8 () (_ BitVec 512)) +(declare-fun a201340_zmm9 () (_ BitVec 512)) +(declare-fun a201340_zmm10 () (_ BitVec 512)) +(declare-fun a201340_zmm11 () (_ BitVec 512)) +(declare-fun a201340_zmm12 () (_ BitVec 512)) +(declare-fun a201340_zmm13 () (_ BitVec 512)) +(declare-fun a201340_zmm14 () (_ BitVec 512)) +(declare-fun a201340_zmm15 () (_ BitVec 512)) +(declare-fun a201340_zmm16 () (_ BitVec 512)) +(declare-fun a201340_zmm17 () (_ BitVec 512)) +(declare-fun a201340_zmm18 () (_ BitVec 512)) +(declare-fun a201340_zmm19 () (_ BitVec 512)) +(declare-fun a201340_zmm20 () (_ BitVec 512)) +(declare-fun a201340_zmm21 () (_ BitVec 512)) +(declare-fun a201340_zmm22 () (_ BitVec 512)) +(declare-fun a201340_zmm23 () (_ BitVec 512)) +(declare-fun a201340_zmm24 () (_ BitVec 512)) +(declare-fun a201340_zmm25 () (_ BitVec 512)) +(declare-fun a201340_zmm26 () (_ BitVec 512)) +(declare-fun a201340_zmm27 () (_ BitVec 512)) +(declare-fun a201340_zmm28 () (_ BitVec 512)) +(declare-fun a201340_zmm29 () (_ BitVec 512)) +(declare-fun a201340_zmm30 () (_ BitVec 512)) +(declare-fun a201340_zmm31 () (_ BitVec 512)) +(declare-const x86mem_0 (Array (_ BitVec 64) (_ BitVec 8))) +(define-fun return_addr () (_ BitVec 64) (mem_readbv64 x86mem_0 fnstart_rsp)) +(assert (= a201340_rbx fnstart_rbx)) +(assert (= a201340_rsp fnstart_rsp)) +(assert (= a201340_rbp fnstart_rbp)) +(assert (= a201340_r12 fnstart_r12)) +(assert (= a201340_r13 fnstart_r13)) +(assert (= a201340_r14 fnstart_r14)) +(assert (= a201340_r15 fnstart_r15)) +; LLVM: %t0 = call i64 (i64) @add(i64 42) +(define-fun x86local_0 () (_ BitVec 64) (bvsub a201340_rsp (_ bv8 64))) +(assert (mc_only_stack_range x86local_0 (_ bv8 64))) +(define-fun x86mem_1 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv64 x86mem_0 x86local_0 a201340_rbp)) +(define-fun x86local_1 () Bool (distinct ((_ extract 64 64) (bvsub (bvsub ((_ sign_extend 1) x86local_0) (bvneg ((_ sign_extend 1) (_ bv16 64)))) (ite false (_ bv1 65) (_ bv0 65)))) ((_ extract 63 63) (bvsub (bvsub ((_ sign_extend 1) x86local_0) (bvneg ((_ sign_extend 1) (_ bv16 64)))) (ite false (_ bv1 65) (_ bv0 65)))))) +(define-fun x86local_2 () Bool (bvult x86local_0 (_ bv16 64))) +(define-fun x86local_3 () (_ BitVec 64) (bvsub x86local_0 (_ bv16 64))) +(define-fun x86local_4 () Bool (bvslt x86local_3 (_ bv0 64))) +(define-fun x86local_5 () Bool (= x86local_3 (_ bv0 64))) +(define-fun x86local_6 () (_ BitVec 8) ((_ extract 7 0) x86local_3)) +(define-fun x86local_7 () Bool (even_parity x86local_6)) +(define-fun x86local_8 () (_ BitVec 64) (bvadd x86local_0 (_ bv18446744073709551612 64))) +(assert (mc_only_stack_range x86local_8 (_ bv4 64))) +(define-fun x86mem_2 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv32 x86mem_1 x86local_8 (_ bv0 32))) +(define-fun x86local_9 () (_ BitVec 64) (bvsub x86local_3 (_ bv8 64))) +(assert (mc_only_stack_range x86local_9 (_ bv8 64))) +(define-fun x86mem_3 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv64 x86mem_2 x86local_9 #x0000000000201359)) +(assert (= #x0000000000201320 #x0000000000201320)) +(assert (= (_ bv42 64) (_ bv42 64))) +(assert (= (mem_readbv64 x86mem_3 x86local_9) #x0000000000201359)) +(declare-const x86mem_4 (Array (_ BitVec 64) (_ BitVec 8))) +(assert (eqrange x86mem_4 x86mem_3 (bvadd x86local_9 (_ bv8 64)) (bvadd fnstart_rsp (_ bv7 64)))) +; LLVM: br label %block_0_201359 +(check-sat-assuming ((not (= (mem_readbv64 x86mem_4 (bvsub fnstart_rsp (_ bv8 64))) fnstart_rbp)))) +(exit) diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt index 420ce8e6f..041d14295 100644 --- a/test/system/CMakeLists.txt +++ b/test/system/CMakeLists.txt @@ -32,5 +32,5 @@ cvc4_add_system_test(reset_assertions) cvc4_add_system_test(sep_log_api) cvc4_add_system_test(smt2_compliance) cvc4_add_system_test(statistics) -cvc4_add_system_test(two_smt_engines) +cvc4_add_system_test(two_solvers) # TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration) diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index 93f5dceb8..315cec7bf 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -19,18 +19,14 @@ #include <iostream> #include <sstream> -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; using namespace std; int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - Result r = smt.checkEntailed(em.mkConst(true)); - - return (Result::ENTAILED == r) ? 0 : 1; + Solver slv; + Result r = slv.checkEntailed(slv.mkBoolean(true)); + return r.isEntailed() ? 0 : 1; } diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp index 2a94dbd98..dc9bd24f6 100644 --- a/test/system/reset_assertions.cpp +++ b/test/system/reset_assertions.cpp @@ -20,34 +20,31 @@ #include <iostream> #include <sstream> -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); - - smt.setOption("incremental", SExpr(true)); - - Type real = em.realType(); - Expr x = em.mkVar("x", real); - Expr four = em.mkConst(Rational(4)); - Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four); - smt.assertFormula(xEqFour); - std::cout << smt.checkSat() << std::endl; - - smt.resetAssertions(); - - Type elementType = em.integerType(); - Type indexType = em.integerType(); - Type arrayType = em.mkArrayType(indexType, elementType); - Expr array = em.mkVar("array", arrayType); - Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four); - Expr ten = em.mkConst(Rational(10)); - Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten); - smt.assertFormula(arrayAtFour_eq_ten); - std::cout << smt.checkSat() << std::endl; + Solver slv; + slv.setOption("incremental", "true"); + + Sort real = slv.getRealSort(); + Term x = slv.mkConst(real, "x"); + Term four = slv.mkReal(4); + Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four); + slv.assertFormula(xEqFour); + std::cout << slv.checkSat() << std::endl; + + slv.resetAssertions(); + + Sort elementType = slv.getIntegerSort(); + Sort indexType = slv.getIntegerSort(); + Sort arrayType = slv.mkArraySort(indexType, elementType); + Term array = slv.mkConst(arrayType, "array"); + Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four); + Term ten = slv.mkReal(10); + Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten); + slv.assertFormula(arrayAtFour_eq_ten); + std::cout << slv.checkSat() << std::endl; } diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 025aaed11..234246112 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -15,48 +15,52 @@ ** minimally functional. **/ +#include "util/statistics.h" + #include <iostream> #include <sstream> +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "smt/smt_engine.h" #include "util/sexpr.h" -#include "util/statistics.h" using namespace CVC4; using namespace std; int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - smt.setOption("incremental", SExpr("true")); - Expr x = em.mkVar("x", em.integerType()); - Expr y = em.mkVar("y", em.integerType()); - smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5)))); - Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0))); - Result r = smt.checkEntailed(q); + api::Solver slv; + ExprManager* em = slv.getExprManager(); + SmtEngine* smt = slv.getSmtEngine(); + smt->setOption("incremental", SExpr("true")); + Expr x = em->mkVar("x", em->integerType()); + Expr y = em->mkVar("y", em->integerType()); + smt->assertFormula(em->mkExpr( + kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5)))); + Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0))); + Result r = smt->checkEntailed(q); if (r != Result::NOT_ENTAILED) { exit(1); } - Statistics stats = smt.getStatistics(); + Statistics stats = smt->getStatistics(); for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) { cout << "stat " << (*i).first << " is " << (*i).second << endl; } - smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5)))); - r = smt.checkEntailed(q); - Statistics stats2 = smt.getStatistics(); + smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5)))); + r = smt->checkEntailed(q); + Statistics stats2 = smt->getStatistics(); bool different = false; for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) { cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl; cout << "stat2 " << (*i).first << " is " << (*i).second << endl; - if(smt.getStatistic((*i).first) != (*i).second) { - cout << "SMT engine reports different value for statistic " - << (*i).first << ": " << smt.getStatistic((*i).first) << endl; + if (smt->getStatistic((*i).first) != (*i).second) + { + cout << "SMT engine reports different value for statistic " << (*i).first + << ": " << smt->getStatistic((*i).first) << endl; exit(1); } different = different || stats.getStatistic((*i).first) != (*i).second; diff --git a/test/system/two_smt_engines.cpp b/test/system/two_solvers.cpp index 71676482e..c5bea4860 100644 --- a/test/system/two_smt_engines.cpp +++ b/test/system/two_solvers.cpp @@ -17,20 +17,16 @@ #include <iostream> #include <sstream> -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; using namespace std; int main() { - ExprManager em; - Options opts; - SmtEngine smt(&em); - SmtEngine smt2(&em); - Result r = smt.checkEntailed(em.mkConst(true)); - Result r2 = smt2.checkEntailed(em.mkConst(true)); - - return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1; + Solver s1; + Solver s2; + Result r = s1.checkEntailed(s1.mkBoolean(true)); + Result r2 = s2.checkEntailed(s2.mkBoolean(true)); + return r.isEntailed() && r2.isEntailed() ? 0 : 1; } diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py new file mode 100644 index 000000000..507aff2ae --- /dev/null +++ b/test/unit/api/python/test_sort.py @@ -0,0 +1,322 @@ +import pytest + +import pycvc4 +from pycvc4 import kinds + + +def testGetDatatype(): + solver = pycvc4.Solver() + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + # expecting no Error + dtypeSort.getDatatype() + + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(Exception): + # expect an exception + bvSort.getDatatype() + + +def testDatatypeSorts(): + solver = pycvc4.Solver() + intSort = solver.getIntegerSort() + # create datatype sort to test + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", intSort) + cons.addSelectorSelf("tail") + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dt = dtypeSort.getDatatype() + assert not dtypeSort.isConstructor() + + with pytest.raises(Exception): + dtypeSort.getConstructorCodomainSort() + + with pytest.raises(Exception): + dtypeSort.getConstructorDomainSorts() + + with pytest.raises(Exception): + dtypeSort.getConstructorArity() + + # get constructor + dcons = dt[0] + consTerm = dcons.getConstructorTerm() + consSort = consTerm.getSort() + assert consSort.isConstructor() + assert not consSort.isTester() + assert not consSort.isSelector() + assert consSort.getConstructorArity() == 2 + consDomSorts = consSort.getConstructorDomainSorts() + assert consDomSorts[0] == intSort + assert consDomSorts[1] == dtypeSort + assert consSort.getConstructorCodomainSort() == dtypeSort + + # get tester + isConsTerm = dcons.getTesterTerm() + assert isConsTerm.getSort().isTester() + + # get selector + dselTail = dcons[1] + tailTerm = dselTail.getSelectorTerm() + assert tailTerm.getSort().isSelector() + + +def testInstantiate(): + solver = pycvc4.Solver() + # instantiate parametric datatype, check should not fail + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + paramDtypeSort.instantiate([solver.getIntegerSort()]) + + # instantiate non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + with pytest.raises(Exception): + dtypeSort.instantiate([solver.getIntegerSort()]) + + +def testGetFunctionArity(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionArity() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionArity() + + +def testGetFunctionDomainSorts(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionDomainSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionDomainSorts() + + +def testGetFunctionCodomainSort(): + solver = pycvc4.Solver() + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionCodomainSort() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getFunctionCodomainSort() + +def testGetArrayIndexSort(): + solver = pycvc4.Solver() + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayIndexSort() + + with pytest.raises(Exception): + indexSort.getArrayIndexSort() + +def testGetArrayElementSort(): + solver = pycvc4.Solver() + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayElementSort() + + with pytest.raises(Exception): + indexSort.getArrayElementSort() + +def testGetSetElementSort(): + solver = pycvc4.Solver() + setSort = solver.mkSetSort(solver.getIntegerSort()) + setSort.getSetElementSort() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSetElementSort() + +def testGetUninterpretedSortName(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortName() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getUninterpretedSortName() + +def testIsUninterpretedSortParameterized(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.isUninterpretedSortParameterized() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.isUninterpretedSortParameterized() + +def testGetUninterpretedSortParamSorts(): + solver = pycvc4.Solver() + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortParamSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getUninterpretedSortParamSorts() + +def testGetUninterpretedSortConstructorName(): + solver = pycvc4.Solver() + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorName() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSortConstructorName() + +def testGetUninterpretedSortConstructorArity(): + solver = pycvc4.Solver() + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorArity() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getSortConstructorArity() + +def testGetBVSize(): + solver = pycvc4.Solver() + bvSort = solver.mkBitVectorSort(32) + bvSort.getBVSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getBVSize() + +def testGetFPExponentSize(): + solver = pycvc4.Solver() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPExponentSize() + +def testGetFPSignificandSize(): + solver = pycvc4.Solver() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPSignificandSize() + +def testGetDatatypeParamSorts(): + solver = pycvc4.Solver() + # create parametric datatype, check should not fail + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + paramDtypeSort.getDatatypeParamSorts() + # create non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + + with pytest.raises(Exception): + dtypeSort.getDatatypeParamSorts() + + +def testGetDatatypeArity(): + solver = pycvc4.Solver() + # create datatype sort, check should not fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dtypeSort.getDatatypeArity() + # create bv sort, check should fail + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getDatatypeArity() + +def testGetTupleLength(): + solver = pycvc4.Solver() + tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) + tupleSort.getTupleLength() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getTupleLength() + +def testGetTupleSorts(): + solver = pycvc4.Solver() + tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()]) + tupleSort.getTupleSorts() + bvSort = solver.mkBitVectorSort(32) + + with pytest.raises(Exception): + bvSort.getTupleSorts() + +def testSortCompare(): + solver = pycvc4.Solver() + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + bvSort2 = solver.mkBitVectorSort(32) + assert bvSort >= bvSort2 + assert bvSort <= bvSort2 + assert (intSort > boolSort) != (intSort < boolSort) + assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort) + +def testSortSubtyping(): + solver = pycvc4.Solver() + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + assert intSort.isSubsortOf(realSort) + assert not realSort.isSubsortOf(intSort) + assert intSort.isComparableTo(realSort) + assert realSort.isComparableTo(intSort) + + arraySortII = solver.mkArraySort(intSort, intSort) + arraySortIR = solver.mkArraySort(intSort, realSort) + assert not arraySortII.isComparableTo(intSort) + # we do not support subtyping for arrays + assert not arraySortII.isComparableTo(arraySortIR) + + setSortI = solver.mkSetSort(intSort) + setSortR = solver.mkSetSort(realSort) + # we support subtyping for sets + assert setSortI.isSubsortOf(setSortR) + assert setSortR.isComparableTo(setSortI) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index f080f5348..ddff63352 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -95,6 +95,7 @@ class SolverBlack : public CxxTest::TestSuite void testUFIteration(); void testGetInfo(); + void testGetInterpolant(); void testGetOp(); void testGetOption(); void testGetUnsatAssumptions1(); @@ -1309,6 +1310,11 @@ void SolverBlack::testGetInfo() TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&); } +void SolverBlack::testGetInterpolant() +{ + // TODO +} + void SolverBlack::testGetOp() { Sort bv32 = d_solver->mkBitVectorSort(32); diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index f07612119..f671fc869 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -17,15 +17,16 @@ #include <cxxtest/TestSuite.h> //Used in some of the tests -#include <vector> #include <sstream> +#include <vector> +#include "api/cvc4cpp.h" +#include "expr/attribute.h" #include "expr/expr_manager.h" -#include "expr/node_value.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" -#include "expr/attribute.h" +#include "expr/node_value.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -35,27 +36,20 @@ using namespace CVC4::smt; using namespace std; class AttributeBlack : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - NodeManager* d_nodeManager; - SmtEngine* d_smtEngine; - SmtScope* d_scope; - public: void setUp() override { - d_exprManager = new ExprManager(); + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); d_nodeManager = NodeManager::fromExprManager(d_exprManager); - d_smtEngine = new SmtEngine(d_exprManager); + d_smtEngine = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smtEngine); } void tearDown() override { delete d_scope; - delete d_smtEngine; - delete d_exprManager; + delete d_slv; } struct PrimitiveIntAttributeId {}; @@ -135,4 +129,10 @@ private: delete node; } + private: + api::Solver* d_slv; + ExprManager* d_exprManager; + NodeManager* d_nodeManager; + SmtEngine* d_smtEngine; + SmtScope* d_scope; }; diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index d28553e08..c632b913e 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -19,56 +19,28 @@ #include <sstream> #include <string> -#include "expr/expr_manager.h" -#include "expr/expr.h" +#include "api/cvc4cpp.h" #include "base/exception.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" using namespace CVC4; using namespace CVC4::kind; using namespace std; class ExprManagerPublic : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - - void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) { - std::vector<Expr> worklist; - worklist.push_back(expr); - - unsigned int childrenFound = 0; - - while( !worklist.empty() ) { - Expr current = worklist.back(); - worklist.pop_back(); - if( current.getKind() == kind ) { - for( unsigned int i = 0; i < current.getNumChildren(); ++i ) { - worklist.push_back( current[i] ); - } - } else { - childrenFound++; - } - } - - TS_ASSERT_EQUALS( childrenFound, numChildren ); - } - - std::vector<Expr> mkVars(Type type, unsigned int n) { - std::vector<Expr> vars; - for( unsigned int i = 0; i < n; ++i ) { - vars.push_back( d_exprManager->mkVar(type) ); - } - return vars; - } - public: - void setUp() override { d_exprManager = new ExprManager; } + void setUp() override + { + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); + } void tearDown() override { try { - delete d_exprManager; + delete d_slv; } catch (Exception& e) { @@ -128,4 +100,44 @@ private: IllegalArgumentException&); } + private: + void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) + { + std::vector<Expr> worklist; + worklist.push_back(expr); + + unsigned int childrenFound = 0; + + while (!worklist.empty()) + { + Expr current = worklist.back(); + worklist.pop_back(); + if (current.getKind() == kind) + { + for (unsigned int i = 0; i < current.getNumChildren(); ++i) + { + worklist.push_back(current[i]); + } + } + else + { + childrenFound++; + } + } + + TS_ASSERT_EQUALS(childrenFound, numChildren); + } + + std::vector<Expr> mkVars(Type type, unsigned int n) + { + std::vector<Expr> vars; + for (unsigned int i = 0; i < n; ++i) + { + vars.push_back(d_exprManager->mkVar(type)); + } + return vars; + } + + api::Solver* d_slv; + ExprManager* d_exprManager; }; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 09452cc7a..86de45fe9 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -19,9 +19,10 @@ #include <sstream> #include <string> +#include "api/cvc4cpp.h" #include "base/exception.h" -#include "expr/expr_manager.h" #include "expr/expr.h" +#include "expr/expr_manager.h" #include "options/options.h" using namespace CVC4; @@ -29,27 +30,6 @@ using namespace CVC4::kind; using namespace std; class ExprPublic : public CxxTest::TestSuite { -private: - - Options opts; - - ExprManager* d_em; - - Expr* a_bool; - Expr* b_bool; - Expr* c_bool_and; - Expr* and_op; - Expr* plus_op; - Type* fun_type; - Expr* fun_op; - Expr* d_apply_fun_bool; - Expr* null; - - Expr* i1; - Expr* i2; - Expr* r1; - Expr* r2; - public: void setUp() override { @@ -62,7 +42,8 @@ private: free(argv[0]); free(argv[1]); - d_em = new ExprManager(opts); + d_slv = new api::Solver(&opts); + d_em = d_slv->getExprManager(); a_bool = new Expr(d_em->mkVar("a", d_em->booleanType())); b_bool = new Expr(d_em->mkVar("b", d_em->booleanType())); @@ -105,7 +86,7 @@ private: delete b_bool; delete a_bool; - delete d_em; + delete d_slv; } catch (Exception& e) { @@ -466,4 +447,25 @@ private: TS_ASSERT(r1->getExprManager() == d_em); TS_ASSERT(r2->getExprManager() == d_em); } + + private: + Options opts; + + api::Solver* d_slv; + ExprManager* d_em; + + Expr* a_bool; + Expr* b_bool; + Expr* c_bool_and; + Expr* and_op; + Expr* plus_op; + Type* fun_type; + Expr* fun_op; + Expr* d_apply_fun_bool; + Expr* null; + + Expr* i1; + Expr* i2; + Expr* r1; + Expr* r2; }; diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h index 1f799cd40..7505215e7 100644 --- a/test/unit/expr/node_algorithm_black.h +++ b/test/unit/expr/node_algorithm_black.h @@ -32,13 +32,6 @@ using namespace CVC4::kind; class NodeAlgorithmBlack : public CxxTest::TestSuite { - private: - NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_intTypeNode; - TypeNode* d_boolTypeNode; - TypeNode* d_bvTypeNode; - public: void setUp() override { @@ -51,8 +44,9 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite void tearDown() override { - delete d_intTypeNode; + delete d_bvTypeNode; delete d_boolTypeNode; + delete d_intTypeNode; delete d_scope; delete d_nodeManager; } @@ -216,4 +210,11 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite TS_ASSERT_EQUALS(subs.size(), 1); TS_ASSERT_EQUALS(subs[x], a); } + + private: + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; + TypeNode* d_intTypeNode; + TypeNode* d_boolTypeNode; + TypeNode* d_bvTypeNode; }; diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 17bab05a4..12a55560d 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -19,6 +19,7 @@ #include <sstream> #include <string> +#include "api/cvc4cpp.h" #include "base/check.h" #include "base/exception.h" #include "context/context.h" @@ -33,16 +34,13 @@ using namespace CVC4::context; using namespace std; class SymbolTableBlack : public CxxTest::TestSuite { -private: - - ExprManager* d_exprManager; - public: void setUp() override { try { - d_exprManager = new ExprManager; + d_slv = new api::Solver(); + d_exprManager = d_slv->getExprManager(); } catch (Exception& e) { @@ -54,7 +52,7 @@ private: void tearDown() override { try { - delete d_exprManager; + delete d_slv; } catch (Exception& e) { @@ -164,4 +162,8 @@ private: // TODO: What kind of exception gets thrown here? TS_ASSERT_THROWS(symtab.popScope(), ScopeException&); } + + private: + api::Solver* d_slv; + ExprManager* d_exprManager; };/* class SymbolTableBlack */ diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 29d9f5dc2..49d6bd9fd 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -17,12 +17,13 @@ #include <cxxtest/TestSuite.h> #include <iostream> -#include <string> #include <sstream> +#include <string> +#include "api/cvc4cpp.h" +#include "expr/expr_manager.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/expr_manager.h" #include "util/cardinality.h" using namespace CVC4; @@ -30,12 +31,14 @@ using namespace CVC4::kind; using namespace std; class TypeCardinalityPublic : public CxxTest::TestSuite { - ExprManager* d_em; - public: - void setUp() override { d_em = new ExprManager(); } + void setUp() override + { + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + } - void tearDown() override { delete d_em; } + void tearDown() override { delete d_slv; } void testTheBasics() { @@ -226,4 +229,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { } } + private: + api::Solver* d_slv; + ExprManager* d_em; };/* TypeCardinalityPublic */ diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h index f42207c49..6e01392ab 100644 --- a/test/unit/theory/regexp_operation_black.h +++ b/test/unit/theory/regexp_operation_black.h @@ -14,17 +14,19 @@ ** Unit tests for symbolic regular expression operations. **/ +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <memory> +#include <vector> + +#include "api/cvc4cpp.h" #include "expr/node.h" #include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/strings/regexp_operation.h" -#include <cxxtest/TestSuite.h> -#include <iostream> -#include <memory> -#include <vector> - using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::smt; @@ -40,8 +42,9 @@ class RegexpOperationBlack : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + d_smt = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smt); d_regExpOpr = new RegExpOpr(); @@ -56,8 +59,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite { delete d_regExpOpr; delete d_scope; - delete d_smt; - delete d_em; + delete d_slv; } void includes(Node r1, Node r2) @@ -147,6 +149,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite } private: + api::Solver* d_slv; ExprManager* d_em; SmtEngine* d_smt; SmtScope* d_scope; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 37999b73a..45d13d416 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -17,14 +17,15 @@ #include <cxxtest/TestSuite.h> //Used in some of the tests -#include <vector> #include <sstream> +#include <vector> +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" -#include "expr/node_value.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" +#include "expr/node_value.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/rewriter.h" @@ -40,8 +41,9 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() override { - d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); + d_smt = d_slv->getSmtEngine(); d_scope = new SmtScope(d_smt); // Ensure that the SMT engine is fully initialized (required for the // rewriter) @@ -53,8 +55,7 @@ class TheoryBlack : public CxxTest::TestSuite { void tearDown() override { delete d_scope; - delete d_smt; - delete d_em; + delete d_slv; } void testArrayConst() { @@ -149,6 +150,7 @@ class TheoryBlack : public CxxTest::TestSuite { } private: + api::Solver* d_slv; ExprManager* d_em; SmtEngine* d_smt; NodeManager* d_nm; diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 3b00fa192..bf0163317 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -16,6 +16,7 @@ #include <cxxtest/TestSuite.h> +#include "api/cvc4cpp.h" #include "expr/array_store_all.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -27,18 +28,14 @@ using namespace CVC4; using namespace std; class ArrayStoreAllBlack : public CxxTest::TestSuite { - ExprManager* d_em; - public: void setUp() override { - d_em = new ExprManager(); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); } - void tearDown() override - { - delete d_em; - } + void tearDown() override { delete d_slv; } void testStoreAll() { Type usort = d_em->mkSort("U"); @@ -80,4 +77,7 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite { d_em->mkConst(Rational(0))))); } + private: + api::Solver* d_slv; + ExprManager* d_em; }; /* class ArrayStoreAllBlack */ diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index f69cc12ea..ac27acfb5 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -15,8 +15,10 @@ **/ #include <cxxtest/TestSuite.h> + #include <sstream> +#include "api/cvc4cpp.h" #include "expr/datatype.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -27,14 +29,11 @@ using namespace CVC4; using namespace std; class DatatypeBlack : public CxxTest::TestSuite { - - ExprManager* d_em; - ExprManagerScope* d_scope; - public: void setUp() override { - d_em = new ExprManager(); + d_slv = new api::Solver(); + d_em = d_slv->getExprManager(); d_scope = new ExprManagerScope(*d_em); Debug.on("datatypes"); Debug.on("groundterms"); @@ -43,7 +42,7 @@ class DatatypeBlack : public CxxTest::TestSuite { void tearDown() override { delete d_scope; - delete d_em; + delete d_slv; } void testEnumeration() { @@ -436,4 +435,8 @@ class DatatypeBlack : public CxxTest::TestSuite { TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); } + private: + api::Solver* d_slv; + ExprManager* d_em; + ExprManagerScope* d_scope; };/* class DatatypeBlack */ |