Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof).
This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set.
There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do
not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases.
: context::ContextNotifyObj(context),
d_context(context),
d_optProofs(optProofs),
- d_parentProof(parentProof)
+ d_parentProof(parentProof),
+ d_nodeHashSet(nullptr),
+ d_nodeLevels(nullptr)
{
}
}
it = d_optProofs.erase(it);
}
+ if (d_nodeHashSet)
+ {
+ Assert(d_nodeLevels);
+ // traverse mapping from context levels to nodes so that we can reinsert the
+ // nodes that are below the current level being popped. The entries in the
+ // map at or above this level are deleted.
+ for (auto it = d_nodeLevels->cbegin(); it != d_nodeLevels->cend();)
+ {
+ if (it->first <= newLvl)
+ {
+ Trace("sat-proof") << "Should re-add SAT assumptions of [" << it->first
+ << "]:\n";
+ for (const auto& assumption : it->second)
+ {
+ Trace("sat-proof") << "\t- " << assumption << "\n";
+ // Note that since it's a hash set we do not care about repetitions
+ d_nodeHashSet->insert(assumption);
+ }
+ ++it;
+ continue;
+ }
+ Trace("sat-proof") << "Should remove from map assumptions of ["
+ << it->first << "]: " << it->second << "\n";
+ it = d_nodeLevels->erase(it);
+ }
+ }
Trace("sat-proof") << pop;
}
+void OptimizedClausesManager::trackNodeHashSet(
+ context::CDHashSet<Node>* nodeHashSet,
+ std::map<int, std::vector<Node>>* nodeLevels)
+{
+ d_nodeHashSet = nodeHashSet;
+ d_nodeLevels = nodeLevels;
+}
+
} // namespace prop
} // namespace cvc5::internal
#define CVC5__PROP__OPT_CLAUSES_MANAGER_H
#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
#include "expr/node.h"
#include "proof/proof.h"
CDProof* parentProof,
std::map<int, std::vector<std::shared_ptr<ProofNode>>>& optProofs);
+ /** Adds a hash set of nodes to be tracked and updated when popping
+ *
+ * This method can be used when it is necessary to track, in a
+ * context-dependent manner, other information, in a node hash set, beyond the
+ * proofs associated with given clauses. For example, the SAT proof manager
+ * needs to bookeep the current assumptions of the SAT solver, which are
+ * stored in a node hash set.
+ *
+ * @param nodeHashSet the node hash set to be updated when context pops
+ * @param nodeLevels a mapping from context levels to nodes to be reinserted
+ * at these levels
+ */
+ void trackNodeHashSet(context::CDHashSet<Node>* nodeHashSet,
+ std::map<int, std::vector<Node>>* nodeLevels);
+
private:
/** Event triggered by the tracked contexting popping
*
std::map<int, std::vector<std::shared_ptr<ProofNode>>>& d_optProofs;
/** Proof to be updated when context pops. */
CDProof* d_parentProof;
+ /** Node hash set to be updated when context pops, if such a set is tracked */
+ context::CDHashSet<Node>* d_nodeHashSet;
+ /** Map from levels to proof nodes. */
+ std::map<int, std::vector<Node>>* d_nodeLevels;
};
} // namespace prop
Trace("cnf-debug") << "\t..saved pf {" << currPropagationProcPf << "} "
<< *currPropagationProcPf.get() << "\n";
d_optClausesPfs[explLevel + 1].push_back(currPropagationProcPf);
-
+ // Notify SAT proof manager that the propagation (which is a SAT assumption)
+ // had its level optimized
+ d_satPM->notifyAssumptionInsertedAtLevel(explLevel,
+ d_currPropagationProccessed);
+ // Reset
d_currPropagationProccessed = Node::null();
}
d_env.getProofNodeManager()->clone(d_proof.getProofFor(clauseNode));
Assert(clauseCnfPf->getRule() != PfRule::ASSUME);
d_optClausesPfs[clLevel + 1].push_back(clauseCnfPf);
+ // Notify SAT proof manager that the propagation (which is a SAT assumption)
+ // had its level optimized
+ d_satPM->notifyAssumptionInsertedAtLevel(clLevel, clauseNode);
}
Node ProofCnfStream::getClauseNode(const SatClause& clause)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
+ d_optResManager.trackNodeHashSet(&d_assumptions, &d_assumptionLevels);
}
void SatProofManager::printClause(const Minisat::Clause& clause)
}
}
+void SatProofManager::notifyAssumptionInsertedAtLevel(int level,
+ Node assumption)
+{
+ Assert(d_assumptions.contains(assumption));
+ d_assumptionLevels[level].push_back(assumption);
+}
+
void SatProofManager::notifyPop()
{
for (context::CDHashMap<Node, int>::const_iterator it =
++it)
{
// Save into map the proof of the resolution chain. We copy to prevent the
- // proof node saved to be restored to suffering unintended updates. This is
+ // proof node saved to be restored of suffering unintended updates. This is
// *necessary*.
std::shared_ptr<ProofNode> clauseResPf =
d_env.getProofNodeManager()->clone(d_resChains.getProofFor(it->first));
/** Notify this proof manager that the SAT solver has user-context popped. */
void notifyPop();
+ /** Notify this proof manager that a SAT assumption has had its level
+ * optmized. */
+ void notifyAssumptionInsertedAtLevel(int level, Node assumption);
+
private:
/** Ends resolution chain concluding clause
*
* - <(or ~l6 l7), l6>
* - <(or l4 ~l7), l7>
*
- * The resulting children and arguments for the CHAIN_RESOLUTION proof step would be:
+ * The resulting children and arguments for the CHAIN_RESOLUTION proof step
+ * would be:
* - [(or l3 l5 l6 l7), ~l5, (or ~l6 l7), (or l4 ~l7)]
* - [l5, l6, l7]
* and the proof step
* manager when the context pops.
*/
std::map<int, std::vector<std::shared_ptr<ProofNode>>> d_optResProofs;
+ /** Maps assertion level to assumptions
+ *
+ * As above, used by d_optResManager to update the assumption set as the
+ * context pops, so that we track the correct current SAT assumptions.
+ */
+ std::map<int, std::vector<Node>> d_assumptionLevels;
/** Manager for optimized resolution conclusions inserted at assertion levels
* below the current user level. */
OptimizedClausesManager d_optResManager;
regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2
regress0/proofs/scope.smt2
+ regress0/proofs/tricky-sat-assumption-incremental-bookeeping.smt2
regress0/proofs/trust-subs-eq-open.smt2
regress0/push-pop/boolean/fuzz_12.smt2
regress0/push-pop/boolean/fuzz_13.smt2
--- /dev/null
+; COMMAND-LINE: -i --produce-proofs --proof-check=eager
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_UFLIA)
+(declare-fun x (Int) Bool)
+(declare-fun y (Int) Bool)
+(declare-fun z (Int) Int)
+(declare-fun _z (Int) Int)
+(assert (= (x 0) (not (y 0))))
+(assert (= (y 0) (> 0 (z 0))))
+(assert (= (z 0) (_z 0)))
+(assert (= 0 (_z 0)))
+(push)
+(check-sat)
+(pop)
+(assert (not (x 0)))
+(check-sat)
projects / cvc5.git / commitdiff