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/uf/proof_equality_engine.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/uf/proof_equality_engine.h')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 314353131..e1105623a 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -180,6 +180,8 @@ class ProofEqEngine : public EagerProofGenerator const std::vector<Node>& args); /** Multi-step version */ TrustNode assertConflict(const std::vector<Node>& exp, ProofStepBuffer& psb); + /** Generator version, where pg has a proof of false from assumptions exp */ + TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg); //-------------------------- assert lemma /** * Called when we have concluded conc, typically via theory specific |