summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress1/sygus/issue4009-qep.smt22
-rw-r--r--test/system/smt2_compliance.cpp3
-rw-r--r--test/unit/api/grammar_black.h2
-rw-r--r--test/unit/api/result_black.h2
-rw-r--r--test/unit/api/solver_black.h2
-rw-r--r--test/unit/expr/node_black.h54
-rw-r--r--test/unit/parser/parser_black.h3
-rw-r--r--test/unit/prop/cnf_stream_white.h2
-rw-r--r--test/unit/theory/evaluator_white.h4
-rw-r--r--test/unit/theory/sequences_rewriter_white.h4
-rw-r--r--test/unit/theory/theory_bv_rewriter_white.h4
-rw-r--r--test/unit/theory/theory_strings_word_white.h4
12 files changed, 39 insertions, 47 deletions
diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2
index 6f17a0c04..cc79954c4 100644
--- a/test/regress/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/regress1/sygus/issue4009-qep.smt2
@@ -1,5 +1,5 @@
; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --sygus-qe-preproc
+; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
index 592144eaa..340326e40 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/system/smt2_compliance.cpp
@@ -61,8 +61,7 @@ int main()
void testGetInfo(api::Solver* solver, const char* s)
{
- ParserBuilder pb(
- solver, "<internal>", solver->getExprManager()->getOptions());
+ ParserBuilder pb(solver, "<internal>", solver->getOptions());
Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
assert(p != NULL);
Command* c = p->nextCommand();
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
index f30f6b0ad..eee067ef2 100644
--- a/test/unit/api/grammar_black.h
+++ b/test/unit/api/grammar_black.h
@@ -37,7 +37,7 @@ class GrammarBlack : public CxxTest::TestSuite
void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
-void GrammarBlack::tearDown() {}
+void GrammarBlack::tearDown() { d_solver.reset(nullptr); }
void GrammarBlack::testAddRule()
{
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
index cbfc9cf23..f9f37a019 100644
--- a/test/unit/api/result_black.h
+++ b/test/unit/api/result_black.h
@@ -22,7 +22,7 @@ class ResultBlack : public CxxTest::TestSuite
{
public:
void setUp() { d_solver.reset(new Solver()); }
- void tearDown() override {}
+ void tearDown() override { d_solver.reset(nullptr); }
void testIsNull();
void testEq();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 4a7b74c8e..d10813f58 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -167,7 +167,7 @@ class SolverBlack : public CxxTest::TestSuite
void SolverBlack::setUp() { d_solver.reset(new Solver()); }
-void SolverBlack::tearDown() {}
+void SolverBlack::tearDown() { d_solver.reset(nullptr); }
void SolverBlack::testGetBooleanSort()
{
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 1b8a7c92f..91242322a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -22,6 +22,8 @@
#include <string>
#include <vector>
+#include "api/cvc4cpp.h"
+#include "smt/smt_engine.h"
#include "expr/expr_manager.h"
#include "expr/node.h"
#include "expr/node_builder.h"
@@ -50,15 +52,13 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N,
class NodeBlack : public CxxTest::TestSuite {
private:
- Options opts;
NodeManager* d_nodeManager;
- NodeManagerScope* d_scope;
- TypeNode* d_booleanType;
- TypeNode* d_realType;
-
+ api::Solver* d_slv;
public:
void setUp() override
{
+ // setup a SMT engine so that options are in scope
+ Options opts;
char* argv[2];
argv[0] = strdup("");
argv[1] = strdup("--output-lang=ast");
@@ -66,18 +66,12 @@ class NodeBlack : public CxxTest::TestSuite {
free(argv[0]);
free(argv[1]);
- d_nodeManager = new NodeManager(NULL, opts);
- d_scope = new NodeManagerScope(d_nodeManager);
- d_booleanType = new TypeNode(d_nodeManager->booleanType());
- d_realType = new TypeNode(d_nodeManager->realType());
+ d_slv = new api::Solver(&opts);
+ d_nodeManager = d_slv->getSmtEngine()->getNodeManager();
}
- void tearDown() override
- {
- delete d_realType;
- delete d_booleanType;
- delete d_scope;
- delete d_nodeManager;
+ void tearDown() override {
+ delete d_slv;
}
bool imp(bool a, bool b) const { return (!a) || (b); }
@@ -114,12 +108,12 @@ class NodeBlack : public CxxTest::TestSuite {
void testOperatorEquals() {
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
TS_ASSERT(a == a);
TS_ASSERT(a == b);
@@ -148,12 +142,12 @@ class NodeBlack : public CxxTest::TestSuite {
void testOperatorNotEquals() {
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
/*structed assuming operator == works */
TS_ASSERT(iff(a != a, !(a == a)));
@@ -208,7 +202,7 @@ class NodeBlack : public CxxTest::TestSuite {
void testOperatorAssign() {
Node a, b;
Node c = d_nodeManager->mkNode(
- NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
+ NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
b = c;
TS_ASSERT(b == c);
@@ -324,8 +318,8 @@ class NodeBlack : public CxxTest::TestSuite {
void testIteNode() {
/*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
- Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
- Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
Node cnd = d_nodeManager->mkNode(OR, a, b);
Node thenBranch = d_nodeManager->mkConst(true);
@@ -383,8 +377,8 @@ class NodeBlack : public CxxTest::TestSuite {
void testGetKind() {
/*inline Kind getKind() const; */
- Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
- Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, a);
TS_ASSERT(NOT == n.getKind());
@@ -392,8 +386,8 @@ class NodeBlack : public CxxTest::TestSuite {
n = d_nodeManager->mkNode(EQUAL, a, b);
TS_ASSERT(EQUAL == n.getKind());
- Node x = d_nodeManager->mkSkolem("x", *d_realType);
- Node y = d_nodeManager->mkSkolem("y", *d_realType);
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
n = d_nodeManager->mkNode(PLUS, x, y);
TS_ASSERT(PLUS == n.getKind());
@@ -470,9 +464,9 @@ class NodeBlack : public CxxTest::TestSuite {
// test iterators
void testIterator() {
NodeBuilder<> b;
- Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
- Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
- Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
Node n = b << x << y << z << kind::AND;
{ // iterator
@@ -717,7 +711,7 @@ class NodeBlack : public CxxTest::TestSuite {
// This is for demonstrating what a certain type of user error looks like.
// Node level0(){
// NodeBuilder<> nb(kind::AND);
- // Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+ // Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
// nb << x;
// nb << x;
// return Node(nb.constructNode());
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 9d5a0fc8d..8668f746b 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -209,8 +209,7 @@ class ParserBlack
d_solver.reset(new api::Solver(&d_options));
}
- void tearDown() {
- }
+ void tearDown() { d_solver.reset(nullptr); }
private:
InputLanguage d_lang;
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 4a30b4179..24dd5ae62 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -145,7 +145,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
d_satSolver = new FakeSatSolver();
d_cnfContext = new context::Context();
d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
- ResourceManager * rm = d_nodeManager->getResourceManager();
+ ResourceManager* rm = d_smt->getResourceManager();
d_cnfStream = new CVC4::prop::TseitinCnfStream(
d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
}
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 3fc95b2a5..0a50bae2d 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -48,9 +48,9 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
+ d_em = new ExprManager;
d_nm = NodeManager::fromExprManager(d_em);
- d_smt = new SmtEngine(d_em);
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
}
diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index c9c897f5f..347289693 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -46,8 +46,8 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
d_rewriter = new ExtendedRewriter(true);
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index d2284aa8f..e6110256a 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -40,8 +40,8 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_smt->finalOptionsAreSet();
diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h
index 2e29d50b8..048d1d707 100644
--- a/test/unit/theory/theory_strings_word_white.h
+++ b/test/unit/theory/theory_strings_word_white.h
@@ -37,8 +37,8 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_em = new ExprManager;
+ d_smt = new SmtEngine(d_em, &opts);
d_scope = new SmtScope(d_smt);
d_nm = NodeManager::currentNM();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback