From bc3269ad3680436ede31a70803ff5879c9e4bf6e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 5 Apr 2011 04:06:10 +0000 Subject: [PATCH] Minor adjustments to the Registrar commit in 1644, documentation. --- src/prop/cnf_stream.cpp | 10 ++++---- src/prop/cnf_stream.h | 11 +++++---- src/prop/prop_engine.cpp | 13 +++++++---- src/theory/registrar.h | 39 +++++++++++++++++++++++-------- src/theory/theory_engine.cpp | 8 +++++-- src/theory/theory_engine.h | 6 ++--- test/unit/prop/cnf_stream_black.h | 31 ++++++++++++++++++++---- 7 files changed, 84 insertions(+), 34 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 65ed6caf6..fc7fa600a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -5,7 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): cconway, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -34,8 +34,8 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar reg) : - d_satSolver(satSolver), d_registrar(reg) { +CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : + d_satSolver(satSolver), d_registrar(registrar) { } void CnfStream::recordTranslation(TNode node) { @@ -47,8 +47,8 @@ void CnfStream::recordTranslation(TNode node) { } -TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg) : - CnfStream(satSolver, reg) { +TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) : + CnfStream(satSolver, registrar) { } void CnfStream::assertClause(TNode node, SatClause& c) { diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 929cae346..28b2cfb03 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -2,10 +2,10 @@ /*! \file cnf_stream.h ** \verbatim ** Original author: taking - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters, cconway + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -71,6 +71,7 @@ private: protected: + /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; /** Top level nodes that we translated */ @@ -180,7 +181,7 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use */ - CnfStream(SatInputInterface* satSolver, theory::Registrar r); + CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -255,7 +256,7 @@ public: * Constructs the stream to use the given sat solver. * @param satSolver the sat solver to use */ - TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg); + TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar); private: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 84e51d1d9..63228a803 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -2,8 +2,8 @@ /*! \file prop_engine.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): taking + ** Major contributors: taking, cconway, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of the propositional engine of CVC4. + ** \brief Implementation of the propositional engine of CVC4 ** ** Implementation of the propositional engine of CVC4. **/ @@ -62,9 +62,12 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) : d_theoryEngine(te), d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; + d_satSolver = new SatSolver(this, d_theoryEngine, d_context); - theory::Registrar reg(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, reg); + + theory::Registrar registrar(d_theoryEngine); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); + d_satSolver->setCnfStream(d_cnfStream); } diff --git a/src/theory/registrar.h b/src/theory/registrar.h index ce3a301d7..19315827e 100644 --- a/src/theory/registrar.h +++ b/src/theory/registrar.h @@ -1,7 +1,30 @@ +/********************* */ +/*! \file registrar.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Class to encapsulate preregistration duties + ** + ** Class to encapsulate preregistration duties. This class permits the + ** CNF stream implementation to reach into the theory engine to + ** preregister only those terms with an associated SAT literal (at the + ** point when they get the SAT literal), without having to refer to the + ** TheoryEngine class directly. + **/ + #include "cvc4_private.h" -#ifndef __CVC4__THEORY_REGISTRAR_H -#define __CVC4__THEORY_REGISTRAR_H +#ifndef __CVC4__THEORY__REGISTRAR_H +#define __CVC4__THEORY__REGISTRAR_H + #include "theory/theory_engine.h" namespace CVC4 { @@ -12,20 +35,16 @@ private: TheoryEngine* d_theoryEngine; public: - Registrar() : d_theoryEngine(NULL){ } - Registrar(TheoryEngine* te) : d_theoryEngine(te){ } + Registrar(TheoryEngine* te) : d_theoryEngine(te) { } - void preRegister(Node n){ - if(d_theoryEngine != NULL){ - d_theoryEngine->preRegister(n); - } + void preRegister(Node n) { + d_theoryEngine->preRegister(n); } };/* class Registrar */ - }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_REGISTRAR_H */ +#endif /* __CVC4__THEORY__REGISTRAR_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index aa70a9bda..cb29bb98e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -137,6 +137,10 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : d_incomplete(ctxt, false), d_statistics() { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + d_theoryTable[theoryId] = NULL; + } + Rewriter::init(); d_sharedTermManager = new SharedTermManager(this, ctxt); @@ -145,8 +149,8 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { - if (d_theoryTable[theoryId]) { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { delete d_theoryTable[theoryId]; } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2e12d3a16..1cdae3810 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -85,7 +85,7 @@ class TheoryEngine { d_engine(engine), d_context(context), d_conflictNode(context), - d_explanationNode(context){ + d_explanationNode(context) { } void newFact(TNode n); @@ -212,8 +212,8 @@ public: d_hasShutDown = true; // Shutdown all the theories - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { - if (d_theoryTable[theoryId]) { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { d_theoryTable[theoryId]->shutdown(); } } 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(); + d_theoryEngine->addTheory(); + d_theoryEngine->addTheory(); + 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: -- 2.30.2