summaryrefslogtreecommitdiff
path: root/src/prop/minisat
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat')
-rw-r--r--src/prop/minisat/core/Solver.cc32
-rw-r--r--src/prop/minisat/minisat.cpp16
-rw-r--r--src/prop/minisat/minisat.h3
3 files changed, 38 insertions, 13 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 411b89514..a682a893b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -232,6 +232,8 @@ CRef Solver::reason(Var x) {
vec<Lit> explanation;
MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+ Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+
// Sort the literals by trail index level
lemma_lt lt(*this);
sort(explanation, lt);
@@ -266,6 +268,12 @@ CRef Solver::reason(Var x) {
}
explanation.shrink(i - j);
+ Debug("pf::sat") << "Solver::reason: explanation = " ;
+ for (int i = 0; i < explanation.size(); ++i) {
+ Debug("pf::sat") << explanation[i] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
// We need an explanation clause so we add a fake literal
if (j == 1) {
// Add not TRUE to the clause
@@ -276,6 +284,7 @@ CRef Solver::reason(Var x) {
CRef real_reason = ca.alloc(explLevel, explanation, true);
// FIXME: at some point will need more information about where this explanation
// came from (ie. the theory/sharing)
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
ProofManager::getCnfProof()->registerConvertedClause(id, true);
// no need to pop current assertion as this is not converted to cnf
@@ -336,6 +345,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// If we are in solve or decision level > 0
if (minisat_busy || decisionLevel() > 0) {
+ Debug("pf::sat") << "Add clause adding a new lemma: ";
+ for (int k = 0; k < ps.size(); ++k) {
+ Debug("pf::sat") << ps[k] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
@@ -379,7 +394,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
cr = ca.alloc(clauseLevel, ps, false);
clauses_persistent.push(cr);
- attachClause(cr);
+ attachClause(cr);
if(PROOF_ON()) {
PROOF(
@@ -1234,12 +1249,12 @@ lbool Solver::search(int nof_conflicts)
} else {
- // If this was a final check, we are satisfiable
+ // If this was a final check, we are satisfiable
if (check_type == CHECK_FINAL) {
- bool decisionEngineDone = proxy->isDecisionEngineDone();
+ bool decisionEngineDone = proxy->isDecisionEngineDone();
// Unless a lemma has added more stuff to the queues
if (!decisionEngineDone &&
- (!order_heap.empty() || qhead < trail.size()) ) {
+ (!order_heap.empty() || qhead < trail.size()) ) {
check_type = CHECK_WITH_THEORY;
continue;
} else if (recheck) {
@@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() {
{
// The current lemma
vec<Lit>& lemma = lemmas[i];
+
+ Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
+ for (int k = 0; k < lemma.size(); ++k) {
+ Debug("pf::sat") << lemma[k] << " ";
+ }
+ Debug("pf::sat") << std::endl;
+
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
Assert (! PROOF_ON());
@@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() {
TNode cnf_assertion = lemmas_cnf_assertion[i].first;
TNode cnf_def = lemmas_cnf_assertion[i].second;
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() {
Node cnf_assertion = lemmas_cnf_assertion[i].first;
Node cnf_def = lemmas_cnf_assertion[i].second;
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bfbf9da6f..ff726e299 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
// FIXME: This relies on the invariant that when ok() is false
// the SAT solver does not add the clause (which is what Minisat currently does)
if (!ok()) {
- return ClauseIdUndef;
+ return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
PROOF( Assert (clause_id != ClauseIdError););
@@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() {
}
bool MinisatSatSolver::ok() const {
- return d_minisat->okay();
+ return d_minisat->okay();
}
void MinisatSatSolver::interrupt() {
@@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const
return true;
}
-void MinisatSatSolver::requirePhase(SatLiteral lit) {
+void MinisatSatSolver::requirePhase(SatLiteral lit) {
Assert(!d_minisat->rnd_pol);
Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl;
SatVariable v = lit.getSatVariable();
d_minisat->freezePolarity(v, lit.isNegated());
}
-bool MinisatSatSolver::flipDecision() {
+bool MinisatSatSolver::flipDecision() {
Debug("minisat") << "flipDecision()" << std::endl;
return d_minisat->flipDecision();
}
-bool MinisatSatSolver::isDecision(SatVariable decn) const {
- return d_minisat->isDecision( decn );
+bool MinisatSatSolver::isDecision(SatVariable decn) const {
+ return d_minisat->isDecision( decn );
}
/** Incremental interface */
@@ -291,7 +291,7 @@ namespace CVC4 {
template<>
prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
return prop::MinisatSatSolver::toSatLiteral(lit);
-}
+}
template<>
void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
@@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause&
}
} /* namespace CVC4 */
-
-
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 535ce1a47..ec5297bb7 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,6 +44,9 @@ public:
void initialize(context::Context* context, TheoryProxy* theoryProxy);
ClauseId addClause(SatClause& clause, bool removable);
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+ Unreachable("Minisat does not support native XOR reasoning");
+ }
SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
SatVariable trueVar() { return d_minisat->trueVar(); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback