diff options
Diffstat (limited to 'src/prop/sat_proof_manager.cpp')
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index da9354c2f..0d075de45 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -35,6 +35,7 @@ SatProofManager::SatProofManager(Minisat::Solver* solver, d_assumptions(userContext), d_conflictLit(undefSatVariable) { + d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } @@ -169,7 +170,6 @@ void SatProofManager::endResChain(Node conclusion, } d_redundantLits.clear(); // build resolution chain - NodeManager* nm = NodeManager::currentNM(); // the conclusion is stored already in the arguments because of the // possibility of reordering std::vector<Node> children, args{conclusion}; @@ -212,7 +212,7 @@ void SatProofManager::endResChain(Node conclusion, Trace("sat-proof") << " : "; if (i > 0) { - args.push_back(nm->mkConst(posFirst)); + args.push_back(posFirst ? d_true : d_false); args.push_back(pivot); Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] "; } @@ -249,7 +249,7 @@ void SatProofManager::endResChain(Node conclusion, // step, which bypasses these. Note that we could generate a chain resolution // rule here by explicitly computing the detailed steps, but leave this for // post-processing. - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(conclusion, ps); // the premises of this resolution may not have been justified yet, so we do // not pass assumptions to check closedness @@ -369,7 +369,6 @@ void SatProofManager::explainLit( // SAT solver, we directly get the literals we need to explain so we no // longer depend on the reference to reason std::vector<Node> toExplain{children.back().begin(), children.back().end()}; - NodeManager* nm = NodeManager::currentNM(); Trace("sat-proof") << push; for (unsigned i = 0; i < size; ++i) { @@ -397,7 +396,7 @@ void SatProofManager::explainLit( // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? currLitNode[0] : currLitNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -429,7 +428,7 @@ void SatProofManager::explainLit( Trace("sat-proof") << pop; // create step args.insert(args.begin(), litNode); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(litNode, ps); // the premises in the limit of the justification may correspond to other // links in the chain which have, themselves, literals yet to be justified. So @@ -490,7 +489,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // get resolution Node cur = link.first; std::shared_ptr<ProofNode> pfn = link.second; - while (pfn->getRule() != PfRule::MACRO_RESOLUTION) + while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST) { Assert(pfn->getChildren().size() == 1 && pfn->getChildren()[0]->getRule() == PfRule::ASSUME) @@ -539,7 +538,6 @@ void SatProofManager::finalizeProof(Node inConflictNode, // arguments for the resolution step to conclude false. std::vector<Node> children{inConflictNode}, args; std::unordered_set<TNode, TNodeHashFunction> premises; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = inConflict.size(); i < size; ++i) { Assert(d_cnfStream->getNodeCache().find(inConflict[i]) @@ -555,7 +553,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? litNode[0] : litNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -578,7 +576,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, } // create step args.insert(args.begin(), d_false); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(d_false, ps); // not yet ready to check closedness because maybe only now we will justify // literals used in resolutions |