From: Alex Ozdemir Date: Wed, 7 Oct 2020 18:48:06 +0000 (-0700) Subject: (proof-new) proofs in ee -> arith pipeline (#5215) X-Git-Tag: cvc5-1.0.0~2739 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d51949548af6df9a18f498de2d424f15988a07b;p=cvc5.git (proof-new) proofs in ee -> arith pipeline (#5215) Threads proofs through the flow of information from the equality engine into the theory of arithmetic. Pretty straightforward. You just have to bundle up information from the EE. --- diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 0c9cb6c9c..e1cb1c3ca 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -172,11 +172,12 @@ RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta) {} /* If you are not an equality engine, don't use this! */ -void RaiseEqualityEngineConflict::raiseEEConflict(Node n) const{ - d_ta.raiseBlackBoxConflict(n); +void RaiseEqualityEngineConflict::raiseEEConflict( + Node n, std::shared_ptr pf) const +{ + d_ta.raiseBlackBoxConflict(n, pf); } - BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta) : d_ta(ta) {} diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 1ce61f46f..796a93ea4 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -19,6 +19,7 @@ #pragma once #include "expr/node.h" +#include "expr/proof_node.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" #include "theory/arith/constraint_forward.h" @@ -177,8 +178,11 @@ private: public: RaiseEqualityEngineConflict(TheoryArithPrivate& ta); - /* If you are not an equality engine, don't use this! */ - void raiseEEConflict(Node n) const; + /* If you are not an equality engine, don't use this! + * + * The proof should prove that `n` is a conflict. + * */ + void raiseEEConflict(Node n, std::shared_ptr pf) const; }; class BoundCountingLookup { diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 404b5bcd0..57214e0f8 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -148,11 +148,13 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1, void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } -void ArithCongruenceManager::raiseConflict(Node conflict){ +void ArithCongruenceManager::raiseConflict(Node conflict, + std::shared_ptr pf) +{ Assert(!inConflict()); Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl; d_inConflict.raise(); - d_raiseConflict.raiseEEConflict(conflict); + d_raiseConflict.raiseEEConflict(conflict, pf); } bool ArithCongruenceManager::inConflict() const{ return d_inConflict.isRaised(); @@ -345,11 +347,22 @@ bool ArithCongruenceManager::propagate(TNode x){ if(rewritten.getConst()){ return true; }else{ + // x rewrites to false. ++(d_statistics.d_conflicts); - - Node conf = flattenAnd(explainInternal(x)); - raiseConflict(conf); + TrustNode trn = explainInternal(x); + Node conf = flattenAnd(trn.getNode()); Debug("arith::congruenceManager") << "rewritten to false "<getProofFor(trn.getProven()); + auto confPf = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {conf.negate()}); + raiseConflict(conf, confPf); + } + else + { + raiseConflict(conf); + } return false; } } @@ -371,9 +384,10 @@ bool ArithCongruenceManager::propagate(TNode x){ << c->negationHasProof() << std::endl; if(c->negationHasProof()){ - Node expC = explainInternal(x); + TrustNode texpC = explainInternal(x); + Node expC = texpC.getNode(); ConstraintCP negC = c->getNegation(); - Node neg = negC->externalExplainByAssertions(); + Node neg = Constraint::externalExplainByAssertions({negC}); Node conf = expC.andNode(neg); Node final = flattenAnd(conf); @@ -443,21 +457,15 @@ void ArithCongruenceManager::enqueueIntoNB(const std::set s, NodeBuilder< } } -Node ArithCongruenceManager::explainInternal(TNode internal){ - std::vector assumptions; - explain(internal, assumptions); - - std::set assumptionSet; - assumptionSet.insert(assumptions.begin(), assumptions.end()); - - if (assumptionSet.size() == 1) { - // All the same, or just one - return assumptions[0]; - }else{ - NodeBuilder<> conjunction(kind::AND); - enqueueIntoNB(assumptionSet, conjunction); - return conjunction; +TrustNode ArithCongruenceManager::explainInternal(TNode internal) +{ + if (isProofEnabled()) + { + return d_pfee->explain(internal); } + // otherwise, explain without proof generator + Node exp = d_ee->mkExplainLit(internal); + return TrustNode::mkTrustPropExp(internal, exp, nullptr); } TrustNode ArithCongruenceManager::explain(TNode external) @@ -465,15 +473,28 @@ TrustNode ArithCongruenceManager::explain(TNode external) Trace("arith-ee") << "Ask for explanation of " << external << std::endl; Node internal = externalToInternal(external); Trace("arith-ee") << "...internal = " << internal << std::endl; - Node exp = explainInternal(internal); - if (isProofEnabled()) + TrustNode trn = explainInternal(internal); + if (isProofEnabled() && trn.getProven()[1] != external) { - Node impl = NodeManager::currentNM()->mkNode(Kind::IMPLIES, exp, external); - // For now, we just trust - auto pfOfImpl = d_pnm->mkNode(PfRule::INT_TRUST, {}, {impl}); - return d_pfGenExplain->mkTrustNode(impl, pfOfImpl); + Assert(trn.getKind() == TrustNodeKind::PROP_EXP); + Assert(trn.getProven().getKind() == Kind::IMPLIES); + Assert(trn.getGenerator() != nullptr); + Trace("arith-ee") << "tweaking proof to prove " << external << " not " + << trn.getProven()[1] << std::endl; + std::vector> assumptionPfs; + std::vector assumptions = andComponents(trn.getNode()); + assumptionPfs.push_back(trn.toProofNode()); + for (const auto& a : assumptions) + { + assumptionPfs.push_back( + d_pnm->mkNode(PfRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {})); + } + auto litPf = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {assumptionPfs}, {external}); + auto extPf = d_pnm->mkScope(litPf, assumptions); + return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf); } - return TrustNode::mkTrustPropExp(external, exp, nullptr); + return trn; } void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 8b9086eb0..3698f46d8 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -129,8 +129,12 @@ private: /** Pointer to the proof equality engine of TheoryArith */ theory::eq::ProofEqEngine* d_pfee; - - void raiseConflict(Node conflict); + /** Raise a conflict node `conflict` to the theory of arithmetic. + * + * When proofs are enabled, a (closed) proof of the conflict should be + * provided. + */ + void raiseConflict(Node conflict, std::shared_ptr pf = nullptr); /** * Are proofs enabled? This is true if a non-null proof manager was provided * to the constructor of this class. @@ -195,8 +199,13 @@ private: void enqueueIntoNB(const std::set all, NodeBuilder<>& nb); - Node explainInternal(TNode internal); -public: + /** + * Determine an explaination for `internal`. That is a conjunction of theory + * literals which imply `internal`. + * + * The TrustNode here is a trusted propagation. + */ + TrustNode explainInternal(TNode internal); public: ArithCongruenceManager(context::Context* satContext, @@ -221,7 +230,12 @@ public: void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee); //--------------------------------- end initialization + /** + * Return the trust node for the explanation of literal. The returned + * trust node is generated by the proof equality engine of this class. + */ TrustNode explain(TNode literal); + void explain(TNode lit, NodeBuilder<>& out); void addWatchedPair(ArithVar s, TNode x, TNode y); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4e4259482..6652d3ee9 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -536,8 +536,17 @@ void TheoryArithPrivate::raiseConflict(ConstraintCP a){ d_conflicts.push_back(a); } -void TheoryArithPrivate::raiseBlackBoxConflict(Node bb){ - if(d_blackBoxConflict.get().isNull()){ +void TheoryArithPrivate::raiseBlackBoxConflict(Node bb, + std::shared_ptr pf) +{ + Debug("arith::bb") << "raiseBlackBoxConflict: " << bb << std::endl; + if (d_blackBoxConflict.get().isNull()) + { + if (options::proofNew()) + { + Debug("arith::bb") << " with proof " << pf << std::endl; + d_blackBoxConflictPf.set(pf); + } d_blackBoxConflict = bb; } } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 5cb281b36..012e45b2f 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -17,9 +17,10 @@ #pragma once +#include + #include #include -#include #include #include "context/cdhashset.h" @@ -57,6 +58,7 @@ #include "theory/eager_proof_generator.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" @@ -329,8 +331,7 @@ private: // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c); /** This is a conflict that is magically known to hold. */ - void raiseBlackBoxConflict(Node bb); - + void raiseBlackBoxConflict(Node bb, std::shared_ptr pf = nullptr); /** * Returns true iff a conflict has been raised. This method is public since * it is needed by the ArithState class to know whether we are in conflict.