diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-05 04:06:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-05 04:06:10 +0000 |
commit | bc3269ad3680436ede31a70803ff5879c9e4bf6e (patch) | |
tree | 867ea6d43ba8bf9d6f0906cd74a563f62f2c39b0 /test/unit | |
parent | 41dddac33ba0332a2ab52983b94044cbdc9e762e (diff) |
Minor adjustments to the Registrar commit in 1644, documentation.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index d2f86d969..fffa36105 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -32,6 +32,13 @@ #include "smt/smt_engine.h" #include "theory/registrar.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" + +#include "theory/builtin/theory_builtin.h" +#include "theory/booleans/theory_bool.h" +#include "theory/arith/theory_arith.h" + using namespace CVC4; using namespace CVC4::context; using namespace CVC4::prop; @@ -78,28 +85,44 @@ public: class CnfStreamBlack : public CxxTest::TestSuite { /** The SAT solver proxy */ - FakeSatSolver *d_satSolver; + FakeSatSolver* d_satSolver; + + /** The theory engine */ + TheoryEngine* d_theoryEngine; + + /** The output channel */ + theory::OutputChannel* d_outputChannel; /** The CNF converter in use */ CnfStream* d_cnfStream; + /** The context */ Context* d_context; - /* ExprManager *d_exprManager; */ - NodeManager *d_nodeManager; + /** The node manager */ + NodeManager* d_nodeManager; void setUp() { d_context = new Context; d_nodeManager = new NodeManager(d_context); + NodeManagerScope nms(d_nodeManager); d_satSolver = new FakeSatSolver; - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, theory::Registrar()); + d_theoryEngine = new TheoryEngine(d_context); + d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(); + d_theoryEngine->addTheory<theory::booleans::TheoryBool>(); + d_theoryEngine->addTheory<theory::arith::TheoryArith>(); + theory::Registrar registrar(d_theoryEngine); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); } void tearDown() { NodeManagerScope nms(d_nodeManager); delete d_cnfStream; + d_theoryEngine->shutdown(); + delete d_theoryEngine; delete d_satSolver; delete d_nodeManager; + delete d_context; } public: |