*/
bool assertionLevelOnly()
{
- return options::unsatCores() && options::incrementalSolving();
+ return (options::proofNew() || options::unsatCores())
+ && options::incrementalSolving();
}
//=================================================================================================
propagation_budget(-1),
asynch_interrupt(false)
{
+ if (pnm)
+ {
+ d_pfManager.reset(
+ new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
+ }
+
if (options::unsatCores())
{
ProofManager::currentPM()->initSatProof(this);
}
CRef Solver::reason(Var x) {
- Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
+ Trace("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
// If we already have a reason, just return it
- if (vardata[x].d_reason != CRef_Lazy) return vardata[x].d_reason;
+ if (vardata[x].d_reason != CRef_Lazy)
+ {
+ if (Trace.isOn("pf::sat"))
+ {
+ Trace("pf::sat") << " Solver::reason: " << vardata[x].d_reason << ", ";
+ if (vardata[x].d_reason == CRef_Undef)
+ {
+ Trace("pf::sat") << "CRef_Undef";
+ }
+ else
+ {
+ for (unsigned i = 0, size = ca[vardata[x].d_reason].size(); i < size;
+ ++i)
+ {
+ Trace("pf::sat") << ca[vardata[x].d_reason][i] << " ";
+ }
+ }
+ Trace("pf::sat") << "\n";
+ }
+ return vardata[x].d_reason;
+ }
// What's the literal we are trying to explain
Lit l = mkLit(x, value(x) != l_True);
vec<Lit> explanation;
MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
- Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl
+ Trace("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl
<< std::endl;
// Sort the literals by trail index level
}
explanation.shrink(i - j);
- Debug("pf::sat") << "Solver::reason: explanation = ";
+ Trace("pf::sat") << "Solver::reason: explanation = ";
for (int k = 0; k < explanation.size(); ++k)
{
- Debug("pf::sat") << explanation[k] << " ";
+ Trace("pf::sat") << explanation[k] << " ";
}
- Debug("pf::sat") << std::endl;
+ Trace("pf::sat") << std::endl;
// We need an explanation clause so we add a fake literal
if (j == 1)
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;
+ Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
+ << std::endl;
if (options::unsatCores())
{
ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
}
// If a literal is false at 0 level (both sat and user level) we also ignore it
if (value(ps[i]) == l_False) {
- if (!options::unsatCores() && level(var(ps[i])) == 0
- && user_level(var(ps[i])) == 0)
+ if (!options::unsatCores() && !isProofEnabled()
+ && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
{
continue;
}
// If we are in solve_ or propagate
if (minisat_busy)
{
- Debug("pf::sat") << "Add clause adding a new lemma: ";
+ Trace("pf::sat") << "Add clause adding a new lemma: ";
for (int k = 0; k < ps.size(); ++k) {
- Debug("pf::sat") << ps[k] << " ";
+ Trace("pf::sat") << ps[k] << " ";
}
- Debug("pf::sat") << std::endl;
+ Trace("pf::sat") << std::endl;
lemmas.push();
ps.copyTo(lemmas.last());
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
- if (options::unsatCores())
+ if (options::unsatCores() || isProofEnabled())
{
// Take care of false units here; otherwise, we need to
// construct the clause below to give to the proof manager
ProofManager::getSatProof()->finalizeProof(
CVC4::Minisat::CRef_Lazy);
}
+ if (isProofEnabled())
+ {
+ d_pfManager->finalizeProof(ps[0], true);
+ }
return ok = false;
}
}
clauses_persistent.push(cr);
attachClause(cr);
- if (options::unsatCores())
+ if (options::unsatCores() || isProofEnabled())
{
- ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind()
- ? INPUT
- : THEORY_LEMMA;
- id = ProofManager::getSatProof()->registerClause(cr, ck);
- // map id to assertion, which may be required if looking for
- // lemmas in unsat core
- if (ck == THEORY_LEMMA)
+ if (options::unsatCores())
{
- ProofManager::getCnfProof()->registerConvertedClause(id);
+ ClauseKind ck =
+ ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->registerClause(cr, ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
}
if (ps.size() == falseLiteralsCount)
{
- ProofManager::getSatProof()->finalizeProof(cr);
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->finalizeProof(cr);
+ }
+ if (isProofEnabled())
+ {
+ d_pfManager->finalizeProof(ca[cr], true);
+ }
return ok = false;
}
}
ProofManager::getCnfProof()->registerConvertedClause(id);
}
}
+ // We need to do this so that the closedness check, if being done,
+ // goes through when we have unit assumptions whose literal has
+ // already been registered, as the ProofCnfStream will not register
+ // them and as they are not the result of propagation will be left
+ // hanging in assumptions accumulator
+ if (isProofEnabled() && ps.size() == 1)
+ {
+ d_pfManager->registerSatLitAssumption(ps[0]);
+ }
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
if (options::unsatCores())
ProofManager::getSatProof()->finalizeProof(confl);
}
}
+ if (isProofEnabled())
+ {
+ if (ca[confl].size() == 1)
+ {
+ d_pfManager->finalizeProof(ca[confl][0]);
+ }
+ else
+ {
+ d_pfManager->finalizeProof(ca[confl]);
+ }
+ }
}
return ok;
} else {
void Solver::attachClause(CRef cr) {
const Clause& c = ca[cr];
- Debug("minisat") << "Solver::attachClause(" << c << "): level " << c.level() << std::endl;
+ if (Debug.isOn("minisat"))
+ {
+ Debug("minisat") << "Solver::attachClause(" << c << "): ";
+ for (unsigned i = 0, size = c.size(); i < size; ++i)
+ {
+ Debug("minisat") << c[i] << " ";
+ }
+ Debug("minisat") << ", level " << c.level() << "\n";
+ }
Assert(c.size() > 1);
watches[~c[0]].push(Watcher(cr, c[1]));
watches[~c[1]].push(Watcher(cr, c[0]));
void Solver::detachClause(CRef cr, bool strict) {
const Clause& c = ca[cr];
+ Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
+ if (Debug.isOn("minisat"))
+ {
+ Debug("minisat") << "Solver::detachClause(" << c << "), CRef " << cr
+ << ", clause ";
+ for (unsigned i = 0, size = c.size(); i < size; ++i)
+ {
+ Debug("minisat") << c[i] << " ";
+ }
+
+ Debug("minisat") << "\n";
+ }
+ assert(c.size() > 1);
if (options::unsatCores())
{
ProofManager::getSatProof()->markDeleted(cr);
}
- Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
- assert(c.size() > 1);
if (strict){
remove(watches[~c[0]], Watcher(cr, c[1]));
void Solver::removeClause(CRef cr) {
Clause& c = ca[cr];
- Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl;
+ if (Debug.isOn("minisat"))
+ {
+ Debug("minisat") << "Solver::removeClause(" << c << "), CRef " << cr
+ << ", clause ";
+ for (unsigned i = 0, size = c.size(); i < size; ++i)
+ {
+ Debug("minisat") << c[i] << " ";
+ }
+ Debug("minisat") << "\n";
+ }
detachClause(cr);
// Don't leave pointers to free'd memory!
- if (locked(c)) vardata[var(c[0])].d_reason = CRef_Undef;
+ if (locked(c))
+ {
+ // a locked clause c is one whose first literal c[0] is true and is
+ // propagated by c itself, i.e. vardata[var(c[0])].d_reason == c. Because
+ // of this if we need to justify the propagation of c[0], via
+ // Solver::reason, if it appears in a resolution chain built lazily we
+ // will be unable to do so after the step below. Thus we eagerly justify
+ // this propagation here.
+ if (isProofEnabled())
+ {
+ Trace("pf::sat")
+ << "Solver::removeClause: eagerly compute propagation of " << c[0]
+ << "\n";
+ d_pfManager->startResChain(c);
+ for (unsigned i = 1, size = c.size(); i < size; ++i)
+ {
+ d_pfManager->addResolutionStep(c[i]);
+ }
+ d_pfManager->endResChain(c[0]);
+ }
+ vardata[var(c[0])].d_reason = CRef_Undef;
+ }
c.mark(1);
ca.free(cr);
}
{
ProofManager::getSatProof()->startResChain(confl);
}
+ if (isProofEnabled())
+ {
+ d_pfManager->startResChain(ca[confl]);
+ }
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
}
// FIXME: can we do it lazily if we actually need the proof?
- if (options::unsatCores() && level(var(q)) == 0)
+ if (level(var(q)) == 0)
{
- ProofManager::getSatProof()->resolveOutUnit(q);
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->resolveOutUnit(q);
+ }
+ if (isProofEnabled())
+ {
+ d_pfManager->addResolutionStep(q);
+ }
}
}
}
seen[var(p)] = 0;
pathC--;
- if (options::unsatCores() && pathC > 0 && confl != CRef_Undef)
+ if (pathC > 0 && confl != CRef_Undef)
{
- ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
+ }
+ if (isProofEnabled())
+ {
+ d_pfManager->addResolutionStep(ca[confl], p);
+ }
}
}while (pathC > 0);
out_learnt[0] = ~p;
+ if (Debug.isOn("newproof::sat"))
+ {
+ Debug("newproof::sat") << "finished with learnt clause ";
+ for (unsigned i = 0, size = out_learnt.size(); i < size; ++i)
+ {
+ prop::SatLiteral satLit = toSatLiteral<Minisat::Solver>(out_learnt[i]);
+ Debug("newproof::sat") << satLit << " ";
+ }
+ Debug("newproof::sat") << "\n";
+ }
// Simplify conflict clause:
int i, j;
{
ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
}
+ if (isProofEnabled())
+ {
+ Debug("newproof::sat")
+ << "Solver::analyze: redundant lit "
+ << toSatLiteral<Minisat::Solver>(out_learnt[i]) << "\n";
+ d_pfManager->addResolutionStep(out_learnt[i], true);
+ }
// Literal is redundant, to be safe, mark the level as current assertion level
// TODO: maybe optimize
max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
seen[var(p)] = 0;
}
-
void Solver::uncheckedEnqueue(Lit p, CRef from)
{
- Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl;
- assert(value(p) == l_Undef);
- assert(var(p) < nVars());
- assigns[var(p)] = lbool(!sign(p));
- vardata[var(p)] = VarData(from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
- trail.push_(p);
- if (theory[var(p)]) {
- // Enqueue to the theory
- d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
+ if (Debug.isOn("minisat"))
+ {
+ Debug("minisat") << "unchecked enqueue of " << p << " ("
+ << trail_index(var(p)) << ") trail size is "
+ << trail.size() << " cap is " << trail.capacity()
+ << ", reason is " << from << ", ";
+ if (from == CRef_Lazy)
+ {
+ Debug("minisat") << "CRef_Lazy";
+ }
+ else if (from == CRef_Undef)
+ {
+ Debug("minisat") << "CRef_Undef";
+ }
+ else
+ {
+ for (unsigned i = 0, size = ca[from].size(); i < size; ++i)
+ {
+ Debug("minisat") << ca[from][i] << " ";
+ }
}
+ Debug("minisat") << "\n";
+ }
+ assert(value(p) == l_Undef);
+ assert(var(p) < nVars());
+ assigns[var(p)] = lbool(!sign(p));
+ vardata[var(p)] = VarData(
+ from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size());
+ trail.push_(p);
+ if (theory[var(p)])
+ {
+ // Enqueue to the theory
+ d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
+ }
}
-
CRef Solver::propagate(TheoryCheckType type)
{
CRef confl = CRef_Undef;
// store a resolution of the literal c propagated
ProofManager::getSatProof()->storeUnitResolution(c[0]);
}
- removeClause(cs[i]);
+ removeClause(cs[i]);
}
else
cs[j++] = cs[i];
conflicts++; conflictC++;
- if (decisionLevel() == 0) {
+ if (decisionLevel() == 0)
+ {
if (options::unsatCores())
{
ProofManager::getSatProof()->finalizeProof(confl);
}
+ if (isProofEnabled())
+ {
+ if (confl == CRef_Lazy)
+ {
+ d_pfManager->finalizeProof();
+ }
+ else
+ {
+ d_pfManager->finalizeProof(ca[confl]);
+ }
+ }
return l_False;
}
// Assert the conflict clause and the asserting literal
if (learnt_clause.size() == 1) {
uncheckedEnqueue(learnt_clause[0]);
-
if (options::unsatCores())
{
ProofManager::getSatProof()->endResChain(learnt_clause[0]);
}
+ if (isProofEnabled())
+ {
+ d_pfManager->endResChain(learnt_clause[0]);
+ }
} else {
CRef cr =
ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
ProofManager::getSatProof()->registerClause(cr, LEARNT);
ProofManager::getSatProof()->endResChain(id);
}
+ if (isProofEnabled())
+ {
+ d_pfManager->endResChain(ca[cr]);
+ }
}
varDecayActivity();
check_type = CHECK_WITH_THEORY;
}
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
- || !withinBudget(ResourceManager::Resource::SatConflictStep))
- {
- // Reached bound on number of conflicts:
- progress_estimate = progressEstimate();
- cancelUntil(0);
- // [mdeters] notify theory engine of restarts for deferred
- // theory processing
- d_proxy->notifyRestart();
- return l_Undef;
- }
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+ || !withinBudget(ResourceManager::Resource::SatConflictStep))
+ {
+ // Reached bound on number of conflicts:
+ progress_estimate = progressEstimate();
+ cancelUntil(0);
+ // [mdeters] notify theory engine of restarts for deferred
+ // theory processing
+ d_proxy->notifyRestart();
+ return l_Undef;
+ }
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
// Pop the trail below the user level
--assertionLevel;
+ Debug("minisat") << "in user pop, decreasing assertion level to "
+ << assertionLevel << "\n"
+ << CVC4::push;
while (true) {
Debug("minisat") << "== unassigning " << trail.last() << std::endl;
Var x = var(trail.last());
break;
}
}
+
// The head should be at the trail top
qhead = trail.size();
// Remove the clauses
removeClausesAboveLevel(clauses_persistent, assertionLevel);
removeClausesAboveLevel(clauses_removable, assertionLevel);
-
+ Debug("minisat") << CVC4::pop;
// Pop the SAT context to notify everyone
d_context->pop(); // SAT context for CVC4
+ Debug("minisat") << "MINISAT POP assertionLevel is " << assertionLevel
+ << ", trail.size is " << trail.size() << "\n";
// Pop the created variables
resizeVars(assigns_lim.last());
assigns_lim.pop();
// The current lemma
vec<Lit>& lemma = lemmas[i];
- Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
+ Trace("pf::sat") << "Solver::updateLemmas: working on lemma: ";
for (int k = 0; k < lemma.size(); ++k) {
- Debug("pf::sat") << lemma[k] << " ";
+ Trace("pf::sat") << lemma[k] << " ";
}
- Debug("pf::sat") << std::endl;
+ Trace("pf::sat") << std::endl;
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
- Assert(!options::unsatCores());
+ Assert(!options::unsatCores() && !isProofEnabled());
conflict = CRef_Lazy;
backtrackLevel = 0;
Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
{
Node cnf_assertion = lemmas_cnf_assertion[j];
- Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
+ Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
<< cnf_assertion << value(lemma[0]) << std::endl;
ClauseId id = ProofManager::getSatProof()->registerUnitClause(
lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
}
-
+ if (CVC4::options::proofNew())
+ {
+ Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: "
+ << lemma[0] << std::endl;
+ }
if (value(lemma[0]) == l_False) {
// We have a conflict
if (lemma.size() > 1) {
{
ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
}
+ if (isProofEnabled())
+ {
+ d_pfManager->storeUnitConflict(lemma[0]);
+ }
}
} else {
Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
ClauseAllocator& to,
CVC4::TSatProof<Solver>* proof)
{
-
+ Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
// FIXME what is this CRef_lazy
if (cr == CRef_Lazy) return;
SatProofManager* Solver::getProofManager()
{
- return d_pfManager ? d_pfManager.get() : nullptr;
+ return isProofEnabled() ? d_pfManager.get() : nullptr;
}
std::shared_ptr<ProofNode> Solver::getProof()
{
- return d_pfManager ? d_pfManager->getProof() : nullptr;
+ return isProofEnabled() ? d_pfManager->getProof() : nullptr;
}
+bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
+
} /* CVC4::Minisat namespace */
} /* CVC4 namespace */
projects / cvc5.git / commitdiff