d_context(context),
assertionLevel(0),
d_pfManager(nullptr),
- d_assertionLevelOnly(
- (options().smt.produceProofs || options().smt.unsatCores)
- && options().base.incrementalSolving),
d_enable_incremental(enableIncremental),
minisat_busy(false)
// Parameters (user settable):
setDecisionVar(v, dvar);
- Trace("minisat") << "new var " << v << std::endl;
+ Trace("minisat") << "new var " << v << " with assertion level "
+ << assertionLevel << std::endl;
// If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
if (preRegister)
// Compute the assertion level for this clause
int explLevel = 0;
- if (d_assertionLevelOnly)
+ if (assertionLevelOnly())
{
explLevel = assertionLevel;
}
else
{
- int i, j;
+ int i, j, size;
Lit prev = lit_Undef;
- for (i = 0, j = 0; i < explanation.size(); ++i)
+ for (i = 0, j = 0, size = explanation.size(); i < size; ++i)
{
// This clause is valid theory propagation, so its level is the level of
// the top literal
}
explanation.shrink(i - j);
- Trace("pf::sat") << "Solver::reason: explanation = ";
- for (int k = 0; k < explanation.size(); ++k)
- {
- Trace("pf::sat") << explanation[k] << " ";
- }
- Trace("pf::sat") << std::endl;
-
// We need an explanation clause so we add a fake literal
if (j == 1)
{
}
}
+ Trace("pf::sat") << "..adding in lvl " << explLevel
+ << " (assertion lvl: " << assertionLevel << ")\n";
+ if (needProof() && explLevel < assertionLevel)
+ {
+ Trace("pf::sat") << "..user level is " << userContext()->getLevel() << "\n";
+ Assert(userContext()->getLevel() == (assertionLevel + 1));
+ d_proxy->notifyCurrPropagationInsertedAtLevel(explLevel);
+ }
// Construct the reason
CRef real_reason = ca.alloc(explLevel, explanation, true);
vardata[x] = VarData(
Lit p; int i, j;
// Which user-level to assert this clause at
- int clauseLevel = (removable && !d_assertionLevelOnly) ? 0 : assertionLevel;
+ int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel;
// Check the clause for tautologies and similar
int falseLiteralsCount = 0;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
// Update the level
- clauseLevel = d_assertionLevelOnly
+ clauseLevel = assertionLevelOnly()
? assertionLevel
: std::max(clauseLevel, intro_level(var(ps[i])));
// Tautologies are ignored
// If we are in solve_ or propagate
if (minisat_busy)
{
- Trace("pf::sat") << "Add clause adding a new lemma: ";
- for (int k = 0; k < ps.size(); ++k) {
- Trace("pf::sat") << ps[k] << " ";
+ if (TraceIsOn("pf::sat"))
+ {
+ Trace("pf::sat") << "Add clause adding a new lemma: ";
+ for (int k = 0, size = ps.size(); k < size; ++k)
+ {
+ Trace("pf::sat") << ps[k] << " ";
+ }
+ Trace("pf::sat") << std::endl;
}
- Trace("pf::sat") << std::endl;
-
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
cr = ca.alloc(clauseLevel, ps, false);
clauses_persistent.push(cr);
attachClause(cr);
-
+ if (needProof() && clauseLevel < assertionLevel)
+ {
+ if (TraceIsOn("pf::sat"))
+ {
+ Trace("pf::sat") << "addClause_: ";
+ for (int k = 0, size = ps.size(); k < size; ++k)
+ {
+ Trace("pf::sat") << ps[k] << " ";
+ }
+ Trace("pf::sat") << " clause/assert levels " << clauseLevel << " / "
+ << assertionLevel << "\n";
+ }
+ SatClause satClause;
+ MinisatSatSolver::toSatClause(ca[cr], satClause);
+ d_proxy->notifyClauseInsertedAtLevel(satClause, clauseLevel);
+ }
if (options().smt.unsatCores || needProof())
{
if (ps.size() == falseLiteralsCount)
}
// Check if it propagates
- if (ps.size() == falseLiteralsCount + 1) {
- if(assigns[var(ps[0])] == l_Undef) {
- Assert(assigns[var(ps[0])] != l_False);
- uncheckedEnqueue(ps[0], cr);
- Trace("cores") << "i'm registering a unit clause, maybe input"
+ if (ps.size() == falseLiteralsCount + 1 && assigns[var(ps[0])] == l_Undef)
+ {
+ Assert(assigns[var(ps[0])] != l_False);
+ uncheckedEnqueue(ps[0], cr);
+ Trace("pf::sat") << "Registering a unit clause " << ps[0]
+ << ", maybe input, with assigned var value "
+ << (assigns[var(ps[0])] == l_True
+ ? "true"
+ : (assigns[var(ps[0])] == l_False ? "false"
+ : "undef"))
+ << ", user_level(" << user_level(var(ps[0])) << ")"
<< std::endl;
- if (ps.size() == 1)
+ if (ps.size() == 1)
+ {
+ // 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 (needProof())
{
- // 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 (needProof())
+ d_pfManager->registerSatLitAssumption(ps[0]);
+ }
+ }
+ CRef confl = propagate(CHECK_WITHOUT_THEORY);
+ if (!(ok = (confl == CRef_Undef)))
+ {
+ if (needProof())
+ {
+ if (ca[confl].size() == 1)
{
- d_pfManager->registerSatLitAssumption(ps[0]);
+ d_pfManager->finalizeProof(ca[confl][0]);
}
- }
- CRef confl = propagate(CHECK_WITHOUT_THEORY);
- if(! (ok = (confl == CRef_Undef)) ) {
- if (needProof())
+ else
{
- if (ca[confl].size() == 1)
- {
- d_pfManager->finalizeProof(ca[confl][0]);
- }
- else
- {
- d_pfManager->finalizeProof(ca[confl]);
- }
+ d_pfManager->finalizeProof(ca[confl]);
}
}
- return ok;
- } else {
- return ok;
}
+ return ok;
}
}
-
return true;
}
Trace("minisat") << "unchecked enqueue of " << p << " ("
<< trail_index(var(p)) << ") trail size is "
<< trail.size() << " cap is " << trail.capacity()
+ << ", assertion level is " << assertionLevel
<< ", reason is " << from << ", ";
if (from == CRef_Lazy)
{
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (c.level() > level) {
- Assert(!locked(c));
+ SatClause satClause;
+ vec<Lit> clauseLits;
+ MinisatSatSolver::toSatClause(c, satClause);
+ MinisatSatSolver::toMinisatClause(satClause, clauseLits);
+ Assert(!locked(c)) << "Locked " << clauseLits;
removeClause(cs[i]);
} else {
cs[j++] = cs[i];
}
else
{
- CRef cr = ca.alloc(d_assertionLevelOnly ? assertionLevel : max_level,
+ CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
learnt_clause,
true);
clauses_removable.push(cr);
if (needProof())
{
d_pfManager->endResChain(ca[cr]);
+ if (TraceIsOn("pf::sat") && ca[cr].level() < assertionLevel)
+ {
+ Trace("pf::sat")
+ << "learnt_clause: " << ca[cr] << " clause/assert levels "
+ << ca[cr].level() << " / " << assertionLevel << "\n";
+ }
}
}
Assert(d_enable_incremental);
Assert(decisionLevel() == 0);
-
+ // Notify sat proof manager that we have popped and now potentially we need to
+ // retrieve the proofs for the clauses inserted into optimized levels
+ if (needProof())
+ {
+ d_pfManager->notifyPop();
+ }
// Pop the trail below the user level
--assertionLevel;
Trace("minisat") << "in user pop, decreasing assertion level to "
if (lemma.size() > 1) {
// If the lemmas is removable, we can compute its level by the level
int clauseLevel = assertionLevel;
- if (removable && !d_assertionLevelOnly)
+ if (removable && !assertionLevelOnly())
{
clauseLevel = 0;
for (int k = 0; k < lemma.size(); ++k)
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
+ // notify cnf stream that this clause's proof must be saved to resist
+ // context-popping
+ if (needProof() && clauseLevel < assertionLevel)
+ {
+ if (TraceIsOn("pf::sat"))
+ {
+ Trace("pf::sat") << "updateLemmas: ";
+ for (int k = 0, size = lemma.size(); k < size; ++k)
+ {
+ Trace("pf::sat") << lemma[k] << " ";
+ }
+ Trace("pf::sat") << " clause/assert levels " << clauseLevel << " / "
+ << assertionLevel << "\n";
+ }
+ SatClause satClause;
+ MinisatSatSolver::toSatClause(ca[lemma_ref], satClause);
+ d_proxy->notifyClauseInsertedAtLevel(satClause, clauseLevel);
+ }
if (removable) {
clauses_removable.push(lemma_ref);
} else {
&& options().smt.proofMode != options::ProofMode::PP_ONLY;
}
+bool Solver::assertionLevelOnly() const
+{
+ return options().smt.unsatCores && !needProof()
+ && options().base.incrementalSolving;
+}
+
} // namespace Minisat
} // namespace cvc5
projects / cvc5.git / commitdiff