nullptr,
userContext(),
"ProofCnfStream::LazyCDProof"),
- d_blocked(userContext())
+ d_blocked(userContext()),
+ d_optClausesManager(userContext(), &d_proof, d_optClausesPfs)
{
}
{
Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
<< ", negated = " << (negated ? "true" : "false")
- << ", removable = " << (removable ? "true" : "false") << ")\n";
+ << ", removable = " << (removable ? "true" : "false")
+ << "), level " << userContext()->getLevel() << "\n";
d_cnfStream.d_removable = removable;
if (pg)
{
{
clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
}
- normalizeAndRegister(clauseExp);
+ d_currPropagationProccessed = normalizeAndRegister(clauseExp);
// consume steps if clausification being recorded. If we are not logging it,
// we need to add the clause as a closed step to the proof so that the SAT
// proof does not have non-input formulas as assumptions.
}
}
+void ProofCnfStream::notifyCurrPropagationInsertedAtLevel(int explLevel)
+{
+ Assert(explLevel < (userContext()->getLevel() - 1));
+ Assert(!d_currPropagationProccessed.isNull());
+ Trace("cnf") << "Need to save curr propagation "
+ << d_currPropagationProccessed << "'s proof in level "
+ << explLevel + 1 << " despite being currently in level "
+ << userContext()->getLevel() << "\n";
+ // Save into map the proof of the processed propagation. Note that
+ // propagations must be explained eagerly, since their justification depends
+ // on the theory engine and may be different if we only get its proof when the
+ // SAT solver pops the user context. Not doing this may lead to open proofs.
+ //
+ // It's also necessary to copy the proof node, so we prevent unintended
+ // updates to the saved proof. Not doing this may also lead to open proofs.
+ std::shared_ptr<ProofNode> currPropagationProcPf =
+ d_env.getProofNodeManager()->clone(
+ d_proof.getProofFor(d_currPropagationProccessed));
+ Assert(currPropagationProcPf->getRule() != PfRule::ASSUME);
+ Trace("cnf-debug") << "\t..saved pf {" << currPropagationProcPf << "} "
+ << *currPropagationProcPf.get() << "\n";
+ d_optClausesPfs[explLevel + 1].push_back(currPropagationProcPf);
+
+ d_currPropagationProccessed = Node::null();
+}
+
+void ProofCnfStream::notifyClauseInsertedAtLevel(const SatClause& clause,
+ int clLevel)
+{
+ Trace("cnf") << "Need to save clause " << clause << " in level "
+ << clLevel + 1 << " despite being currently in level "
+ << userContext()->getLevel() << "\n";
+ Node clauseNode = getClauseNode(clause);
+ Trace("cnf") << "Node equivalent: " << clauseNode << "\n";
+ Assert(clLevel < (userContext()->getLevel() - 1));
+ // As above, also justify eagerly.
+ std::shared_ptr<ProofNode> clauseCnfPf =
+ d_env.getProofNodeManager()->clone(d_proof.getProofFor(clauseNode));
+ Assert(clauseCnfPf->getRule() != PfRule::ASSUME);
+ d_optClausesPfs[clLevel + 1].push_back(clauseCnfPf);
+}
Node ProofCnfStream::getClauseNode(const SatClause& clause)
{
#include "proof/proof_node_manager.h"
#include "proof/theory_proof_step_buffer.h"
#include "prop/cnf_stream.h"
+#include "prop/opt_clauses_manager.h"
#include "prop/sat_proof_manager.h"
#include "smt/env_obj.h"
* generator. */
bool isBlocked(std::shared_ptr<ProofNode> pfn);
+ /** Notify that current propagation inserted at lower level than current.
+ *
+ * The proof of the current propagation (d_currPropagationProccessed) will be
+ * saved in d_optClausesPfs, so that it is not potentially lost when the user
+ * context is popped.
+ */
+ void notifyCurrPropagationInsertedAtLevel(int explLevel);
+ /** Notify that added clause was inserted at lower level than current.
+ *
+ * As above, the proof of this clause is saved in d_optClausesPfs.
+ */
+ void notifyClauseInsertedAtLevel(const SatClause& clause, int clLevel);
+
private:
/**
* Same as above, except that uses the saved d_removable flag. It calls the
* These are proof nodes added to this class by external generators. */
context::CDHashSet<std::shared_ptr<ProofNode>, ProofNodeHashFunction>
d_blocked;
+
+ /** The current propagation being processed via this class. */
+ Node d_currPropagationProccessed;
+ /** User-context-dependent map assertion level to proof nodes.
+ *
+ * This map is used to update the internal proof of this class when the
+ * context pops.
+ */
+ std::map<int, std::vector<std::shared_ptr<ProofNode>>> d_optClausesPfs;
+ /** Manager for optimized propagations and added clauses inserted at assertion
+ * levels below the current user level. */
+ OptimizedClausesManager d_optClausesManager;
};
} // namespace prop
void theoryCheck(theory::Theory::Effort effort);
+ /** Get an explanation for literal `l` and save it on clause `explanation`. */
void explainPropagation(SatLiteral l, SatClause& explanation);
+ /** Notify that current propagation inserted at lower level than current.
+ *
+ * This method should be called by the SAT solver when the explanation of the
+ * current propagation is added at lower level than the current user level.
+ * It'll trigger a call to the ProofCnfStream to notify it that the proof of
+ * this propagation should be saved in case it's needed after this user
+ * context is popped.
+ */
+ void notifyCurrPropagationInsertedAtLevel(int explLevel);
+ /** Notify that added clause was inserted at lower level than current.
+ *
+ * As above, but for clauses asserted into the SAT solver. This cannot be done
+ * in terms of "current added clause" because the clause added at a lower
+ * level could be for example a lemma derived at a prior moment whose
+ * assertion the SAT solver delayed.
+ */
+ void notifyClauseInsertedAtLevel(const SatClause& clause, int clLevel);
void theoryPropagate(SatClause& output);
projects / cvc5.git / commitdiff