registrar.h \
prop_engine.cpp \
prop_engine.h \
- sat.h \
- sat.cpp \
+ theory_proxy.h \
+ theory_proxy.cpp \
cnf_stream.h \
cnf_stream.cpp \
sat_module.h \
#include "util/output.h"
#include "expr/command.h"
#include "expr/expr.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
#include <queue>
#define __CVC4__PROP__CNF_STREAM_H
#include "expr/node.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
#include "prop/registrar.h"
#include <ext/hash_map>
#include "prop/minisat/mtl/Sort.h"
#include "prop/minisat/core/Solver.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
#include "prop/sat_module.h"
#include "util/output.h"
#include "expr/command.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
#include "prop/sat_module.h"
#include "theory/theory_engine.h"
+++ /dev/null
-/********************* */
-/*! \file sat.cpp
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: dejan, taking, 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
-#include "prop/sat.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-#include "theory/rewriter.h"
-#include "expr/expr_stream.h"
-
-namespace CVC4 {
-namespace prop {
-
-void TheoryProxy::variableNotify(SatVariable var) {
- d_theoryEngine->preRegister(getNode(SatLiteral(var)));
-}
-
-void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
- d_theoryEngine->check(effort);
-}
-
-void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
- // Get the propagated literals
- std::vector<TNode> outputNodes;
- d_theoryEngine->getPropagatedLiterals(outputNodes);
- for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
- Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
- output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
- }
-}
-
-void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
- TNode lNode = d_cnfStream->getNode(l);
- Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
- Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
- Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
- if (theoryExplanation.getKind() == kind::AND) {
- Node::const_iterator it = theoryExplanation.begin();
- Node::const_iterator it_end = theoryExplanation.end();
- explanation.push_back(l);
- for (; it != it_end; ++ it) {
- explanation.push_back(~d_cnfStream->getLiteral(*it));
- }
- } else {
- explanation.push_back(l);
- explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
- }
-}
-
-void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
- Node literalNode = d_cnfStream->getNode(l);
- Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
- Assert(!literalNode.isNull());
- d_theoryEngine->assertFact(literalNode);
-}
-
-SatLiteral TheoryProxy::getNextDecisionRequest() {
- TNode n = d_theoryEngine->getNextDecisionRequest();
- return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
-}
-
-bool TheoryProxy::theoryNeedCheck() const {
- return d_theoryEngine->needCheck();
-}
-
-void TheoryProxy::removeClausesAboveLevel(int level) {
- d_cnfStream->removeClausesAboveLevel(level);
-}
-
-TNode TheoryProxy::getNode(SatLiteral lit) {
- return d_cnfStream->getNode(lit);
-}
-
-void TheoryProxy::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 TheoryProxy::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 TheoryProxy::getNextReplayDecision() {
-#ifdef CVC4_REPLAY
- if(Options::current()->replayStream != NULL) {
- Expr e = Options::current()->replayStream->nextExpr();
- if(!e.isNull()) { // we get null node when out of decisions to replay
- // convert & return
- return d_cnfStream->getLiteral(e);
- }
- }
-#endif /* CVC4_REPLAY */
- //FIXME!
- return undefSatLiteral;
-}
-
-void TheoryProxy::logDecision(SatLiteral lit) {
-#ifdef CVC4_REPLAY
- if(Options::current()->replayLog != NULL) {
- Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
- *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
- }
-#endif /* CVC4_REPLAY */
-}
-
-void TheoryProxy::checkTime() {
- d_propEngine->checkTime();
-}
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file sat.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: taking, cconway, dejan
- ** Minor contributors (to current version): barrett
- ** 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 SAT Solver.
- **
- ** SAT Solver.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PROP__SAT_H
-#define __CVC4__PROP__SAT_H
-
-// Just defining this for now, since there's no other SAT solver bindings.
-// Optional blocks below will be unconditionally included
-#define __CVC4_USE_MINISAT
-
-#include "theory/theory.h"
-#include "util/options.h"
-#include "util/stats.h"
-
-#include "prop/sat_module.h"
-
-#ifdef __CVC4_USE_MINISAT
-
-#include "prop/minisat/core/Solver.h"
-#include "prop/minisat/core/SolverTypes.h"
-#include "prop/minisat/simp/SimpSolver.h"
-
-#endif /* __CVC4_USE_MINISAT */
-
-namespace CVC4 {
-
-class TheoryEngine;
-
-namespace prop {
-
-class PropEngine;
-class CnfStream;
-
-/**
- * The proxy class that allows the SatSolver to communicate with the theories
- */
-class TheoryProxy {
-
- /** The prop engine we are using */
- PropEngine* d_propEngine;
-
- /** The CNF engine we are using */
- CnfStream* d_cnfStream;
-
- /** The theory engine we are using */
- TheoryEngine* d_theoryEngine;
-
- /** 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;
-
-public:
- TheoryProxy(PropEngine* propEngine,
- TheoryEngine* theoryEngine,
- context::Context* context,
- CnfStream* cnfStream);
-
- ~TheoryProxy();
-
-
- void theoryCheck(theory::Theory::Effort effort);
-
- void explainPropagation(SatLiteral l, SatClause& explanation);
-
- void theoryPropagate(SatClause& output);
-
- void enqueueTheoryLiteral(const SatLiteral& l);
-
- SatLiteral getNextDecisionRequest();
-
- bool theoryNeedCheck() const;
-
- void removeClausesAboveLevel(int level);
-
- /**
- * Notifies of a new variable at a decision level.
- */
- void variableNotify(SatVariable var);
-
- void unregisterVar(SatLiteral lit);
-
- void renewVar(SatLiteral lit, int level = -1);
-
- TNode getNode(SatLiteral lit);
-
- void notifyRestart();
-
- void notifyNewLemma(SatClause& lemma);
-
- SatLiteral getNextReplayDecision();
-
- void logDecision(SatLiteral lit);
-
- void checkTime();
-
-};/* class SatSolver */
-
-/* Functions that delegate to the concrete SAT solver. */
-
-inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
- TheoryEngine* theoryEngine,
- context::Context* context,
- CnfStream* cnfStream) :
- d_propEngine(propEngine),
- d_cnfStream(cnfStream),
- d_theoryEngine(theoryEngine),
- d_context(context)
-{}
-
-}/* CVC4::prop namespace */
-
-inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
- out << lit.toString();
- return out;
-}
-
-inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
- out << "clause:";
- for(unsigned i = 0; i < clause.size(); ++i) {
- out << " " << clause[i];
- }
- out << ";";
- return out;
-}
-
-inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
- std::string str;
- switch(val) {
- case prop::SatValUnknown:
- str = "_";
- case prop::SatValTrue:
- str = "1";
- case prop::SatValFalse:
- str = "0";
- default:
- str = "Error";
-
- out << str;
- return out;
-}
-
-} /* prop namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PROP__SAT_H */
#include "context/context.h"
#include "theory/theory_engine.h"
#include "expr/expr_stream.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
// DPLLT Minisat
#include "prop/minisat/simp/SimpSolver.h"
--- /dev/null
+/********************* */
+/*! \file sat.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: dejan, taking, 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/theory_proxy.h"
+#include "context/context.h"
+#include "theory/theory_engine.h"
+#include "theory/rewriter.h"
+#include "expr/expr_stream.h"
+
+namespace CVC4 {
+namespace prop {
+
+void TheoryProxy::variableNotify(SatVariable var) {
+ d_theoryEngine->preRegister(getNode(SatLiteral(var)));
+}
+
+void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
+ d_theoryEngine->check(effort);
+}
+
+void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
+ // Get the propagated literals
+ std::vector<TNode> outputNodes;
+ d_theoryEngine->getPropagatedLiterals(outputNodes);
+ for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
+ Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
+ output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
+ }
+}
+
+void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
+ TNode lNode = d_cnfStream->getNode(l);
+ Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
+ Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
+ Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+ if (theoryExplanation.getKind() == kind::AND) {
+ Node::const_iterator it = theoryExplanation.begin();
+ Node::const_iterator it_end = theoryExplanation.end();
+ explanation.push_back(l);
+ for (; it != it_end; ++ it) {
+ explanation.push_back(~d_cnfStream->getLiteral(*it));
+ }
+ } else {
+ explanation.push_back(l);
+ explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
+ }
+}
+
+void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
+ Node literalNode = d_cnfStream->getNode(l);
+ Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
+ Assert(!literalNode.isNull());
+ d_theoryEngine->assertFact(literalNode);
+}
+
+SatLiteral TheoryProxy::getNextDecisionRequest() {
+ TNode n = d_theoryEngine->getNextDecisionRequest();
+ return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
+}
+
+bool TheoryProxy::theoryNeedCheck() const {
+ return d_theoryEngine->needCheck();
+}
+
+void TheoryProxy::removeClausesAboveLevel(int level) {
+ d_cnfStream->removeClausesAboveLevel(level);
+}
+
+TNode TheoryProxy::getNode(SatLiteral lit) {
+ return d_cnfStream->getNode(lit);
+}
+
+void TheoryProxy::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 TheoryProxy::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 TheoryProxy::getNextReplayDecision() {
+#ifdef CVC4_REPLAY
+ if(Options::current()->replayStream != NULL) {
+ Expr e = Options::current()->replayStream->nextExpr();
+ if(!e.isNull()) { // we get null node when out of decisions to replay
+ // convert & return
+ return d_cnfStream->getLiteral(e);
+ }
+ }
+#endif /* CVC4_REPLAY */
+ //FIXME!
+ return undefSatLiteral;
+}
+
+void TheoryProxy::logDecision(SatLiteral lit) {
+#ifdef CVC4_REPLAY
+ if(Options::current()->replayLog != NULL) {
+ Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
+ *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
+ }
+#endif /* CVC4_REPLAY */
+}
+
+void TheoryProxy::checkTime() {
+ d_propEngine->checkTime();
+}
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sat.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: taking, cconway, dejan
+ ** Minor contributors (to current version): barrett
+ ** 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 SAT Solver.
+ **
+ ** SAT Solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROP__SAT_H
+#define __CVC4__PROP__SAT_H
+
+// Just defining this for now, since there's no other SAT solver bindings.
+// Optional blocks below will be unconditionally included
+#define __CVC4_USE_MINISAT
+
+#include "theory/theory.h"
+#include "util/options.h"
+#include "util/stats.h"
+
+#include "prop/sat_module.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace prop {
+
+class PropEngine;
+class CnfStream;
+
+/**
+ * The proxy class that allows the SatSolver to communicate with the theories
+ */
+class TheoryProxy {
+
+ /** The prop engine we are using */
+ PropEngine* d_propEngine;
+
+ /** The CNF engine we are using */
+ CnfStream* d_cnfStream;
+
+ /** The theory engine we are using */
+ TheoryEngine* d_theoryEngine;
+
+ /** 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;
+
+public:
+ TheoryProxy(PropEngine* propEngine,
+ TheoryEngine* theoryEngine,
+ context::Context* context,
+ CnfStream* cnfStream);
+
+ ~TheoryProxy();
+
+
+ void theoryCheck(theory::Theory::Effort effort);
+
+ void explainPropagation(SatLiteral l, SatClause& explanation);
+
+ void theoryPropagate(SatClause& output);
+
+ void enqueueTheoryLiteral(const SatLiteral& l);
+
+ SatLiteral getNextDecisionRequest();
+
+ bool theoryNeedCheck() const;
+
+ void removeClausesAboveLevel(int level);
+
+ /**
+ * Notifies of a new variable at a decision level.
+ */
+ void variableNotify(SatVariable var);
+
+ void unregisterVar(SatLiteral lit);
+
+ void renewVar(SatLiteral lit, int level = -1);
+
+ TNode getNode(SatLiteral lit);
+
+ void notifyRestart();
+
+ void notifyNewLemma(SatClause& lemma);
+
+ SatLiteral getNextReplayDecision();
+
+ void logDecision(SatLiteral lit);
+
+ void checkTime();
+
+};/* class SatSolver */
+
+/* Functions that delegate to the concrete SAT solver. */
+
+inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
+ TheoryEngine* theoryEngine,
+ context::Context* context,
+ CnfStream* cnfStream) :
+ d_propEngine(propEngine),
+ d_cnfStream(cnfStream),
+ d_theoryEngine(theoryEngine),
+ d_context(context)
+{}
+
+}/* CVC4::prop namespace */
+
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
+ out << lit.toString();
+ return out;
+}
+
+inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
+ out << "clause:";
+ for(unsigned i = 0; i < clause.size(); ++i) {
+ out << " " << clause[i];
+ }
+ out << ";";
+ return out;
+}
+
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+ std::string str;
+ switch(val) {
+ case prop::SatValUnknown:
+ str = "_";
+ break;
+ case prop::SatValTrue:
+ str = "1";
+ break;
+ case prop::SatValFalse:
+ str = "0";
+ break;
+ default:
+ str = "Error";
+ break;
+ }
+
+ out << str;
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROP__SAT_H */
projects / cvc5.git / commitdiff