/*****************************************************************************/
/*!
*\file minisat_solver.cpp
*\brief Adaptation of MiniSat to DPLL(T)
*
* Author: Alexander Fuchs
*
* Created: Fri Sep 08 11:04:00 2006
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*/
/*****************************************************************************/
/****************************************************************************************[Solver.C]
MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include "minisat_solver.h"
#include "minisat_types.h"
#include <cmath>
#include <iostream>
#include <algorithm>
using namespace std;
using namespace MiniSat;
///
/// Constants
///
// if true do propositional propagation to exhaustion
// before asserting propagated literals to the theories.
// that is, a SAT propagation is not immediately asserted to the theories as well,
// but only when the SAT core has to do a decision.
//
// this way a branch may be closed propositionally only,
// which avoids work on the theory part,
// and introduction of new theory clauses and implications.
const bool defer_theory_propagation = true;
/// theory implications
// retrieve explanations of theory implications eagerly
// and store them right away as clauses
const bool eager_explanation = true;
// if explanations for theory implications are retrieved lazily
// during regressions, should they be added as clauses?
//
// only used if eager_explanation is false.
const bool keep_lazy_explanation = true;
/// pushes
// determines which theory operations are done,
// when unit propagation is done to exhaustion at the root level
// because a push is done.
// if true then assert propositional propagations to theories as well
// (this is done anyway when defer_theory_propagation is false)
const bool push_theory_propagation = true;
// if push_theory_propagation is also true,
// retrieve and propagate theory implications as well
const bool push_theory_implication = true;
// if push_theory_propagation is also true,
// retrieve and add theory clauses as well (and handle their propagations)
const bool push_theory_clause = true;
// the number of literals considered in propLookahead()
const vector<Var>::size_type prop_lookahead = 1;
// print the derivation
const bool protocol = false;
// perform expensive assertion checks
const bool debug_full = false;
///
/// conversions between MiniSat and CVC data types:
///
bool MiniSat::cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals) {
// register all clause literals
SAT::Clause::const_iterator j, jend;
for (j = clause.begin(), jend = clause.end(); j != jend; ++j) {
const SAT::Lit& literal = *j;
// simplify based on true/false literals
if (literal.isTrue())
return false;
if (!literal.isFalse())
literals.push_back(cvcToMiniSat(literal));
}
return true;
}
Clause* MiniSat::cvcToMiniSat(const SAT::Clause& clause, int id) {
vector<MiniSat::Lit> literals;
if (cvcToMiniSat(clause, literals)) {
return Clause_new(literals, id);
}
else {
return NULL;
}
}
/// Initialization
Solver::Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider) :
d_inSearch(false),
d_ok(true),
d_conflict(NULL),
d_qhead (0),
d_thead (0),
d_registeredVars (1),
d_clauseIDCounter (3), // -1 and -2 are used in Clause for special clauses,
// and negative ids are in general used for theory clauses,
// so avoid overlap by setting 3 as the possible first clause id.
d_popRequests (0),
d_cla_inc (1),
d_cla_decay (1),
d_var_inc (1),
d_var_decay (1),
d_order (d_assigns, d_activity),
d_simpDB_assigns (0),
d_simpDB_props (0),
d_simpRD_learnts (0),
d_theoryAPI(theoryAPI),
d_decider(decider),
d_derivation(NULL/*new Derivation()*/),
d_default_params(SearchParams(0.95, 0.999, 0.02)),
d_expensive_ccmin(true)
{ }
// add a lemma which has not been computed just now (see push(), createFrom()),
// so it is not necessary propagating
void Solver::insertLemma(const Clause* lemma, int clauseID, int pushID) {
// need to add lemmas manually,
// as addClause/insertClause assume that the lemma has just been computed and is propagating,
// and as we want to keep the activity.
vector<Lit> literals;
lemma->toLit(literals);
// just ignore lemma if already satisfied by clauses
if (!simplifyClause(literals, clauseID)) {
// ensure that order is appropriate for watched literals
orderClause(literals);
Clause* newLemma = Lemma_new(literals, clauseID, pushID);
newLemma->activity() = lemma->activity();
// add to watches and lemmas
if (newLemma->size() >= 2) {
addWatch(~(*newLemma)[0], newLemma);
addWatch(~(*newLemma)[1], newLemma);
}
d_learnts.push_back(newLemma);
d_stats.learnts_literals += newLemma->size();
// unsatisfiable
if (newLemma->size() == 0 || getValue((*newLemma)[0]) == l_False) {
updateConflict(newLemma);
}
// propagate
if (newLemma->size() == 1 || getValue((*newLemma)[1]) == l_False) {
if (!enqueue((*newLemma)[0], d_rootLevel, newLemma)) {
DebugAssert(false, "MiniSat::Solver::insertLemma: conflicting/implying lemma");
}
}
}
}
Solver* Solver::createFrom(const Solver* oldSolver) {
Solver* solver = new MiniSat::Solver(oldSolver->d_theoryAPI, oldSolver->d_decider);
// reuse literal activity
// assigning d_activity before the clauses are added
// will automatically rebuild d_order in the right way.
solver->d_cla_inc = oldSolver->d_cla_inc;
solver->d_var_inc = oldSolver->d_var_inc;
solver->d_activity = oldSolver->d_activity;
// build the current formula
// add the formula and assignment from the previous solver
// first assignment, as this contains only unit clauses, then clauses,
// as these are immediately simplified by the assigned unit clauses
// get the old assignment
const vector<MiniSat::Lit>& trail = oldSolver->getTrail();
for (vector<MiniSat::Lit>::const_iterator i = trail.begin(); i != trail.end(); ++i) {
solver->addClause(*i);
}
// get the old clause set
const vector<MiniSat::Clause*>& clauses = oldSolver->getClauses();
for (vector<MiniSat::Clause*>::const_iterator i = clauses.begin(); i != clauses.end(); ++i) {
solver->addClause(**i, false);
}
// get the old lemmas
const vector<MiniSat::Clause*>& lemmas = oldSolver->getLemmas();
for (vector<MiniSat::Clause*>::const_iterator i = lemmas.begin();
!solver->isConflicting() && i != lemmas.end(); ++i) {
// can use clauseID for clause id as well as push id -
// after all this is the root level, so all lemmas are ok in any push level anyway
int clauseID = solver->nextClauseID();
solver->insertLemma(*i, clauseID, clauseID);
}
return solver;
}
Solver::~Solver() {
for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); ++i)
remove(*i, true);
for (vector<Clause*>::const_iterator i = d_clauses.begin(); i != d_clauses.end(); ++i)
remove(*i, true);
while (!d_pendingClauses.empty()) {
xfree(d_pendingClauses.front());
d_pendingClauses.pop();
}
while (!d_theoryExplanations.empty()) {
xfree(d_theoryExplanations.top().second);
d_theoryExplanations.pop();
}
delete d_derivation;
}
///
/// String representation
//
std::string Solver::toString(Lit literal, bool showAssignment) const {
ostringstream buffer;
buffer << literal.toString();
if (showAssignment) {
if (getValue(literal) == l_True)
buffer << "(+)";
else if (getValue(literal) == l_False)
buffer << "(-)";
}
return buffer.str();
}
std::string Solver::toString(const std::vector<Lit>& clause, bool showAssignment) const {
ostringstream buffer;
for (size_type j = 0; j < clause.size(); ++j) {
buffer << toString(clause[j], showAssignment) << " ";
}
buffer << endl;
return buffer.str();
}
std::string Solver::toString(const Clause& clause, bool showAssignment) const {
std::vector<Lit> literals;
clause.toLit(literals);
return toString(literals, showAssignment);
}
void Solver::printState() const {
cout << "Lemmas: " << endl;
for (size_type i = 0; i < d_learnts.size(); ++i) {
cout << toString(*(d_learnts[i]), true);
}
cout << endl;
cout << "Clauses: " << endl;
for (size_type i = 0; i < d_clauses.size(); ++i) {
cout << toString(*(d_clauses[i]), true);
}
cout << endl;
cout << "Assignment: " << endl;
for (size_type i = 0; i < d_qhead; ++i) {
string split = "";
if (getReason(d_trail[i].var()) == Clause::Decision()) {
split = "(S)";
}
cout << toString(d_trail[i], false) << split << " ";
}
cout << endl;
}
void Solver::printDIMACS() const {
int max_id = nVars();
int num_clauses = d_clauses.size() + d_trail.size();// + learnts.size() ;
// header
cout << "c minisat test" << endl;
cout << "p cnf " << max_id << " " << num_clauses << endl;
// clauses
for (size_type i = 0; i < d_clauses.size(); ++i) {
Clause& clause = *d_clauses[i];
for (int j = 0; j < clause.size(); ++j) {
Lit lit = clause[j];
cout << toString(lit, false) << " ";
}
cout << "0" << endl;
}
// lemmas
//for (int i = 0; i < learnts.size(); ++i) {
// Clause& clause = *learnts[i];
// for (int j = 0; j < clause.size(); ++j) {
// Lit lit = clause[j];
// cout << toString(lit, false) << " ";
// }
// cout << "0" << endl;
//}
// context
for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
Lit lit(*i);
if (getReason(lit.var()) == Clause::Decision())
cout << toString(lit, false) << " 0" << endl;
else
cout << toString(lit, false) << " 0" << endl;
}
}
/// Operations on clauses:
bool Solver::isRegistered(Var var) {
for (vector<Hash::hash_set<Var> >::const_iterator i = d_registeredVars.begin();
i != d_registeredVars.end(); ++i) {
if ((*i).count(var) > 0) return true;
}
return false;
}
// registers var with given index to all data structures
void Solver::registerVar(Var index) {
if (isRegistered(index)) return;
if (nVars() <= index) {
// 2 * index + 1 will be accessed for neg. literal,
// so we need + 1 fiels for 0 field
d_watches .resize(2 * index + 2);
d_reason .resize(index + 1, NULL);
d_assigns .resize(index + 1, toInt(l_Undef));
d_level .resize(index + 1, -1);
d_activity .resize(index + 1, 0);
d_analyze_seen.resize(index + 1, 0);
d_pushIDs .resize(index + 1, -1);
d_order .newVar(index);
if (d_derivation != NULL) d_trail_pos.resize(index + 1, d_trail.max_size());
}
DebugAssert(!d_registeredVars.empty(), "MiniSat::Solver::registerVar: d_registeredVars is empty");
d_registeredVars.back().insert(index);
}
void Solver::addClause(Lit p) {
vector<Lit> literals;
literals.push_back(p);
addClause(literals, nextClauseID());
}
void Solver::addClause(const SAT::Clause& clause, bool isTheoryClause) {
vector<MiniSat::Lit> literals;
if (cvcToMiniSat(clause, literals)) {
int clauseID = nextClauseID();
// theory clauses have negative ids:
if (isTheoryClause) clauseID = -clauseID;
if (getDerivation() != NULL) getDerivation()->registerInputClause(clauseID);
addClause(literals, clauseID);
}
else {
// ignore tautologies
return;
}
}
void Solver::addClause(const Clause& clause, bool keepClauseID) {
vector<Lit> literals;
for (int i = 0; i < clause.size(); ++i) {
literals.push_back(clause[i]);
}
if (keepClauseID) {
addClause(literals, clause.id());
} else {
addClause(literals, nextClauseID());
}
}
// Note:
// tried to improve efficiency by asserting unit clauses first,
// then clauses of size 2, and so on,
// in the hope to immediately simplify or remove clauses.
//
// didn't work well with the theories, though,
// lead to significant overhead, even when the derivation did not change much.
// presumably as this interleaves clauses belonging to different 'groups',
// which describe different concepts and are better handled in sequence
// without interleaving them.
void Solver::addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause) {
SAT::CNF_Formula::const_iterator i, iend;
// for comparison: this is the order used by xchaff
//for (i = cnf.end()-1, iend = cnf.begin()-1; i != iend; --i) {
for (i = cnf.begin(), iend = cnf.end(); i != iend; i++) {
addClause(*i, isTheoryClause);
}
}
// based on root level assignment removes all permanently falsified literals.
// return true if clause is permanently satisfied.
bool Solver::simplifyClause(vector<Lit>& literals, int clausePushID) const {
// Check if clause is a tautology: p \/ -p \/ C:
for (size_type i = 1; i < literals.size(); i++){
if (literals[i-1] == ~literals[i])
return true;
}
// Remove permanently satisfied clauses and falsified literals:
size_type i, j;
for (i = j = 0; i < literals.size(); i++) {
bool rootAssign =
getLevel(literals[i]) == d_rootLevel
&& isImpliedAt(literals[i], clausePushID);
if (rootAssign && (getValue(literals[i]) == l_True))
return true;
else if (rootAssign && (getValue(literals[i]) == l_False))
;
else
literals[j++] = literals[i];
}
literals.resize(j);
return false;
}
// need the invariant, that
// a) either two undefined literals are chosen as watched literals,
// or b) that after backtracking either a) kicks in
// or the clause is still satisfied/unit
//
// so either:
// - find two literals which are undefined or satisfied
// - or find a literal that is satisfied or unsatisfied
// and the most recently falsified literal
// - or the two most recently falsified literals
// and put these two literals at the first two positions
void Solver::orderClause(vector<Lit>& literals) const {
if (literals.size() >= 2) {
int first = 0;
int levelFirst = getLevel(literals[first]);
lbool valueFirst = getValue(literals[first]);
int second = 1;
int levelSecond = getLevel(literals[second]);
lbool valueSecond = getValue(literals[second]);
for (size_type i = 2; i < literals.size(); i++) {
// found two watched or satisfied literals
if (!(valueFirst == l_False) && !(valueSecond == l_False))
break;
// check if new literal is better than the currently picked ones
int levelNew = getLevel(literals[i]);
lbool valueNew = getValue(literals[i]);
// usable, take instead of previously chosen literal
if (!(valueNew == l_False)) {
if ((valueFirst == l_False) && (valueSecond == l_False)) {
if (levelFirst > levelSecond) {
second = i; levelSecond = levelNew; valueSecond = valueNew;
} else {
first = i; levelFirst = levelNew; valueFirst = valueNew;
}
}
else if (valueFirst == l_False) {
first = i; levelFirst = levelNew; valueFirst = valueNew;
}
else {
second = i; levelSecond = levelNew; valueSecond = valueNew;
}
}
// check if new pick was falsified more recently than the others
else {
if ((valueFirst == l_False) && (valueSecond == l_False)) {
if ((levelNew > levelFirst) && (levelNew > levelSecond)) {
if (levelSecond > levelFirst) {
first = i; levelFirst = levelNew; valueFirst = valueNew;
}
else {
second = i; levelSecond = levelNew; valueSecond = valueNew;
}
}
else if (levelNew > levelFirst) {
first = i; levelFirst = levelNew; valueFirst = valueNew;
}
else if (levelNew > levelSecond) {
second = i; levelSecond = levelNew; valueSecond = valueNew;
}
}
else if (valueFirst == l_False) {
if (levelNew > levelFirst) {
first = i; levelFirst = levelNew; valueFirst = valueNew;
}
}
else { // valueSecond == l_false
if (levelNew > levelSecond) {
second = i; levelSecond = levelNew; valueSecond = valueNew;
}
}
}
}
Lit swap = literals[0]; literals[0] = literals[first]; literals[first] = swap;
swap = literals[1]; literals[1] = literals[second]; literals[second] = swap;
// if a literal is satisfied, the first literal is satisfied,
// otherwise if a literal is falsified, the second literal is falsified.
if (
// satisfied literal at first position
((getValue(literals[0]) != l_True) && (getValue(literals[1]) == l_True))
||
// falsified literal at second position
(getValue(literals[0]) == l_False)
)
{
Lit swap = literals[0]; literals[0] = literals[1]; literals[1] = swap;
}
}
}
void Solver::addClause(vector<Lit>& literals, int clauseID) {
// sort clause
std::sort(literals.begin(), literals.end());
// remove duplicates
vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
literals.erase(end, literals.end());
// register var for each clause literal
for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
registerVar(i->var());
}
// simplify clause
vector<Lit> simplified(literals);
bool replaceReason = false;
if (simplifyClause(simplified, clauseID)) {
// it can happen that a unit clause was contradictory when it was added (in a non-root state).
// then it was first added to list of pending clauses,
// and the conflict analyzed and retracted:
// this lead to the computation of a lemma which was used as a reason for the literal
// instead of the unit clause itself.
// so fix this here
if (literals.size() == 1 && getReason(literals[0].var())->learnt()) {
replaceReason = true;
}
else {
// permanently satisfied clause
return;
}
}
// record derivation for a simplified clause
if (getDerivation() != NULL && simplified.size() < literals.size()) {
// register original clause as start of simplification
Clause* c = Clause_new(literals, clauseID);
getDerivation()->registerClause(c);
getDerivation()->removedClause(c);
// register simplification steps
Inference* inference = new Inference(clauseID);
size_type j = 0;
for (size_type i = 0; i < literals.size(); ++i) {
// literal removed in simplification
if (j >= simplified.size() || literals[i] != simplified[j]) {
inference->add(literals[i], getDerivation()->computeRootReason(~literals[i], this));
}
// keep literal
else {
++j;
}
}
// register resolution leading to simplified clause
clauseID = nextClauseID();
getDerivation()->registerInference(clauseID, inference);
}
// insert simplified clause
orderClause(simplified);
Clause* c = Clause_new(simplified, clauseID);
insertClause(c);
if (replaceReason) {
d_reason[literals[0].var()] = c;
}
}
void Solver::insertClause(Clause* c) {
// clause set is unsatisfiable
if (!d_ok) {
remove(c, true);
return;
}
if (getDerivation() != NULL) getDerivation()->registerClause(c);
if (c->size() == 0){
d_conflict = c;
// for garbage collection: need to put clause somewhere
if (!c->learnt()) {
d_clauses.push_back(c);
} else {
d_learnts.push_back(c);
}
d_ok = false;
return;
}
// process clause -
// if clause is conflicting add it to pending clause and return
// unit clause
if (c->size() == 1) {
if (!enqueue((*c)[0], d_rootLevel, c)) {
// this backtracks to d_rootLevel, as reason c is just one literal,
// which is immediately UIP, so c will be learned as a lemma as well.
updateConflict(c);
d_pendingClauses.push(c);
return;
}
}
// non-unit clause
else {
// ensure that for a lemma the second literal has the highest decision level
if (c->learnt()){
DebugAssert(getValue((*c)[0]) == l_Undef,
"MiniSat::Solver::insertClause: first literal of new lemma not undefined");
IF_DEBUG (
for (int i = 1; i < c->size(); ++i) {
DebugAssert(getValue((*c)[i]) == l_False,
"MiniSat::Solver::insertClause: lemma literal not false");
}
)
// Put the second watch on the literal with highest decision level:
int max_i = 1;
int max = getLevel((*c)[1]);
for (int i = 2; i < c->size(); i++) {
if (getLevel((*c)[i]) > max) {
max = getLevel((*c)[i]);
max_i = i;
}
}
Lit swap((*c)[1]);
(*c)[1] = (*c)[max_i];
(*c)[max_i] = swap;
// (newly learnt clauses should be considered active)
claBumpActivity(c);
}
// satisfied
if (getValue((*c)[0]) == l_True) {
;
}
// conflicting
else if (getValue((*c)[0]) == l_False) {
IF_DEBUG (
for (int i = 1; i < c->size(); ++i) {
DebugAssert(getValue((*c)[i]) == l_False,
"MiniSat::Solver::insertClause: bogus conflicting clause");
}
)
updateConflict(c);
d_pendingClauses.push(c);
return;
}
// propagation
else if (getValue((*c)[1]) == l_False) {
DebugAssert(getValue((*c)[0]) == l_Undef,
"MiniSat::Solver::insertClause: bogus propagating clause");
IF_DEBUG (
for (int i = 1; i < c->size(); ++i) {
DebugAssert(getValue((*c)[i]) == l_False,
"MiniSat::Solver::insertClause: bogus propagating clause");
}
)
if (!enqueue((*c)[0], getImplicationLevel(*c), c)) {
DebugAssert(false, "MiniSat::Solver::insertClause: conflicting/implying clause");
}
}
// Watch clause:
addWatch(~(*c)[0], c);
addWatch(~(*c)[1], c);
}
// clause is not conflicting, so insert it into the clause list.
d_stats.max_literals += c->size();
if (!c->learnt()) {
d_clauses.push_back(c);
d_stats.clauses_literals += c->size();
} else {
d_learnts.push_back(c);
d_stats.learnts_literals += c->size();
}
}
// Disposes a clauses and removes it from watcher lists.
// NOTE! Low-level; does NOT change the 'clauses' and 'learnts' vector.
void Solver::remove(Clause* c, bool just_dealloc) {
// no watches added for clauses of size < 2
if (!just_dealloc && c->size() >= 2){
removeWatch(getWatches(~(*c)[0]), c);
removeWatch(getWatches(~(*c)[1]), c);
}
if (c->learnt()) d_stats.learnts_literals -= c->size();
else d_stats.clauses_literals -= c->size();
if (getDerivation() == NULL) xfree(c);
else getDerivation()->removedClause(c);
}
/// Conflict handling
// Pre-condition: 'elem' must exists in 'ws' OR 'ws' must be empty.
void Solver::removeWatch(std::vector<Clause*>& ws, Clause* elem) {
if (ws.size() == 0) return; // (skip lists that are already cleared)
size_type j = 0;
for (; ws[j] != elem; j++) {
// want to find the right j, so the loop should be executed
// and not wrapped in a debug guard
DebugAssert(j < ws.size(), "MiniSat::Solver::removeWatch: elem not in watched list");
}
ws[j] = ws.back();
ws.pop_back();
}
// for a clause, of which the first literal is implied,
// get the highest decision level of the implying literals,
// i.e. the decision level from which on the literal is implied
//
// as theory clauses can be added at any time,
// this is not necessarily the level of the second literal.
// thus, all literals have to be checked.
int Solver::getImplicationLevel(const Clause& clause) const {
int currentLevel = decisionLevel();
int maxLevel = d_rootLevel;
for (int i = 1; i < clause.size(); ++i) {
DebugAssert(getValue(clause[i]) == l_False,
"MiniSat::Solver::getImplicationLevelFull: literal not false");
int newLevel = getLevel(clause[i]);
// highest possible level
if (newLevel == currentLevel)
return currentLevel;
// highest level up to now
if (newLevel > maxLevel)
maxLevel = newLevel;
}
return maxLevel;
}
// like getImplicationLevel, but for all literals,
// i.e. for conflicting instead of propagating clause
int Solver::getConflictLevel(const Clause& clause) const {
int decisionLevel = d_rootLevel;
for (int i = 0; i < clause.size(); ++i) {
DebugAssert(getValue(clause[i]) == l_False, "MiniSat::Solver::getConflictLevel: literal not false");
int newLevel = getLevel(clause[i]);
if (newLevel > decisionLevel)
decisionLevel = newLevel;
}
return decisionLevel;
}
Clause* Solver::getReason(Lit literal, bool _resolveTheoryImplication) {
Var var = literal.var();
Clause* reason = d_reason[var];
if (!_resolveTheoryImplication)
return reason;
DebugAssert(reason != NULL, "MiniSat::getReason: reason[var] == NULL.");
if (reason == Clause::TheoryImplication()) {
if (getValue(literal) == l_True)
resolveTheoryImplication(literal);
else
resolveTheoryImplication(~literal);
reason = d_reason[var];
}
DebugAssert(d_reason[var] != Clause::TheoryImplication(),
"MiniSat::getReason: reason[var] == TheoryImplication.");
return reason;
}
bool Solver::isConflicting() const {
return (d_conflict != NULL);
}
void Solver::updateConflict(Clause* clause) {
DebugAssert(clause != NULL, "MiniSat::updateConflict: clause == NULL.");
IF_DEBUG (
for (int i = 0; i < clause->size(); ++i) {
DebugAssert(getValue((*clause)[i]) == l_False, "MiniSat::Solver::updateConflict: literal not false");
}
)
if (
(d_conflict == NULL)
||
(clause->size() < d_conflict->size())
) {
d_conflict = clause;
}
}
// retrieve the explanation and update the implication level of a theory implied literal.
// if necessary, do this recursively (bottom up) for the literals in the explanation.
// assumes that the literal is true in the current context
void Solver::resolveTheoryImplication(Lit literal) {
if (eager_explanation) return;
if (d_reason[literal.var()] == Clause::TheoryImplication()) {
// instead of recursion put the theory implications to check in toRegress,
// and the theory implications depending on them in toComplete
stack<Lit> toRegress;
stack<Clause*> toComplete;
toRegress.push(literal);
SAT::Clause clauseCVC;
while (!toRegress.empty()) {
// get the explanation for the first theory implication
literal = toRegress.top();
DebugAssert(getValue(literal) == l_True,
"MiniSat::Solver::resolveTheoryImplication: literal is not true");
toRegress.pop();
d_theoryAPI->getExplanation(miniSatToCVC(literal), clauseCVC);
Clause* explanation = cvcToMiniSat(clauseCVC, nextClauseID());
// must ensure that propagated literal is at first position
for (int i = 0; i < (*explanation).size(); ++i) {
if ((*explanation)[i] == literal) {
MiniSat::Lit swap = (*explanation)[0];
(*explanation)[0] = (*explanation)[i];
(*explanation)[i] = swap;
break;
}
}
// assert that clause is implying the first literal
IF_DEBUG(
DebugAssert((*explanation)[0] == literal,
"MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 1");
DebugAssert(getValue((*explanation)[0]) == l_True,
"MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 2");
for (int i = 1; i < (*explanation).size(); ++i) {
DebugAssert(getValue((*explanation)[i]) == l_False,
"MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 3");
}
)
d_reason[literal.var()] = explanation;
// if any of the reasons is also a theory implication,
// then need to know its level first, so add it to toRegress
for (int i = 1; i < (*explanation).size(); ++i) {
if (d_reason[(*explanation)[i].var()] == Clause::TheoryImplication()) {
toRegress.push((*explanation)[i]);
}
}
// set literal and its explanation aside for later processing
toComplete.push(explanation);
}
// now set the real implication levels after they have been resolved
// std::pair<Lit, Clause*> pair;
while (!toComplete.empty()) {
Clause* explanation = toComplete.top();
toComplete.pop();
IF_DEBUG (
for (int i = 1; i < explanation->size(); ++i) {
DebugAssert (d_reason[(*explanation)[i].var()] != Clause::TheoryImplication(),
"MiniSat::Solver::resolveTheoryImplication: not done to completion");
}
)
// update propagation information
int level = getImplicationLevel(*explanation);
setLevel((*explanation)[0], level);
setPushID((*explanation)[0].var(), explanation);
if (keep_lazy_explanation) {
// the reason can be added to the clause set without any effect,
// as the explanation implies the first literal, which is currently true
// so neither propagation nor conflict are triggered,
// only the correct literals are registered as watched literals.
addClause(*explanation, true);
xfree(explanation);
} else {
// store explanation for later deallocation
d_theoryExplanations.push(std::make_pair(level, explanation));
}
}
}
}
/// Conflict handling
Clause* Solver::analyze(int& out_btlevel) {
DebugAssert(d_conflict != NULL, "MiniSat::Solver::analyze called when no conflict was detected");
// compute the correct decision level for theory propagated literals
//
// need to find the most recent implication level of any of the literals in d_conflict,
// after updating conflict levels due to lazy retrieval of theory implications.
//
// that is, really need to do:
// 1) assume that the currently highest known level is the UIP Level,
// initially this is the decision level
// 2) find a literal in the conflict clause whose real implication level is the UIP Level
// 3) if their is no such literal, pick the new UIP level as the highest of their implication levels,
// and repeat
//
// unfortunately, 2) is not that easy:
// - if the literals' level is smaller than the UIP level the literal can be ignored
// - otherwise, it might depend on theory implications,
// who have just been assumed to be of the UIP level, but which in reality are of lower levels.
// So, must check all literals the literal depends on,
// until the real level of all of them is determined,
// and thus also of the literal we are really interested in.
// this can be stopped if the level must be lower than the (currently assumed) UIP level,
// or if it is sure that the literal really has the UIP level.
// but this is only the case if it depends on the decision literal of the UIP level.
//
// but how to find this out efficiently?
//
// so, this is done as an approximation instead:
// 1) if the explanation of a (conflict clause) literal is known, stop and take the literal's level
// 2) otherwise, retrieve its explanation,
// and do 1) and 2) on each literal in the explanation.
// then set the original literal's level to the highest level of its explanation.
//
// as an example, if we have:
// - theory implication A in level n
// - propositional implication B depending on A and literals below level n
// - propositional implication C depending on B and literals below level n
// then A, B, C will all be assumed to be of level n,
// and if C is in a conflict it will be assumed to be of level n
// in the conflict analysis
//
// this is fast to compute,
// but it is not clear if starting from the real UIP level
// would lead to a significantly better lemma
for (int j = 0; j < d_conflict->size(); j++){
resolveTheoryImplication(~((*d_conflict)[j]));
}
int UIPLevel = getConflictLevel(*d_conflict);
// clause literals to regress are marked by setting analyze_d_seen[var]
// seen should be false for all variables
IF_DEBUG (
for (size_type i = 0; i < d_analyze_seen.size(); ++i) {
DebugAssert (d_analyze_seen[i] == 0, "MiniSat::Solver::analyze: analyze_seen is not clear at: " /*+ i*/);
}
)
// index into trail, regression is done chronologically (in combination with analyze_seen)
int index = d_trail.size() - 1;
// lemma is generated here;
vector<Lit> out_learnt;
// number of literals to regress in current decision level
int pathC = 0;
// highest level below UIP level, i.e. the level to backtrack to
out_btlevel = 0;
// current literal to regress
Lit p = lit_Undef;
// derivation logging
Inference* inference = NULL;
if (getDerivation() != NULL) inference = new Inference(d_conflict->id());
// conflict clause is the initial clause to regress
Clause* confl = d_conflict;
d_conflict = NULL;
// compute pushID as max pushID of all regressed clauses
int pushID = confl->pushID();
// leave room for the asserting literal
if (UIPLevel != d_rootLevel) out_learnt.push_back(lit_Undef);
// do until pathC == 1, i.e. UIP found
if (confl->size() == 1) {
p = ~(*confl)[0];
} else do {
DebugAssert (confl != Clause::Decision(), "MiniSat::Solver::analyze: no reason for conflict");
DebugAssert (confl != Clause::TheoryImplication(), "MiniSat::Solver::analyze: theory implication not resolved");
if (confl->learnt()) claBumpActivity(confl);
// regress p
for (int j = (p == lit_Undef) ? 0 : 1; j < confl->size(); j++){
Lit q = (*confl)[j];
DebugAssert(getValue(q) == l_False, "MiniSat::Solver::analyze: literal to regress is not false");
DebugAssert(getLevel(q) <= UIPLevel, "MiniSat::Solver::analyze: literal above UIP level");
// get explanation and compute implication level for theory implication
resolveTheoryImplication(~q);
// first time that q is in a reason, so process it
if (!d_analyze_seen[q.var()]) {
// q is falsified at root level, so it can be dropped
if (getLevel(q) == d_rootLevel) {
d_analyze_redundant.push_back(q);
d_analyze_seen[q.var()] = 1;
}
else {
varBumpActivity(q);
d_analyze_seen[q.var()] = 1;
// mark q to regress
if (getLevel(q) == UIPLevel)
pathC++;
// add q to lemma
else{
out_learnt.push_back(q);
out_btlevel = max(out_btlevel, getLevel(q));
}
}
}
}
// for clause conflicting at root level pathC can be 0 right away
if (pathC == 0) break;
// pick next literal in UIP level to regress.
// as trail is not ordered wrt. implication level (theory clause/ implications),
// check also if the next literal is really from the UIP level.
while (!d_analyze_seen[d_trail[index].var()] || (getLevel(d_trail[index])) != UIPLevel) {
--index;
}
--index;
// this could theoretically happen if UIP Level is 0,
// but should be catched as then the conflict clause
// is simplified to the empty clause.
DebugAssert(index >= -1, "MiniSat::Solver::analyze: index out of bound");
// set up p to be regressed
p = d_trail[index+1];
d_analyze_seen[p.var()] = 0;
pathC--;
confl = getReason(p);
pushID = max(pushID, confl->pushID());
if (getDerivation() != NULL && pathC > 0) inference->add(~p, confl);
} while (pathC > 0);
if (UIPLevel != d_rootLevel) out_learnt[0] = ~p;
// check that the UIP has been found
IF_DEBUG (
DebugAssert ((out_learnt.size() == 0 && UIPLevel == d_rootLevel)
|| getLevel(out_learnt[0]) == UIPLevel,
"MiniSat::Solver::analyze: backtracked past UIP level.");
for (size_type i = 1; i < out_learnt.size(); ++i) {
DebugAssert (getLevel(out_learnt[i]) < UIPLevel,
"MiniSat::Solver::analyze: conflict clause contains literal from UIP level or higher.");
}
)
analyze_minimize(out_learnt, inference, pushID);
// clear seen for lemma
for (vector<Lit>::const_iterator j = out_learnt.begin(); j != out_learnt.end(); ++j) {
d_analyze_seen[j->var()] = 0;
}
// finish logging of conflict clause generation
int clauseID = nextClauseID();
if (getDerivation() != NULL) getDerivation()->registerInference(clauseID, inference);
return Lemma_new(out_learnt, clauseID, pushID);
}
class lastToFirst_lt { // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
const vector<MiniSat::size_type>& d_trail_pos;
public:
lastToFirst_lt(const vector<MiniSat::size_type>& trail_pos) : d_trail_pos(trail_pos) {}
bool operator () (Lit p, Lit q) {
return d_trail_pos[p.var()] > d_trail_pos[q.var()];
}
};
void Solver::analyze_minimize(vector<Lit>& out_learnt, Inference* inference, int& pushID) {
// for empty clause current analyze_minimize will actually do something wrong
if (out_learnt.size() > 1) {
// literals removed from out_learnt in conflict clause minimization,
// including reason literals which had to be removed as well
// (except for literals implied at root level).
size_type i, j;
// 1) Simplify conflict clause (a lot):
// drop a literal if it is implied by the remaining lemma literals:
// that is, as in 2), but also recursively taking the reasons
// for the implying clause, and their reasone, and so on into consideration.
if (d_expensive_ccmin){
// (maintain an abstraction of levels involved in conflict)
uint min_level = 0;
for (i = 1; i < out_learnt.size(); i++)
min_level |= 1 << (getLevel(out_learnt[i]) & 31);
for (i = j = 1; i < out_learnt.size(); i++) {
Lit lit(out_learnt[i]);
if (getReason(lit) == Clause::Decision() || !analyze_removable(lit, min_level, pushID))
out_learnt[j++] = lit;
}
}
// 2) Simplify conflict clause (a little):
// drop a literal if it is implied by the remaining lemma literals:
// that is, if the other literals of its implying clause
// are falsified by the other lemma literals.
else {
for (i = j = 1; i < out_learnt.size(); i++) {
Lit lit(out_learnt[i]);
Clause& c = *getReason(lit);
if (&c == Clause::Decision()) {
out_learnt[j++] = lit;
} else {
bool keep = false;
// all literals of the implying clause must be:
for (int k = 1; !keep && k < c.size(); k++) {
if (
// already part of the lemma
!d_analyze_seen[c[k].var()]
&&
// or falsified in the root level
getLevel(c[k]) != d_rootLevel
) {
// failed, can't remove lit
out_learnt[j++] = lit;
keep = true;
}
}
if (!keep) {
d_analyze_redundant.push_back(lit);
}
}
}
}
out_learnt.resize(j);
}
// clean seen for simplification and log derivation
// do this in reverse chronological order of variable assignment
// in combination with removing duplication literals after each resolution step
// this allows to resolve on each literal only once,
// as it depends only on literals (its clause contains only literals)
// which were assigned earlier.
if (getDerivation() != NULL) {
std::sort(d_analyze_redundant.begin(), d_analyze_redundant.end(), lastToFirst_lt(d_trail_pos));
}
for (vector<Lit>::const_iterator i = d_analyze_redundant.begin(); i != d_analyze_redundant.end(); ++i) {
Lit lit(*i);
d_analyze_seen[lit.var()] = 0;
// if this literal is falsified in the root level,
// but not implied in the current push level,
// and the lemma is currently valid in levels lower than the current push level,
// then don't remove the literal.
// instead move it to the end of the lemma,
// so that it won't hurt performance.
if (out_learnt.size() > 0 // found the empty clause, so remove all literals
&&
getLevel(lit) == d_rootLevel
&&
getPushID(lit) > pushID
&&
!d_pushes.empty()
&&
getPushID(lit) > d_pushes.front().d_clauseID
) {
out_learnt.push_back(lit);
continue;
}
// update the push level and the derivation wrt. the removed literal
pushID = max(pushID, getPushID(lit));
if (getDerivation() != NULL) {
// resolve on each removed literal with its reason
if (getLevel(lit) == d_rootLevel) {
inference->add(lit, getDerivation()->computeRootReason(~lit, this));
}
else {
Clause* reason = getReason(lit);
inference->add(lit, reason);
}
}
}
d_analyze_redundant.clear();
}
// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
//
// 'p' can be removed if it depends only on literals
// on which they other conflict clause literals do depend as well.
bool Solver::analyze_removable(Lit p, uint min_level, int pushID) {
DebugAssert(getReason(p) != Clause::Decision(), "MiniSat::Solver::analyze_removable: p is a decision.");
d_analyze_stack.clear();
d_analyze_stack.push_back(p);
int top = d_analyze_redundant.size();
while (d_analyze_stack.size() > 0){
DebugAssert(getReason(d_analyze_stack.back()) != Clause::Decision(),
"MiniSat::Solver::analyze_removable: stack var is a decision.");
DebugAssert(getReason(d_analyze_stack.back()) != Clause::TheoryImplication(),
"MiniSat::Solver::analyze_removable: stack var is an unresolved theory implication.");
Clause& c = *getReason(d_analyze_stack.back()); d_analyze_stack.pop_back();
for (int i = 1; i < c.size(); i++) {
Lit p = c[i];
// ignore literals already considered or implied at root level
if (!d_analyze_seen[p.var()]) {
if (getLevel(p) == d_rootLevel) {
d_analyze_redundant.push_back(p);
d_analyze_seen[p.var()] = 1;
}
else {
// min_level is a precheck,
// only try to remove literals which might be implied,
// at least wrt. to the abstraction min_level
if (getReason(p) != Clause::Decision() && ((1 << (getLevel(p) & 31)) & min_level) != 0){
d_analyze_seen[p.var()] = 1;
d_analyze_stack.push_back(p);
d_analyze_redundant.push_back(p);
} else {
// failed, so undo changes to seen literals/redundant and return
for (size_type j = top; j < d_analyze_redundant.size(); ++j) {
d_analyze_seen[d_analyze_redundant[j].var()] = 0;
}
d_analyze_redundant.resize(top);
return false;
}
}
}
}
}
d_analyze_redundant.push_back(p);
return true;
}
bool Solver::isImpliedAt(Lit lit, int clausePushID) const {
return
// literal asserted before first push
(d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
||
// or literal depends only on clauses added before given clause
getPushID(lit) < clausePushID;
}
// Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
// the clause is binary and satisfied, in which case the first literal is true)
// Returns True if clause is satisfied (will be removed), False otherwise.
//
bool Solver::isPermSatisfied(Clause* c) const {
for (int i = 0; i < c->size(); i++){
Lit lit((*c)[i]);
if (getValue(lit) == l_True
&& getLevel(lit) == d_rootLevel
&& isImpliedAt(lit, c->pushID())
)
return true;
}
return false;
}
// a split decision, returns FALSE if immediate conflict.
bool Solver::assume(Lit p) {
d_trail_lim.push_back(d_trail.size());
d_stats.max_level = std::max(d_trail_lim.size(), size_type(d_stats.max_level));
return enqueue(p, decisionLevel(), Clause::Decision());
}
// Revert to the state at given level, assert conflict clause and pending clauses
void Solver::backtrack(int toLevel, Clause* learnt_clause) {
DebugAssert (decisionLevel() > toLevel, "MiniSat::Solver::backtrack: backtrack not to previous level");
// backtrack theories
DebugAssert(toLevel >= d_rootLevel, "MiniSat::Solver::backtrack: backtrack beyond root level");
for (int i = toLevel; i < decisionLevel(); ++i) {
d_theoryAPI->pop();
}
// backtrack trail
int trail_size = d_trail.size();
int trail_jump = d_trail_lim[toLevel];
int first_invalid = d_trail_lim[toLevel];
for (int c = first_invalid; c < trail_size; ++c) {
Var x = d_trail[c].var();
// only remove enqueued elements which are not still implied after backtracking
if (getLevel(x) > toLevel) {
//setLevel(x, -1);
d_assigns[x] = toInt(l_Undef);
d_reason [x] = NULL;
//d_pushIDs[x] = -1;
d_order.undo(x);
}
else {
d_trail[first_invalid] = d_trail[c];
if (d_derivation != NULL) d_trail_pos[x] = first_invalid;
++first_invalid;
}
}
// shrink queue
d_trail.resize(first_invalid);
d_trail_lim.resize(toLevel);
d_qhead = trail_jump;
d_thead = d_qhead;
// insert lemma
// we want to insert the lemma before the original conflicting clause,
// so that propagation is done on the lemma instead of that clause.
// as that clause might be a theory clause in d_pendingClauses,
// the lemma has to be inserted before the pending clauses are added.
insertClause(learnt_clause);
// enqueue clauses which were conflicting in previous assignment
while (!isConflicting() && !d_pendingClauses.empty()) {
Clause* c = d_pendingClauses.front();
d_pendingClauses.pop();
addClause(*c, true);
}
// deallocate explanations for theory implications
// which have been retracted and are thus not needed anymore.
//
// not necessarily ordered by level,
// so stackwise deallocation by level does not necessarily remove
// all possible explanations as soon as possible.
// still, should be a good enough compromise between speed and completeness.
bool done = false;
while (!done && !d_theoryExplanations.empty()) {
std::pair<int, Clause*> pair = d_theoryExplanations.top();
if (pair.first > toLevel) {
d_theoryExplanations.pop();
remove(pair.second, true);
}
else {
done = true;
}
}
}
/*_________________________________________________________________________________________________
|
| enqueue : (p : Lit) (from : Clause*) -> [bool]
|
| Description:
| Puts a new fact on the propagation queue as well as immediately updating the variable's value.
| Should a conflict arise, FALSE is returned.
|
| Input:
| p - The fact to enqueue
| decisionLevel - The level from which on this propagation/decision holds.
| if a clause is added in a non-root level, there might be propagations
| which are not only valid in the current, but also earlier levels.
| from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
| Default value is NULL (no reason).
| GClause::s_theoryImplication means theory implication where explanation
| has not been retrieved yet.
|
| Output:
| TRUE if fact was enqueued without conflict, FALSE otherwise.
|________________________________________________________________________________________________@*/
bool Solver::enqueue(Lit p, int decisionLevel, Clause* from) {
lbool value(getValue(p));
if (value != l_Undef) {
return value != l_False;
}
else {
Var var(p.var());
d_assigns[var] = toInt(lbool(p.sign()));
setLevel(var, decisionLevel);
d_reason [var] = from;
setPushID(var, from);
d_trail.push_back(p);
if (d_derivation != NULL) d_trail_pos[var] = d_trail.size();
return true;
}
}
/*_________________________________________________________________________________________________
|
| propagate : [void] -> [Clause*]
|
| Description:
| Propagates one enqueued fact. If a conflict arises, updateConflict is called.
|________________________________________________________________________________________________@*/
// None:
//
// due to theory clauses and lazy retrieval of theory implications we get propagations
// out of any chronological order.
// therefore it is not guaranteed that in a propagating clause
// the first two literals (the watched literals) have the highest decision level.
//
// this doesn't matter, though, it suffices to ensure that
// if there are less than two undefined literals in a clause,
// than these are at the first two positions?
//
// Reasoning, for eager retrieval of explanations for theory implications:
// case analysis for first two positions:
// 1) TRUE, TRUE
// then the clause is satisfied until after backtracking
// the first two literals are undefined, or we get case 2) TRUE, FALSE
//
// 2) TRUE, FALSE
// if TRUE is true because it is a theory implication of FALSE,
// this is fine, as TRUE and FALSE will be backtracked at the same time,
// and then both literals will be undefined.
//
// this holds in general if TRUE was set before FALSE was set,
// so this case is fine.
//
// and TRUE can't be set after FALSE was set,
// as this would imply that all other literals are falsified as well
// (otherwise the FALSE literal would be replace by an undefined/satisfied literal),
// and then TRUE would be implied at the same level as FALSE
//
// 3) FALSE, TRUE
// can not happen, falsifying the first literal will reorder this to TRUE, FALSE
//
// 4) FALSE, FALSE
// Both literals must be falsified at the current level,
// as falsifying one triggers unit propagation on the other in the same level.
// so after backtracking both are undefined.
//
//
// now, if explanations for theory implications are retrieved lazily,
// then the level in which a literal was set might change later on.
// i.e. first it is assumed to be of the level in which the theory implication happened,
// but later on, when checking its explanation,
// the real level might be calculated to be an earlier level.
//
// this means, when the original level was L and the real level is K,
// that this literal is going to be undefined when backtracking before L,
// but is immediately propagated again if the new level is >= K.
// this is done until level K is reached,
// then this literal behaves like any ordinary literal.
// (ensured by backtrack)
//
// case analysis for first two positions:
// 1) TRUE, TRUE
// same as before
//
// 2) TRUE, FALSE
// the new case is that TRUE was initially of level <= FALSE,
// but now FALSE is set to a level < TRUE.
//
// then when on backtracking TRUE is unset,
// FALSE will also be unset, but then right away be set to FALSE again,
// so they work fine as watched literals.
//
// 3) FALSE, TRUE
// same as before
//
// 4) FALSE, FALSE
// if the level of both literals is unchanged,
// changes in other literals don't matter,
// as after backtracking both are undefined (same as before)
//
// if for one of the two (or both) the level is changed,
// after backtracking it will be falsified again immediately,
// and the watched literal works as expected:
// either the other literal is propagated,
// or there is now an undefined literal in the rest of the clause
// which becomes the new watched literal.
//
// changes in the rest of the clause are of no consequence,
// as they are assumed to be false in the conflict level,
// changes in their level do not change this,
// and after backtracking they are again taken into consideration
// for finding a new watched literal.
//
// so, even for lazy retrieval of theory implication explanations
// there is no need to explicitly set the 2nd watched literal
// to the most recently falsified one.
void Solver::propagate() {
Lit p = d_trail[d_qhead++]; // 'p' is enqueued fact to propagate.
vector<Clause*>& ws = getWatches(p);
d_stats.propagations++;
--d_simpDB_props;
if (getLevel(p) == d_rootLevel) ++d_simpDB_assigns;
// propagate p to theories
if (!defer_theory_propagation) {
d_theoryAPI->assertLit(miniSatToCVC(p));
++d_thead;
}
vector<Clause*>::iterator j = ws.begin();
vector<Clause*>::iterator i = ws.begin();
vector<Clause*>::iterator end = ws.end();
while (i != end) {
Clause& c = **i;
++i;
// Make sure the false literal is data[1]:
Lit false_lit = ~p;
if (c[0] == false_lit) {
c[0] = c[1];
c[1] = false_lit;
}
Lit first = c[0];
lbool val = getValue(first);
// If 0th watch is true, then clause is already satisfied.
if (val == l_True) {
DebugAssert(getValue(c[0]) == l_True && getValue(c[1]) == l_False,
"MiniSat::Solver:::propagate: True/False");
*j = &c; ++j;
}
// Look for new watch:
else {
for (int k = 2; k < c.size(); k++) {
if (getValue(c[k]) != l_False) {
c[1] = c[k];
c[k] = false_lit;
addWatch(~c[1], &c);
goto FoundWatch;
}
}
// Did not find watch -- clause is unit under assignment:
// check that all other literals are false
IF_DEBUG(
for (int z = 1; z < c.size(); ++z) {
DebugAssert(getValue(c[z]) == l_False,
"MiniSat::Solver:::propagate: Unit Propagation");
}
);
*j = &c; ++j;
if (!enqueue(first, getImplicationLevel(c), &c)){
// clause is conflicting
updateConflict(&c);
d_qhead = d_trail.size();
// remove gap created by watches for which a new watch has been picked
if (i != j) ws.erase(j, i);
return;
}
FoundWatch:;
}
}
// remove gap created by watches for which a new watch has been picked
ws.erase(j, ws.end());
}
/*_________________________________________________________________________________________________
|
| reduceDB : () -> [void]
|
| Description:
| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
|________________________________________________________________________________________________@*/
struct reduceDB_lt {
bool operator () (Clause* x, Clause* y) {
return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity());
}
};
void Solver::reduceDB() {
d_stats.lm_simpl++;
size_type i, j;
double extra_lim = d_cla_inc / d_learnts.size(); // Remove any clause below this activity
std::sort(d_learnts.begin(), d_learnts.end(), reduceDB_lt());
for (i = j = 0; i < d_learnts.size() / 2; i++){
if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]))
remove(d_learnts[i]);
else
d_learnts[j++] = d_learnts[i];
}
for (; i < d_learnts.size(); i++){
if (d_learnts[i]->size() > 2 && !isReason(d_learnts[i]) && d_learnts[i]->activity() < extra_lim)
remove(d_learnts[i]);
else
d_learnts[j++] = d_learnts[i];
}
d_learnts.resize(d_learnts.size() - (i - j), NULL);
d_stats.del_lemmas += (i - j);
d_simpRD_learnts = d_learnts.size();
}
/*_________________________________________________________________________________________________
|
| simplifyDB : [void] -> [bool]
|
| Description:
| Simplify the clause database according to the current top-level assigment. Currently, the only
| thing done here is the removal of satisfied clauses, but more things can be put here.
|________________________________________________________________________________________________@*/
void Solver::simplifyDB() {
// clause set is unsatisfiable
if (isConflicting()) return;
// need to do propagation to exhaustion before watches can be removed below.
// e.g. in a <- b, c, where b an c are satisfied by unit clauses,
// and b and c have been added to the propagation queue,
// but not propagated yet: then the watches are not evaluated yet,
// and a has not been propapagated.
// thus by removing the watches on b and c,
// the propagation of a would be lost.
DebugAssert(d_qhead == d_trail.size(),
"MiniSat::Solver::simplifyDB: called while propagation queue was not empty");
d_stats.db_simpl++;
// Clear watcher lists:
// could do that only for literals which are implied permanently,
// but we don't know that anymore with the push/pop interface:
// even if the push id of a literal is less than the first push clause id,
// it might depend on theory clauses,
// which will be retracted after a pop,
// so that the literal is not implied anymore.
// thus, this faster way of cleaning watches can not be used,
// instead they have to removed per clause below
/*
Lit lit;
for (vector<Lit>::const_iterator i = d_trail.begin(); i != d_trail.end(); ++i) {
lit = *i;
if (getLevel(lit) == d_rootLevel
&&
// must be in the root push
(d_pushes.empty() || getPushID(lit) <= d_pushes.front().d_clauseID)
) {
getWatches(lit).clear();
getWatches(~(lit)).clear();
}
}
*/
// Remove satisfied clauses:
for (int type = 0; type < 2; type++){
vector<Clause*>& cs = type ? d_learnts : d_clauses;
size_type j = 0;
bool satisfied = false;
for (vector<Clause*>::const_iterator i = cs.begin(); i != cs.end(); ++i) {
Clause* clause = *i;
if (isReason(clause)) {
cs[j++] = clause;
}
else {
satisfied = false;
// falsified = 0;
int k = 0;
int end = clause->size() - 1;
// skip the already permanently falsified tail
// clause should not be permanently falsified,
// as simplifyDB should only be called in a consistent state.
while (
(getLevel((*clause)[end]) == d_rootLevel)
&&
(getValue((*clause)[end]) == l_False)) {
DebugAssert(end > 0,
"MiniSat::Solver::simplifyDB: permanently falsified clause found");
--end;
}
while (k < end) {
Lit lit((*clause)[k]);
if (getLevel(lit) != d_rootLevel) {
++k;
}
else if (getValue(lit) == l_True) {
if (isImpliedAt(lit, clause->pushID())) {
satisfied = true;
break;
}
else {
++k;
}
}
else if (k > 1 && getValue(lit) == l_False) {
--end;
(*clause)[k] = (*clause)[end];
(*clause)[end] = lit;
} else {
++k;
}
}
if (satisfied) {
d_stats.del_clauses++;
remove(clause);
}
else {
cs[j++] = clause;
}
}
// isReason also ensures that unit clauses are kept
/*
if (!isReason(clause) && isPermSatisfied(clause)) {
d_stats.del_clauses++;
remove(clause);
}
else {
cs[j++] = clause;
}*/
}
cs.resize(j);
}
d_simpDB_assigns = 0;
d_simpDB_props = d_stats.clauses_literals + d_stats.learnts_literals;
}
void Solver::protocolPropagation() const {
if (protocol) {
Lit lit(d_trail[d_qhead]);
cout << "propagate: " << decisionLevel() << " : " << lit.index() << endl;
cout << "propagate: " << decisionLevel() << " : " << toString(lit, true)
<< " at: " << getLevel(lit);
if (getReason(lit.var()) != Clause::Decision())
cout << " from: " << toString(*getReason(lit.var()), true);
cout << endl;
}
}
void Solver::propLookahead(const SearchParams& params) {
// retrieve the best vars according to the heuristic
vector<Var> nextVars(prop_lookahead);
vector<Var>::size_type fetchedVars = 0;
while (fetchedVars < nextVars.size()) {
Var nextVar = d_order.select(params.random_var_freq);
if (isRegistered(nextVar) || nextVar == var_Undef) {
nextVars[fetchedVars] = nextVar;
++fetchedVars;
}
}
// and immediately put the variables back
for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
if (nextVars[i] != var_Undef) d_order.undo(nextVars[i]);
}
// propagate on these vars
int level = decisionLevel();
int first_invalid = d_trail.size();
for (vector<Var>::size_type i = 0; i < nextVars.size(); ++i) {
Var nextVar = nextVars[i];
if (nextVar == var_Undef) continue;
for (int sign = 0; sign < 2; ++sign) {
// first propagate on +var, then on -var
if (sign == 0) {
assume(Lit(nextVar, true));
} else {
assume(Lit(nextVar, false));
}
while (d_qhead < d_trail.size() && !isConflicting()) {
protocolPropagation();
propagate();
}
// propagation found a conflict
if (isConflicting()) return;
// otherwise remove assumption and backtrack
for (int i = d_trail.size() - 1; i >= first_invalid; --i) {
Var x = d_trail[i].var();
d_assigns[x] = toInt(l_Undef);
d_reason [x] = NULL;
d_order.undo(x);
}
d_trail.resize(first_invalid);
d_trail_lim.resize(level);
d_qhead = first_invalid;
}
}
}
CVC3::QueryResult Solver::search() {
DebugAssert(d_popRequests == 0, "MiniSat::Solver::search: pop requests pending");
DebugAssert(!d_pushes.empty(), "MiniSat::Solver::search: no push before search");
d_inSearch = true;
SearchParams params(d_default_params);
d_stats.starts++;
d_var_decay = 1 / params.var_decay;
d_cla_decay = 1 / params.clause_decay;
if (protocol) printState();
// initial unit propagation has been done in push -
// already unsatisfiable without search
if (!d_ok) {
if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
return CVC3::UNSATISFIABLE;
}
// main search loop
SAT::Lit literal;
SAT::Clause clause;
SAT::CNF_Formula_Impl clauses;
for (;;){
// if (d_learnts.size() == 1 && decisionLevel() == 3) printState();
// -1 needed if the current 'propagation' is a split
DebugAssert(d_thead <= d_qhead, "MiniSat::Solver::search: thead <= qhead");
DebugAssert(d_trail_lim.size() == 0 || d_qhead >= (size_type)d_trail_lim[decisionLevel() - 1],
"MiniSat::Solver::search: qhead >= trail_lim[decisionLevel()");
DebugAssert(d_trail_lim.size() == 0 || d_thead >= (size_type)d_trail_lim[decisionLevel() - 1],
"MiniSat::Solver::search: thead >= trail_lim[decisionLevel()");
// 1. clause set detected to be unsatisfiable
if (!d_ok) {
d_stats.conflicts++;
if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
return CVC3::UNSATISFIABLE;
}
// 2. out of resources, e.g. quantifier instantiation aborted
if (d_theoryAPI->outOfResources()) {
return CVC3::ABORT;
}
// 3. boolean conflict, backtrack
if (d_conflict != NULL){
d_stats.conflicts++;
// unsatisfiability detected
if (decisionLevel() == d_rootLevel){
d_ok = false;
if (getDerivation() != NULL) getDerivation()->finish(d_conflict, this);
return CVC3::UNSATISFIABLE;
}
int backtrack_level;
Clause* learnt_clause = analyze(backtrack_level);
backtrack(backtrack_level, learnt_clause);
if (protocol) {
cout << "conflict clause: " << toString(*learnt_clause, true);
clauses.print();
}
varDecayActivity();
claDecayActivity();
if (protocol) {
cout << "backtrack to: " << backtrack_level << endl;
}
}
// 4. theory conflict - cheap theory consistency check
else if (d_theoryAPI->checkConsistent(clause, false) == SAT::DPLLT::INCONSISTENT) {
if (protocol) {
cout << "theory inconsistency: " << endl;
clause.print();
}
d_stats.theory_conflicts++;
addClause(clause, true);
clause.clear();
}
// 5. boolean propagation
else if (d_qhead < d_trail.size()) {
// do boolean propagation to exhaustion
// before telling the theories about propagated literals
if (defer_theory_propagation) {
while (d_ok && d_qhead < d_trail.size() && !isConflicting()) {
protocolPropagation();
propagate();
}
}
// immediately tell theories about boolean propagations
else {
protocolPropagation();
propagate();
}
}
// :TODO: move to 8. tell theories about new boolean propagations
// problem: can lead to worse performance,
// apparently then to many theory clauses are learnt,
// so need to forget them (database cleanup), or limit them (subsumption test)
else if (defer_theory_propagation && d_thead < d_qhead) {
while (d_thead < d_qhead) {
d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
++d_thead;
}
}
// everything else
else {
DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
// 6. theory clauses
if (d_theoryAPI->getNewClauses(clauses)) {
if (protocol) {
cout << "theory clauses: " << endl;
clauses.print();
}
addFormula(clauses, true);
clauses.reset();
continue;
}
// 7. theory implication
literal = d_theoryAPI->getImplication();
if (!literal.isNull()) {
Lit lit = cvcToMiniSat(literal);
if (protocol) {
cout << "theory implication: " << lit.index() << endl;
}
if (
// get explanation now
eager_explanation
||
// enqueue, and retrieve explanation (as a conflict clause)
// only if this implication is responsible for a conflict.
!enqueue(lit, decisionLevel(), Clause::TheoryImplication())
) {
d_theoryAPI->getExplanation(literal, clause);
if (protocol) {
cout << "theory implication reason: " << endl;
clause.print();
}
addClause(clause, true);
clause.clear();
}
continue;
}
// // 8. tell theories about new boolean propagations
// if (defer_theory_propagation && d_thead < d_qhead) {
// d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
// ++d_thead;
// continue;
// }
// DebugAssert(d_qhead == d_thead, "MiniSat::Solver::search: d_qhead != d_thead");
// 9. boolean split
Lit next = lit_Undef;
// use CVC decider
if (d_decider != NULL) {
literal = d_decider->makeDecision();
if (!literal.isNull()) {
next = cvcToMiniSat(literal);
}
}
// use MiniSat's decision heuristic
else {
Var nextVar = d_order.select(params.random_var_freq);
if (nextVar != var_Undef){
next = ~Lit(nextVar, false);
}
}
if (next != lit_Undef) {
// Simplify the set of problem clauses:
// there must have been enough propagations in root level,
// and no simplification too recently
if (false && d_simpDB_props <= 0 && d_simpDB_assigns > (nAssigns() / 10)) {
simplifyDB();
DebugAssert(d_ok, "MiniSat::Solver::search: simplifyDB resulted in conflict");
}
// Reduce the set of learnt clauses:
//if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
//if (learnts.size()-nAssigns() >= nClauses() / 3)
// don't remove lemmas unless there are a significant number
//if (d_learnts.size() - nAssigns() < nClauses() / 3)
//return;
// don't remove lemmas unless there are lots of new ones
// if (d_learnts.size() - nAssigns() < 3 * d_simpRD_learnts)
// return;
// :TODO:
//reduceDB();
d_stats.decisions++;
d_theoryAPI->push();
DebugAssert(getValue(next) == l_Undef,
"MiniSat::Solver::search not undefined split variable chosen.");
if (protocol) {
cout << "Split: " << next.index() << endl;
}
// do lookahead based on MiniSat's decision heuristic
propLookahead(params);
if (isConflicting()) {
++d_stats.debug;
continue;
}
if (!assume(next)) {
DebugAssert(false, "MiniSat::Solver::search contradictory split variable chosen.");
}
continue;
}
// 10. full theory consistency check
SAT::DPLLT::ConsistentResult result = d_theoryAPI->checkConsistent(clause, true);
// inconsistency detected
if (result == SAT::DPLLT::INCONSISTENT) {
if (protocol) {
cout << "theory conflict (FULL): " << endl;
clause.print();
}
d_stats.theory_conflicts++;
addClause(clause, true);
clause.clear();
continue;
}
// perhaps consistent, new clauses added by theory propagation
if (result == SAT::DPLLT::MAYBE_CONSISTENT) {
if (d_theoryAPI->getNewClauses(clauses)) {
if (protocol) {
cout << "theory clauses: " << endl;
clauses.print();
}
addFormula(clauses, true);
clauses.reset();
}
// it can happen that after doing a full consistency check
// there are actually no new theory clauses,
// but then there will be new decisions in the next round.
continue;
}
// consistent
if (result == SAT::DPLLT::CONSISTENT) {
return CVC3::SATISFIABLE;
}
FatalAssert(false, "DPLLTMiniSat::search: unreachable");
return CVC3::SATISFIABLE;
}
}
}
/// Activity
// Divide all variable activities by 1e100.
//
void Solver::varRescaleActivity() {
for (int i = 0; i < nVars(); i++)
d_activity[i] *= 1e-100;
d_var_inc *= 1e-100;
}
// Divide all constraint activities by 1e100.
//
void Solver::claRescaleActivity() {
for (vector<Clause*>::const_iterator i = d_learnts.begin(); i != d_learnts.end(); i++)
(*i)->activity() *= (float)1e-20;
d_cla_inc *= 1e-20;
}
///
/// expensive debug checks
///
void Solver::checkWatched(const Clause& clause) const {
// unary clauses are not watched
if (clause.size() < 2) return;
for (int i = 0; i < 2; ++i) {
Lit lit = clause[i];
bool found = false;
const vector<Clause*>& ws = getWatches(~lit);
// simplifyDB removes watches on permanently set literals
if (getLevel(lit) == d_rootLevel) found = true;
// search for clause in watches
for (size_type j = 0; !found && j < ws.size(); ++j) {
if (ws[j] == &clause) found = true;
}
if (!found) {
printState();
cout << toString(clause, true) << " : " << toString(clause[i], false) << endl;
FatalAssert(false, "MiniSat::Solver::checkWatched");
}
}
}
void Solver::checkWatched() const {
if (!debug_full) return;
for (size_type i = 0; i < d_clauses.size(); ++i) {
checkWatched(*d_clauses[i]);
}
for (size_type i = 0; i < d_learnts.size(); ++i) {
checkWatched(*d_learnts[i]);
}
}
void Solver::checkClause(const Clause& clause) const {
// unary clauses are true anyway
if (clause.size() < 2) return;
// 1) the first two literals are undefined
if (getValue(clause[0]) == l_Undef && getValue(clause[1]) == l_Undef)
return;
// 2) one of the first two literals is satisfied
else if (getValue(clause[0]) == l_True || getValue(clause[1]) == l_True)
return;
// 3) the first literal is undefined and all other literals are falsified
// 4) all literals are falsified
else {
bool ok = true;
if (getValue(clause[0]) == l_True)
ok = false;
for (int j = 1; ok && j < clause.size(); ++j) {
if (getValue(clause[j]) != l_False) {
ok = false;
}
}
if (ok) return;
}
printState();
cout << endl;
cout << toString(clause, true) << endl;
FatalAssert(false, "MiniSat::Solver::checkClause");
}
void Solver::checkClauses() const {
if (!debug_full) return;
for (size_type i = 0; i < d_clauses.size(); ++i) {
checkClause(*d_clauses[i]);
}
for (size_type i = 0; i < d_learnts.size(); ++i) {
checkClause(*d_learnts[i]);
}
}
void Solver::checkTrail() const {
if (!debug_full) return;
for (size_type i = 0; i < d_trail.size(); ++i) {
Lit lit = d_trail[i];
Var var = lit.var();
Clause* reason = d_reason[var];
if (reason == Clause::Decision()
||
reason == Clause::TheoryImplication()) {
}
else {
const Clause& clause = *reason;
// check that the first clause literal is the implied literal
FatalAssert(clause.size() > 0, "MiniSat::Solver::checkTrail: empty clause as reason for " /*+ var*/);
FatalAssert(lit == clause[0], "MiniSat::Solver::checkTrail: incorrect reason for " /*+ var*/);
FatalAssert(d_assigns[var] == toInt(lbool(lit.sign())), "MiniSat::Solver::checkTrail: incorrect value for " /*+ var*/);
// check that other literals are in the trail before this literal and this literal's level
for (int j = 1; j < clause.size(); ++j) {
Lit clauseLit = clause[j];
Var clauseVar = clauseLit.var();
FatalAssert(getLevel(var) >= getLevel(clauseVar),
"MiniSat::Solver::checkTrail: depends on later asserted literal " /*+ var*/);
bool found = false;
for (size_type k = 0; k < i; ++k) {
if (d_trail[k] == ~clauseLit) {
found = true;
break;
}
}
FatalAssert(found, "MiniSat::Solver::checkTrail: depends on literal not in context " /*+ var*/);
}
}
}
}
void Solver::setPushID(Var var, Clause* from) {
// check that var is implied by from
DebugAssert(getReason(var) == from, "MiniSat::Solver::setPushID: wrong reason given");
int pushID = std::numeric_limits<int>::max();
if (from != Clause::Decision() && from != Clause::TheoryImplication()) {
pushID = from->pushID();
for (int i = 1; i < from->size(); ++i) {
pushID = std::max(pushID, getPushID((*from)[i]));
}
}
d_pushIDs[var] = pushID;
}
void Solver::push() {
DebugAssert(!inSearch(), "MiniSat::Solver::push: already in search");
// inconsistency before this push, so nothing can happen after it,
// so just mark this push as useless.
// (can happen if before checkSat initial unit propagation finds an inconsistency)
if (!d_ok) {
d_pushes.push_back(PushEntry(-1, 0, 0, 0));
return;
}
d_registeredVars.resize(d_registeredVars.size() + 1);
// reinsert lemmas kept over the last pop
for (vector<Clause*>::const_iterator i = d_popLemmas.begin(); i != d_popLemmas.end(); ++i) {
Clause* lemma = *i;
insertLemma(lemma, lemma->id(), lemma->pushID());
d_stats.learnts_literals -= lemma->size();
remove(lemma, true);
}
d_popLemmas.clear();
// do propositional propagation to exhaustion, including the theory
if (push_theory_propagation) {
SAT::Lit literal;
SAT::Clause clause;
SAT::CNF_Formula_Impl clauses;
// while more can be propagated
while (!isConflicting() && (d_qhead < d_trail.size() || d_thead < d_qhead)) {
// do propositional propagation to exhaustion
while (!isConflicting() && d_qhead < d_trail.size()) {
protocolPropagation();
propagate();
}
// also propagate to theories right away
if (defer_theory_propagation) {
while (!isConflicting() && d_thead < d_qhead) {
d_theoryAPI->assertLit(miniSatToCVC(d_trail[d_thead]));
++d_thead;
}
}
// propagate a theory implication
if (push_theory_implication) {
literal = d_theoryAPI->getImplication();
if (!literal.isNull()) {
Lit lit = cvcToMiniSat(literal);
if (protocol) {
cout << "theory implication: " << lit.index() << endl;
}
if (
// get explanation now
eager_explanation
||
// enqueue, and retrieve explanation (as a conflict clause)
// only if this implication is responsible for a conflict.
!enqueue(lit, decisionLevel(), Clause::TheoryImplication())
) {
d_theoryAPI->getExplanation(literal, clause);
if (protocol) {
cout << "theory implication reason: " << endl;
clause.print();
}
addClause(clause, false);
clause.clear();
}
continue;
}
}
// add a theory clause
if (push_theory_clause && d_theoryAPI->getNewClauses(clauses)) {
if (protocol) {
cout << "theory clauses: " << endl;
clauses.print();
}
addFormula(clauses, false);
clauses.reset();
continue;
}
}
}
// do propositional propagation to exhaustion, but only on the propositional level
else {
while (!isConflicting() && d_qhead < d_trail.size()) {
protocolPropagation();
propagate();
}
}
simplifyDB();
// can happen that conflict is detected in propagate
// but d_ok is not immediately set to false
if (isConflicting()) d_ok = false;
if (d_derivation != NULL) d_derivation->push(d_clauseIDCounter);
d_pushes.push_back(PushEntry(d_clauseIDCounter - 1, d_trail.size(), d_qhead, d_thead));
};
void Solver::requestPop() {
DebugAssert(inPush(), "MiniSat::Solver::requestPop: no more pushes");
// pop theories on first pop of consistent solver,
// for inconsistent solver this is done in dpllt_minisat before the pop
if (d_popRequests == 0 && isConsistent()) popTheories();
++d_popRequests;
}
void Solver::doPops() {
if (d_popRequests == 0) return;
while (d_popRequests > 1) {
--d_popRequests;
d_pushes.pop_back();
}
pop();
}
void Solver::popTheories() {
for (int i = d_rootLevel; i < decisionLevel(); ++i) {
d_theoryAPI->pop();
}
}
void Solver::popClauses(const PushEntry& pushEntry, vector<Clause*>& clauses) {
size_type i = 0;
while (i != clauses.size()) {
// keep clause
if (clauses[i]->pushID() >= 0
&&
clauses[i]->pushID() <= pushEntry.d_clauseID) {
++i;
}
// remove clause
else {
remove(clauses[i]);
clauses[i] = clauses.back();
clauses.pop_back();
}
}
}
void Solver::pop() {
DebugAssert(d_popRequests == 1, "Minisat::Solver::pop: d_popRequests != 1");
--d_popRequests;
PushEntry pushEntry = d_pushes.back();
d_pushes.pop_back();
// solver was already inconsistent before the push
if (pushEntry.d_clauseID == -1) {
DebugAssert(!d_ok, "Minisat::Solver::pop: inconsistent push, but d_ok == true");
return;
}
// backtrack trail
//
// Note:
// the entries that were added to the trail after the push,
// and are kept over the pop,
// are all based on propagating clauses/lemmas also kept after the push.
// as they are not yet propagated yet, but only in the propagation queue,
// watched literals will work fine.
size_type first_invalid = pushEntry.d_trailSize;
for (size_type i = pushEntry.d_trailSize; i != d_trail.size(); ++i) {
Var x = d_trail[i].var();
//setLevel(x, -1);
d_assigns[x] = toInt(l_Undef);
d_reason [x] = NULL;
//d_pushIDs[x] = -1;
d_order.undo(x);
}
d_trail.resize(first_invalid);
d_trail_lim.resize(0);
d_qhead = pushEntry.d_qhead;
d_thead = pushEntry.d_thead;
// remove clauses added after push
popClauses(pushEntry, d_clauses);
// move all lemmas that are not already the reason for an implication
// to pending lemmas - these are to be added when the next push is done.
size_type i = 0;
while (i != d_popLemmas.size()) {
if (d_popLemmas[i]->pushID() <= pushEntry.d_clauseID) {
++i;
} else {
remove(d_popLemmas[i], true);
d_popLemmas[i] = d_popLemmas.back();
d_popLemmas.pop_back();
}
}
i = 0;
while (i != d_learnts.size()) {
Clause* lemma = d_learnts[i];
// lemma is propagating, so it was already present before the push
if (isReason(lemma)) {
++i;
}
// keep lemma?
else {
d_stats.learnts_literals -= lemma->size();
// lemma ok after push, mark it for reinsertion in the next push
if (lemma->pushID() <= pushEntry.d_clauseID) {
if (lemma->size() >= 2) {
removeWatch(getWatches(~(*lemma)[0]), lemma);
removeWatch(getWatches(~(*lemma)[1]), lemma);
}
d_popLemmas.push_back(lemma);
}
// lemma needs to be removed
else {
remove(lemma);
}
d_learnts[i] = d_learnts.back();
d_learnts.pop_back();
}
}
d_stats.debug += d_popLemmas.size();
// remove all pending clauses and explanations
while (!d_pendingClauses.empty()) {
remove(d_pendingClauses.front(), true);
d_pendingClauses.pop();
}
while (!d_theoryExplanations.empty()) {
remove(d_theoryExplanations.top().second, true);
d_theoryExplanations.pop();
}
// backtrack registered variables
d_registeredVars.resize(d_pushes.size() + 1);
// this needs to be done _after_ clauses have been removed above,
// as it might deallocate removed clauses
if (d_derivation != NULL) d_derivation->pop(pushEntry.d_clauseID);
// not conflicting or in search anymore
d_conflict = NULL;
d_ok = true;
d_inSearch = false;
};
syntax highlighted by Code2HTML, v. 0.9.1