diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/prop | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 7 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 13 | ||||
-rw-r--r-- | src/prop/sat.cpp | 50 | ||||
-rw-r--r-- | src/prop/sat.h | 14 |
4 files changed, 79 insertions, 5 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 09e072370..7f1456639 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -43,8 +43,9 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) : +CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), + d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { } @@ -129,7 +130,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { n.toString().c_str(), n.getType().toString().c_str()); - bool negated = false; + bool negated CVC4_UNUSED = false; SatLiteral lit; if(n.getKind() == kind::NOT) { @@ -178,7 +179,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries - if ( theoryLiteral || + if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || Dump.isOn("clauses") ) { d_nodeCache[lit] = node; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 5eaeeef94..c9fd4a08b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -69,6 +69,13 @@ protected: TranslationCache d_translationCache; NodeCache d_nodeCache; + /** + * True if the lit-to-Node map should be kept for all lits, not just + * theory lits. This is true if e.g. replay logging is on, which + * dumps the Nodes corresponding to decision literals. + */ + const bool d_fullLitToNodeMap; + /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -179,8 +186,10 @@ public: * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use * @param registrar the entity that takes care of preregistration of Nodes + * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * even for non-theory literals. */ - CnfStream(SatInputInterface* satSolver, theory::Registrar registrar); + CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -283,7 +292,7 @@ public: private: /** - * Same as above, except that removable is rememebered. + * Same as above, except that removable is remembered. */ void convertAndAssert(TNode node, bool negated); diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 36f411df4..7df7535dd 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -22,6 +22,7 @@ #include "prop/sat.h" #include "context/context.h" #include "theory/theory_engine.h" +#include "theory/rewriter.h" #include "expr/expr_stream.h" namespace CVC4 { @@ -89,6 +90,55 @@ TNode SatSolver::getNode(SatLiteral lit) { void SatSolver::notifyRestart() { d_propEngine->checkTime(); d_theoryEngine->notifyRestart(); + + static uint32_t lemmaCount = 0; + + if(Options::current()->lemmaInputChannel != NULL) { + while(Options::current()->lemmaInputChannel->hasNewLemma()) { + Debug("shared") << "shared" << std::endl; + Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Node asNode = lemma.getNode(); + asNode = theory::Rewriter::rewrite(asNode); + + if(d_shared.find(asNode) == d_shared.end()) { + d_shared.insert(asNode); + if(asNode.getKind() == kind::OR) { + ++lemmaCount; + if(lemmaCount % 1 == 0) { + Debug("shared") << "=) " << asNode << std::endl; + } + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + } else { + Debug("shared") << "=(" << asNode << std::endl; + } + } else { + Debug("shared") <<"drop shared " << asNode << std::endl; + } + } + } +} + +void SatSolver::notifyNewLemma(SatClause& lemma) { + Assert(lemma.size() > 0); + if(Options::current()->lemmaOutputChannel != NULL) { + if(lemma.size() == 1) { + // cannot share units yet + //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + } else { + NodeBuilder<> b(kind::OR); + for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { + b << d_cnfStream->getNode(lemma[i]); + } + Node n = b; + + if(d_shared.find(n) == d_shared.end()) { + d_shared.insert(n); + Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + } else { + Debug("shared") <<"drop new " << n << std::endl; + } + } + } } SatLiteral SatSolver::getNextReplayDecision() { diff --git a/src/prop/sat.h b/src/prop/sat.h index be3ed244b..e86443827 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + /* Pointer to the concrete SAT solver. Including this via the preprocessor saves us a level of indirection vs, e.g., defining a sub-class for each solver. */ @@ -263,6 +269,8 @@ public: void notifyRestart(); + void notifyNewLemma(SatClause& lemma); + SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine, d_minisat->random_var_freq = Options::current()->satRandomFreq; d_minisat->random_seed = Options::current()->satRandomSeed; + // Give access to all possible options in the sat solver + d_minisat->var_decay = Options::current()->satVarDecay; + d_minisat->clause_decay = Options::current()->satClauseDecay; + d_minisat->restart_first = Options::current()->satRestartFirst; + d_minisat->restart_inc = Options::current()->satRestartInc; + d_statistics.init(d_minisat); } |