From 41dddac33ba0332a2ab52983b94044cbdc9e762e Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 4 Apr 2011 20:42:23 +0000 Subject: [PATCH] Merging the satliteral-before-prereg branch into trunk. Theory preregistration is now called during the conversion to cnf. This fixes bug 257. --- src/prop/cnf_stream.cpp | 18 +++++++++++++----- src/prop/cnf_stream.h | 7 +++++-- src/prop/prop_engine.cpp | 4 +++- src/smt/smt_engine.cpp | 3 ++- src/theory/Makefile.am | 1 + src/theory/registrar.h | 31 +++++++++++++++++++++++++++++++ src/theory/theory_engine.cpp | 8 ++++---- src/theory/theory_engine.h | 1 + test/unit/prop/cnf_stream_black.h | 3 ++- 9 files changed, 62 insertions(+), 14 deletions(-) create mode 100644 src/theory/registrar.h diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e278c8175..65ed6caf6 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -21,6 +21,7 @@ #include "sat.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" +#include "theory/theory_engine.h" #include "expr/node.h" #include "util/Assert.h" #include "util/output.h" @@ -33,8 +34,8 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver) : - d_satSolver(satSolver) { +CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar reg) : + d_satSolver(satSolver), d_registrar(reg) { } void CnfStream::recordTranslation(TNode node) { @@ -45,8 +46,9 @@ void CnfStream::recordTranslation(TNode node) { } } -TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) : - CnfStream(satSolver) { + +TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg) : + CnfStream(satSolver, reg) { } void CnfStream::assertClause(TNode node, SatClause& c) { @@ -114,6 +116,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // Here, you can have it Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; + // have to keep track of this, because with the call to preRegister(), + // the cnf stream is re-entrant! + bool wasAssertingLemma = d_assertingLemma; + d_registrar.preRegister(node); + d_assertingLemma = wasAssertingLemma; + return lit; } @@ -147,7 +155,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); - Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s", node.toString().c_str()); + Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); SatLiteral literal = find->second.literal; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9d152a915..929cae346 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "prop/sat.h" +#include "theory/registrar.h" #include @@ -70,6 +71,8 @@ private: protected: + theory::Registrar d_registrar; + /** Top level nodes that we translated */ std::vector d_translationTrail; @@ -177,7 +180,7 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use */ - CnfStream(SatInputInterface* satSolver); + CnfStream(SatInputInterface* satSolver, theory::Registrar r); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -252,7 +255,7 @@ public: * Constructs the stream to use the given sat solver. * @param satSolver the sat solver to use */ - TseitinCnfStream(SatInputInterface* satSolver); + TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg); private: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4da3aa842..84e51d1d9 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -21,6 +21,7 @@ #include "sat.h" #include "theory/theory_engine.h" +#include "theory/registrar.h" #include "util/Assert.h" #include "util/options.h" #include "util/output.h" @@ -62,7 +63,8 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) : d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; d_satSolver = new SatSolver(this, d_theoryEngine, d_context); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); + theory::Registrar reg(d_theoryEngine); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, reg); d_satSolver->setCnfStream(d_cnfStream); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb6dd3460..6ea9de45e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -463,7 +463,8 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) throw(NoSuchFunctionException, AssertionException) { Debug("smt") << "push_back assertion " << n << endl; smt.d_haveAdditions = true; - smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); + Node node = SmtEnginePrivate::preprocess(smt, n); + smt.d_propEngine->assertFormula(node); } void SmtEngine::ensureBoolean(const BoolExpr& e) { diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index a9ff5376d..b72502eca 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -19,6 +19,7 @@ libtheory_la_SOURCES = \ shared_term_manager.cpp \ shared_data.h \ shared_data.cpp \ + registrar.h \ rewriter.h \ rewriter_attributes.h \ rewriter.cpp \ diff --git a/src/theory/registrar.h b/src/theory/registrar.h new file mode 100644 index 000000000..ce3a301d7 --- /dev/null +++ b/src/theory/registrar.h @@ -0,0 +1,31 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_REGISTRAR_H +#define __CVC4__THEORY_REGISTRAR_H +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +class Registrar { +private: + TheoryEngine* d_theoryEngine; + +public: + Registrar() : d_theoryEngine(NULL){ } + + Registrar(TheoryEngine* te) : d_theoryEngine(te){ } + + void preRegister(Node n){ + if(d_theoryEngine != NULL){ + d_theoryEngine->preRegister(n); + } + } + +};/* class Registrar */ + + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY_REGISTRAR_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d1040e6fc..aa70a9bda 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -162,13 +162,15 @@ struct preprocess_stack_element { }; Node TheoryEngine::preprocess(TNode node) { - // Remove ITEs and rewrite the node Node preprocessed = Rewriter::rewrite(removeITEs(node)); + return preprocessed; +} +void TheoryEngine::preRegister(TNode preprocessed) { // If we are pre-registered already we are done if (preprocessed.getAttribute(PreRegistered())) { - return preprocessed; + return; } // Do a topological sort of the subexpressions and preregister them @@ -223,8 +225,6 @@ Node TheoryEngine::preprocess(TNode node) { } } } - - return preprocessed; } /** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index be2e6e271..2e12d3a16 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -247,6 +247,7 @@ public: * @param n the node to preprocess */ Node preprocess(TNode n); + void preRegister(TNode preprocessed); /** * Assert the formula to the appropriate theory. diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 7258e630d..d2f86d969 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,6 +30,7 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" +#include "theory/registrar.h" using namespace CVC4; using namespace CVC4::context; @@ -91,7 +92,7 @@ void setUp() { d_context = new Context; d_nodeManager = new NodeManager(d_context); d_satSolver = new FakeSatSolver; - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, theory::Registrar()); } void tearDown() { -- 2.30.2