diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 10 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 11 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 13 |
3 files changed, 19 insertions, 15 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); } |