summaryrefslogtreecommitdiff
path: root/test/unit/prop/cnf_stream_black.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-04-28 01:12:21 +0000
committerMorgan Deters <mdeters@gmail.com>2012-04-28 01:12:21 +0000
commit9ac1cb18f03a5edf4b50532d29e195f74d6a83c2 (patch)
tree1a0a5d07391b8d22d546c64bd050b9ec4396352b /test/unit/prop/cnf_stream_black.h
parentbee9dd1d28afec632381083bdfb7e3ed119dd35a (diff)
New LogicInfo functionality.
src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps track of which theories are active (which should remain constant throughout the life of an SmtEngine) and other details (like integers, reals, linear/nonlinear, etc.). This class has a default constructor which is the most all-inclusive logic. Alternatively, this class can be constructed from an SMT-LIB logic string (the empty string gives the same as "QF_SAT"). Once constructed, theories can be enabled or disabled, quantifiers flipped on and off, integers flipped on and off, etc. At any point an SMT-LIB-like logic string can be extracted. The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine (and, in turn, the theories) only a const reference to it. This ensures that the logic info doesn't mutate over the course of the run. As part of this commit, the TheoryEngine's old notion of "active theories" has been completely removed. As a result, SMT benchmarks that are incorrectly tagged with a logic will assert-fail or worse. (We should probably fail more gracefully in this case.) One such example was bug303.smt2, which used UF reasoning but was tagged QF_LIA. This has been fixed.
Diffstat (limited to 'test/unit/prop/cnf_stream_black.h')
-rw-r--r--test/unit/prop/cnf_stream_black.h7
1 files changed, 6 insertions, 1 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 5c20b534d..63ba95b57 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -110,6 +110,9 @@ class CnfStreamBlack : public CxxTest::TestSuite {
/** The SAT solver proxy */
FakeSatSolver* d_satSolver;
+ /** The logic info */
+ LogicInfo* d_logicInfo;
+
/** The theory engine */
TheoryEngine* d_theoryEngine;
@@ -134,7 +137,8 @@ class CnfStreamBlack : public CxxTest::TestSuite {
d_nodeManager = new NodeManager(d_context, NULL);
NodeManagerScope nms(d_nodeManager);
d_satSolver = new FakeSatSolver();
- d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+ d_logicInfo = new LogicInfo();
+ 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);
d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
@@ -146,6 +150,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
delete d_cnfStream;
d_theoryEngine->shutdown();
delete d_theoryEngine;
+ delete d_logicInfo;
delete d_satSolver;
delete d_nodeManager;
delete d_userContext;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback