diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
commit | e568f34e1f4713c678336fbef1006e585128d466 (patch) | |
tree | a20636a5d50a84d22016f278e9f3a036436125dd /test/unit/prop | |
parent | d71827eef17c181d225f64ea59d26c34d76b9b1e (diff) |
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
Diffstat (limited to 'test/unit/prop')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c24104acc..de0510582 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -146,6 +146,7 @@ class CnfStreamBlack : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); d_satSolver = new FakeSatSolver(); d_logicInfo = new LogicInfo(); + d_logicInfo->lock(); d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo); d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); @@ -200,9 +201,15 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } + void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -255,12 +262,6 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } - void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); - } - void testVar() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); |