diff options
Diffstat (limited to 'test')
-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/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/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 |
14 files changed, 204 insertions, 181 deletions
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/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/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 */ |