diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-01-25 20:20:58 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-25 22:20:58 -0600 |
commit | 909a0aa67266d7659decf56f2e6eb8101a802d45 (patch) | |
tree | b435672d7efe2649ce36f43d2c3844ed44cf0304 | |
parent | eaad5bdc7a38fcc38baa0e3b73f6c39a0ec6fb05 (diff) |
Add proofs to TheoryArithPrivate::propagate (#5812)
Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 52 |
1 files changed, 47 insertions, 5 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index f905c971b..d51efa707 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4028,12 +4028,54 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { outputPropagate(toProp); }else if(constraint->negationHasProof()){ - Node exp = d_congruenceManager.explain(toProp).getNode(); - Node notNormalized = normalized.getKind() == NOT ? - normalized[0] : normalized.notNode(); - Node lp = flattenAnd(exp.andNode(notNormalized)); + // The congruence manager can prove: antecedents => toProp, + // ergo. antecedents ^ ~toProp is a conflict. + TrustNode exp = d_congruenceManager.explain(toProp); + Node notNormalized = normalized.negate(); + std::vector<Node> ants(exp.getNode().begin(), exp.getNode().end()); + ants.push_back(notNormalized); + Node lp = safeConstructNary(kind::AND, ants); Debug("arith::prop") << "propagate conflict" << lp << endl; - raiseBlackBoxConflict(lp); + if (proofsEnabled()) + { + // Assume all of antecedents and ~toProp (rewritten) + std::vector<Pf> pfAntList; + for (size_t i = 0; i < ants.size(); ++i) + { + pfAntList.push_back(d_pnm->mkAssume(ants[i])); + } + Pf pfAnt = pfAntList.size() > 1 + ? d_pnm->mkNode(PfRule::AND_INTRO, pfAntList, {}) + : pfAntList[0]; + // Use modus ponens to get toProp (un rewritten) + Pf pfConc = d_pnm->mkNode( + PfRule::MODUS_PONENS, + {pfAnt, exp.getGenerator()->getProofFor(exp.getProven())}, + {}); + // prove toProp (rewritten) + Pf pfConcRewritten = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pfConc}, {normalized}); + Pf pfNotNormalized = d_pnm->mkAssume(notNormalized); + // prove bottom from toProp and ~toProp + Pf pfBot; + if (normalized.getKind() == kind::NOT) + { + pfBot = d_pnm->mkNode( + PfRule::CONTRA, {pfNotNormalized, pfConcRewritten}, {}); + } + else + { + pfBot = d_pnm->mkNode( + PfRule::CONTRA, {pfConcRewritten, pfNotNormalized}, {}); + } + // close scope + Pf pfNotAnd = d_pnm->mkScope(pfBot, ants); + raiseBlackBoxConflict(lp, pfNotAnd); + } + else + { + raiseBlackBoxConflict(lp); + } outputConflicts(); return; }else{ |