summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cnf_stream.cpp75
-rw-r--r--src/prop/cnf_stream.h3
-rw-r--r--src/prop/minisat/core/Solver.cc49
-rw-r--r--src/prop/minisat/core/Solver.h6
-rw-r--r--src/prop/prop_engine.cpp48
-rw-r--r--src/prop/prop_engine.h20
-rw-r--r--src/prop/sat.h24
-rw-r--r--src/prop/sat_module.cpp3
-rw-r--r--src/prop/sat_module.h6
9 files changed, 217 insertions, 17 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9f49d81a2..396454fac 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f
d_registrar(registrar) {
}
-void CnfStream::recordTranslation(TNode node) {
+void CnfStream::recordTranslation(TNode node, bool alwaysRecord) {
+ Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl;
if (!d_removable) {
- d_translationTrail.push_back(stripNot(node));
+ node = stripNot(node);
+ if(d_translationCache.find(node)->second.recorded) {
+ Debug("cnf") << "--> Already recorded, not recording again." << std::endl;
+ } else {
+ Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl;
+ Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!");
+ d_translationTrail.push_back(node);
+ d_translationCache.find(node)->second.recorded = true;
+ d_translationCache.find(node.notNode())->second.recorded = true;
+ }
}
}
@@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const {
void TseitinCnfStream::ensureLiteral(TNode n) {
if(hasLiteral(n)) {
// Already a literal!
- SatLiteral lit = getLiteral(n);
+ // newLiteral() may be necessary to renew a previously-extant literal
+ SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true);
NodeCache::iterator i = d_nodeCache.find(lit);
if(i == d_nodeCache.end()) {
// Store backward-mappings
@@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
+ Assert(node.getKind() != kind::NOT);
// Get the literal for this node
SatLiteral lit;
if (!hasLiteral(node)) {
- // If no literal, well make one
+ // If no literal, we'll make one
lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
d_translationCache[node].literal = lit;
d_translationCache[node.notNode()].literal = ~lit;
@@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
// We will translate clauses, so remember the level
int level = d_satSolver->getAssertionLevel();
+ d_translationCache[node].recorded = false;
+ d_translationCache[node.notNode()].recorded = false;
d_translationCache[node].level = level;
d_translationCache[node.notNode()].level = level;
// If it's a theory literal, need to store it for back queries
if ( theoryLiteral || d_fullLitToNodeMap ||
( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
- Dump.isOn("clauses") ) {
+ (Dump.isOn("clauses")) ) {
d_nodeCache[lit] = node;
d_nodeCache[~lit] = node.notNode();
}
@@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
}
}
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(node, true);
+
return lit;
}
@@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
assertClause(xorNode, a, ~b, xorLit);
assertClause(xorNode, ~a, b, xorLit);
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(xorNode, true);
+
return xorLit;
}
@@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
// This needs to go last, as the clause might get modified by the SAT solver
assertClause(orNode, clause);
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(orNode, true);
+
// Return the literal
return orLit;
}
@@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
clause[n_children] = andLit;
// This needs to go last, as the clause might get modified by the SAT solver
assertClause(andNode, clause);
+
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(andNode, true);
+
return andLit;
}
@@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
assertClause(impliesNode, a, impliesLit);
assertClause(impliesNode, ~b, impliesLit);
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(impliesNode, true);
+
return impliesLit;
}
@@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
assertClause(iffNode, ~a, ~b, iffLit);
assertClause(iffNode, a, b, iffLit);
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(iffNode, true);
+
return iffLit;
}
@@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
assertClause(iteNode, iteLit, ~condLit, ~thenLit);
assertClause(iteNode, iteLit, condLit, ~elseLit);
+ // We have a literal, so it has to be recorded. The definitional clauses
+ // go away on user-pop, so this literal will have to be re-vivified if it's
+ // used subsequently.
+ recordTranslation(iteNode, true);
+
return iteLit;
}
@@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
// If the non-negated node has already been translated, get the translation
if(isTranslated(node)) {
+ Debug("cnf") << "toCNF(): already translated" << endl;
nodeLit = getLiteral(node);
} else {
// Handle each Boolean operator case
@@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
void CnfStream::removeClausesAboveLevel(int level) {
while (d_translationTrail.size() > 0) {
+ Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl;
TNode node = d_translationTrail.back();
+ // Get the translation information
+ TranslationInfo& infoPos = d_translationCache.find(node)->second;
+ // If the level of the node is less or equal to given we are done
+ if (infoPos.level >= 0 && infoPos.level <= level) {
+ Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl;
+ break;
+ }
Debug("cnf") << "Removing node " << node << " from CNF translation" << endl;
d_translationTrail.pop_back();
- // Get the translation informations
- TranslationInfo& infoPos = d_translationCache.find(node)->second;
// If already untranslated, we're done
if (infoPos.level == -1) continue;
- // If the level of the node is less or equal to given we are done
- if (infoPos.level <= level) break;
// Otherwise we have to undo the translation
undoTranslate(node, level);
}
@@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
// Untranslate
infoPos.level = -1;
+ infoPos.recorded = false;
// Untranslate the negation node
// If not a not node, unregister it from sat and untranslate the negation
@@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
Assert(it != d_translationCache.end());
TranslationInfo& infoNeg = (*it).second;
infoNeg.level = -1;
+ infoNeg.recorded = false;
}
// undoTranslate the children
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index c9306952b..4812c6a21 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -52,6 +52,7 @@ public:
/** Per node translation information */
struct TranslationInfo {
+ bool recorded;
/** The level at which this node was translated (negative if not translated) */
int level;
/** The literal of this node */
@@ -109,7 +110,7 @@ protected:
}
/** Record this translation */
- void recordTranslation(TNode node);
+ void recordTranslation(TNode node, bool alwaysRecord = false);
/**
* Moves the node and all of it's parents to level 0.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 3fe9db10c..678fe28dc 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -714,10 +714,11 @@ CRef Solver::propagate(TheoryCheckType type)
}
void Solver::propagateTheory() {
-
- SatClause propagatedLiteralsClause;
+ SatClause propagatedLiteralsClause;
+ // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
+ // is online. This just incorporates those propagations previously discovered.
proxy->theoryPropagate(propagatedLiteralsClause);
-
+
vec<Lit> propagatedLiterals;
DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
@@ -885,10 +886,22 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (c.level() > level) {
- Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl;
+ if(Debug.isOn("minisat")) {
+ Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":";
+ for(int i = 0; i < c.size(); ++i) {
+ Debug("minisat") << " " << c[i];
+ }
+ Debug("minisat") << std::endl;
+ }
removeClause(cs[i]);
} else {
- Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl;
+ if(Debug.isOn("minisat")) {
+ Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":";
+ for(int i = 0; i < c.size(); ++i) {
+ Debug("minisat") << " " << c[i];
+ }
+ Debug("minisat") << std::endl;
+ }
cs[j++] = cs[i];
}
}
@@ -1328,16 +1341,25 @@ void Solver::push()
Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
trail_user.push(lit_Undef);
trail_ok.push(ok);
+ trail_user_lim.push(trail.size());
+ assert(trail_user_lim.size() == assertionLevel);
+ Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
}
void Solver::pop()
{
assert(enable_incremental);
+ Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl;
popTrail();
+ Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl;
+
+ assert(decisionLevel() == 0);
+ assert(trail_user_lim.size() == assertionLevel);
--assertionLevel;
+ Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl;
Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl;
// Remove all the clauses asserted (and implied) above the new base level
@@ -1346,6 +1368,23 @@ void Solver::pop()
Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl;
+ int downto = trail_user_lim.last();
+ while(downto < trail.size()) {
+ Debug("minisat") << "== unassigning " << trail.last() << std::endl;
+ Var x = var(trail.last());
+ if(intro_level(x) != -1) {// might be unregistered
+ assigns [x] = l_Undef;
+ vardata[x].trail_index = -1;
+ polarity[x] = sign(trail.last());
+ insertVarOrder(x);
+ }
+ trail.pop();
+ }
+ qhead = trail.size();
+ Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl;
+ assert(trail_user_lim.last() == qhead);
+ trail_user_lim.pop();
+
// Unset any units learned or added at this level
Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl;
while(trail_user.last() != lit_Undef) {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 426268b4b..c0dd00166 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -191,6 +191,10 @@ public:
int nVars () const; // The current number of variables.
int nFreeVars () const;
+ // Debugging SMT explanations
+ //
+ bool properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l)
+
// Resource contraints:
//
void setConfBudget(int64_t x);
@@ -282,6 +286,7 @@ protected:
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
vec<Lit> trail_user; // Stack of assignments to UNdo on user pop.
+ vec<int> trail_user_lim; // Separator indices for different user levels in 'trail'.
vec<bool> trail_ok; // Stack of "whether we're in conflict" flags.
vec<VarData> vardata; // Stores reason and level for each variable.
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
@@ -462,6 +467,7 @@ inline int Solver::nClauses () const { return clauses_persisten
inline int Solver::nLearnts () const { return clauses_removable.size(); }
inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline bool Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
inline void Solver::setDecisionVar(Var v, bool b)
{
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7d0353122..2538e6d0c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -232,6 +232,10 @@ void PropEngine::pop() {
Debug("prop") << "pop()" << endl;
}
+bool PropEngine::isRunning() const {
+ return d_inCheckSat;
+}
+
void PropEngine::interrupt() throw(ModalException) {
if(! d_inCheckSat) {
throw ModalException("SAT solver is not currently solving anything; "
@@ -247,5 +251,49 @@ void PropEngine::spendResource() throw() {
// TODO implement me
}
+bool PropEngine::properExplanation(TNode node, TNode expl) const {
+ if(! d_cnfStream->hasLiteral(node)) {
+ Trace("properExplanation") << "properExplanation(): Failing because node "
+ << "being explained doesn't have a SAT literal ?!" << std::endl
+ << "properExplanation(): The node is: " << node << std::endl;
+ return false;
+ }
+
+ SatLiteral nodeLit = d_cnfStream->getLiteral(node);
+
+ for(TNode::kinded_iterator i = expl.begin(kind::AND),
+ i_end = expl.end(kind::AND);
+ i != i_end;
+ ++i) {
+ if(! d_cnfStream->hasLiteral(*i)) {
+ Trace("properExplanation") << "properExplanation(): Failing because one of explanation "
+ << "nodes doesn't have a SAT literal" << std::endl
+ << "properExplanation(): The explanation node is: " << *i << std::endl;
+ return false;
+ }
+
+ SatLiteral iLit = d_cnfStream->getLiteral(*i);
+
+ if(iLit == nodeLit) {
+ Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl
+ << "properExplanation(): " << node << std::endl
+ << "properExplanation(): cannot be made to explain itself!" << std::endl;
+ return false;
+ }
+
+ if(! d_satSolver->properExplanation(nodeLit, iLit)) {
+ Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl
+ << "properExplanation(): " << *i << std::endl
+ << "properExplanation(): is not part of a proper explanation node for" << std::endl
+ << "properExplanation(): " << node << std::endl
+ << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl
+ << "properExplanation(): node wasn't propagated before the node being explained" << std::endl;
+ return false;
+ }
+ }
+
+ return true;
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4f83888fc..91b9a61e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -242,6 +242,12 @@ public:
void pop();
/**
+ * Return true if we are currently searching (either in this or
+ * another thread).
+ */
+ bool isRunning() const;
+
+ /**
* Check the current time budget.
*/
void checkTime();
@@ -258,11 +264,23 @@ public:
*/
void spendResource() throw();
+ /**
+ * For debugging. Return true if "expl" is a well-formed
+ * explanation for "node," meaning:
+ *
+ * 1. expl is either a SAT literal or an AND of SAT literals
+ * currently assigned true;
+ * 2. node is assigned true;
+ * 3. node does not appear in expl; and
+ * 4. node was assigned after all of the literals in expl
+ */
+ bool properExplanation(TNode node, TNode expl) const;
+
};/* class PropEngine */
inline void SatTimer::check() {
- if(expired()) {
+ if(d_propEngine.isRunning() && expired()) {
Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
d_propEngine.interrupt();
}
diff --git a/src/prop/sat.h b/src/prop/sat.h
index a6bdcb309..14b42e445 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -49,6 +49,30 @@ class PropEngine;
class CnfStream;
/* Definitions of abstract types and conversion functions for SAT interface */
+/*
+inline SatLiteral variableToLiteral(SatVariable var) {
+ return Minisat::mkLit(var);
+}
+
+inline bool literalSign(SatLiteral lit) {
+ return Minisat::sign(lit);
+}
+
+static inline size_t
+hashSatLiteral(const SatLiteral& literal) {
+ return (size_t) Minisat::toInt(literal);
+}
+
+inline std::string stringOfLiteralValue(SatLiteralValue val) {
+ if( val == l_False ) {
+ return "0";
+ } else if (val == l_True ) {
+ return "1";
+ } else { // unknown
+ return "_";
+ }
+}
+*/
/**
* The proxy class that allows the SatSolver to communicate with the theories
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp
index 9391acbe5..db911f488 100644
--- a/src/prop/sat_module.cpp
+++ b/src/prop/sat_module.cpp
@@ -383,6 +383,9 @@ SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}
+bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+ return true;
+}
/** Incremental interface */
diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h
index 320dfe09b..9c49c7d67 100644
--- a/src/prop/sat_module.h
+++ b/src/prop/sat_module.h
@@ -152,6 +152,8 @@ public:
virtual void pop() = 0;
+ virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
+
};
// toodo add ifdef
@@ -179,11 +181,11 @@ public:
SatLiteralValue value(SatLiteral l);
SatLiteralValue modelValue(SatLiteral l);
-
void unregisterVar(SatLiteral lit);
void renewVar(SatLiteral lit, int level = -1);
int getAssertionLevel() const;
+
// helper methods for converting from the internal Minisat representation
static SatVariable toSatVariable(BVMinisat::Var var);
@@ -254,6 +256,8 @@ public:
SatLiteralValue modelValue(SatLiteral l);
+ bool properExplanation(SatLiteral lit, SatLiteral expl) const;
+
/** Incremental interface */
int getAssertionLevel() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback