diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-03 19:15:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 19:15:30 -0500 |
commit | a5b834d5af88e372d9c6340653f831a09daf1d39 (patch) | |
tree | 13b998f9887589f9f9d5f0619a0139d982d7e3b8 /src/theory/theory_inference_manager.h | |
parent | 0fe081a56db369372584a5fcd35a4c4e4fb1c23f (diff) |
Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)
This gives theories a finer grained control over explained lemmas and conflicts.
A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.
This is required for the new strings inference manager on proof-new.
This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.
Diffstat (limited to 'src/theory/theory_inference_manager.h')
-rw-r--r-- | src/theory/theory_inference_manager.h | 52 |
1 files changed, 49 insertions, 3 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 080a09ba8..92116648e 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -77,6 +77,11 @@ class TheoryInferenceManager */ void setEqualityEngine(eq::EqualityEngine* ee); /** + * Are proofs enabled in this inference manager? Returns true if the proof + * node manager pnm provided to the constructor of this class was non-null. + */ + bool isProofEnabled() const; + /** * Reset, which resets counters regarding the number of added lemmas and * internal facts. This method should be manually called by the theory at * the appropriate time for the purpose of tracking the usage of this @@ -127,7 +132,7 @@ class TheoryInferenceManager void conflict(TNode conf); /** * Raise trusted conflict tconf (of any form) where a proof generator has - * been provided in a custom way. + * been provided (as part of the trust node) in a custom way. */ void trustedConflict(TrustNode tconf); /** @@ -140,6 +145,29 @@ class TheoryInferenceManager void conflictExp(PfRule id, const std::vector<Node>& exp, const std::vector<Node>& args); + /** + * Make the trust node corresponding to the conflict of the above form. It is + * the responsibility of the caller to subsequently call trustedConflict with + * the returned trust node. + */ + TrustNode mkConflictExp(PfRule id, + const std::vector<Node>& exp, + const std::vector<Node>& args); + /** + * Explain and send conflict from contradictory facts. This method is called + * when proof generator pg has a proof of false from free assumptions exp. + * This method sends a trusted conflict corresponding to the official + * equality engine's explanation of literals in exp, with the proof equality + * engine as the proof generator (if it exists), where pg provides the + * final step(s) of this proof during this call. + */ + void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg); + /** + * Make the trust node corresponding to the conflict of the above form. It is + * the responsibility of the caller to subsequently call trustedConflict with + * the returned trust node. + */ + TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg); //--------------------------------------- lemmas /** * Send (trusted) lemma lem with property p on the output channel. @@ -191,9 +219,19 @@ class TheoryInferenceManager LemmaProperty p = LemmaProperty::NONE, bool doCache = true); /** + * Make the trust node for the above method. It is responsibility of the + * caller to subsequently call trustedLemma with the returned trust node. + */ + TrustNode mkLemmaExp(Node conc, + PfRule id, + const std::vector<Node>& exp, + const std::vector<Node>& noExplain, + const std::vector<Node>& args); + /** * Same as above, but where pg can provide a proof of conc from free - * assumptions in exp. It is required to do so in the remainder of the user - * context when this method returns true. + * assumptions in exp. This sends a trusted lemma on the output channel where + * the proof equality engine is the proof generator. The generator pg + * is asked to provide the final step(s) of this proof during this call. * * @param conc The conclusion of the lemma * @param exp The set of (all) literals that imply conc @@ -211,6 +249,14 @@ class TheoryInferenceManager LemmaProperty p = LemmaProperty::NONE, bool doCache = true); /** + * Make the trust node for the above method. It is responsibility of the + * caller to subsequently call trustedLemma with the returned trust node. + */ + TrustNode mkLemmaExp(Node conc, + const std::vector<Node>& exp, + const std::vector<Node>& noExplain, + ProofGenerator* pg = nullptr); + /** * Has this inference manager cached and sent the given lemma (in this user * context)? This method can be overridden by the particular manager. If not, * this returns true if lem is in the cache d_lemmasSent maintained by this |