summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt2
-rw-r--r--test/regress/regress0/strings/issue4662-consume-nterm.smt26
-rw-r--r--test/regress/regress1/quantifiers/eqrange_ex_1.smt2160
-rw-r--r--test/system/CMakeLists.txt2
-rw-r--r--test/system/boilerplate.cpp14
-rw-r--r--test/system/reset_assertions.cpp49
-rw-r--r--test/system/statistics.cpp38
-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.py322
-rw-r--r--test/unit/api/solver_black.h6
-rw-r--r--test/unit/expr/attribute_black.h30
-rw-r--r--test/unit/expr/expr_manager_public.h86
-rw-r--r--test/unit/expr/expr_public.h50
-rw-r--r--test/unit/expr/node_algorithm_black.h17
-rw-r--r--test/unit/expr/symbol_table_black.h14
-rw-r--r--test/unit/expr/type_cardinality_public.h18
-rw-r--r--test/unit/theory/regexp_operation_black.h21
-rw-r--r--test/unit/theory/theory_black.h16
-rw-r--r--test/unit/util/array_store_all_black.h14
-rw-r--r--test/unit/util/datatype_black.h15
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback