From 5eabda0f55cee3be81aa7ae126269c32e818322f Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 5 Jan 2016 16:29:44 -0800 Subject: Add SmtGlobals Class - The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library. - The option replayLog has been removed due to inconsistent memory management. - SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently. - There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine. - A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction. - Selected classes have been given a copy of this pointer in their constructors. - Removed the dependence on Node from Result. Moving Result back into util/. --- test/unit/prop/cnf_stream_white.h | 4 +++- test/unit/theory/theory_arith_white.h | 3 ++- test/unit/theory/theory_engine_white.h | 11 ++++++----- test/unit/theory/theory_white.h | 16 ++++++++++------ 4 files changed, 21 insertions(+), 13 deletions(-) (limited to 'test/unit') diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index e705da409..bab71d8b2 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -155,7 +155,9 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_theoryEngine = d_smt->d_theoryEngine; d_satSolver = new FakeSatSolver(); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine), new context::Context()); + d_cnfStream = new CVC4::prop::TseitinCnfStream( + d_satSolver, new theory::TheoryRegistrar(d_theoryEngine), + new context::Context(), d_smt->globals()); } void tearDown() { diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index d8615eda7..4313a9b64 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -114,7 +114,8 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL; - d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo); + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), + d_logicInfo, d_smt->globals()); preregistered = new std::set(); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 399feb43e..2ecb4e225 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -120,13 +120,14 @@ class FakeTheory : public Theory { // static std::deque s_expected; public: - FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) + FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) : + Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, globals) { } /** Register an expected rewrite call */ - static void expect(RewriteType type, FakeTheory* thy, - TNode n, bool topLevel) throw() { + static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel) + throw() + { RewriteItem item = { type, thy, n, topLevel }; //s_expected.push_back(item); } @@ -224,7 +225,7 @@ public: void registerTerm(TNode) { Unimplemented(); } void check(Theory::Effort) { Unimplemented(); } void propagate(Theory::Effort) { Unimplemented(); } - void explain(TNode, Theory::Effort) { Unimplemented(); } + Node explain(TNode) { Unimplemented(); } Node getValue(TNode n) { return Node::null(); } };/* class FakeTheory */ diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index c804ca307..429e72fc6 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -52,7 +52,9 @@ public: ~TestOutputChannel() {} - void safePoint() throw(Interrupted, AssertionException) {} + void safePoint(uint64_t amount) + throw(Interrupted, UnsafeInterruptException, AssertionException) + {} void conflict(TNode n) throw(AssertionException) { @@ -119,9 +121,10 @@ public: set d_registered; vector d_getSequence; - DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) { - } + DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, globals) + {} void registerTerm(TNode n) { // check that we registerTerm() a term only once @@ -156,7 +159,7 @@ public: } void preRegisterTerm(TNode n) {} void propagate(Effort level) {} - void explain(TNode n, Effort level) {} + Node explain(TNode n) { return Node::null(); } Node getValue(TNode n) { return Node::null(); } string identify() const { return "DummyTheory"; } };/* class DummyTheory */ @@ -196,7 +199,8 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; - d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo); + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), + *d_logicInfo, d_smt->globals()); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); -- cgit v1.2.3