diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-10-09 05:55:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-09 07:55:14 -0500 |
commit | 5fd55819da2ea6fdf0472f2e212330d09c4b5317 (patch) | |
tree | 826c5f9ee804a7ac19ea51242667edc7a76dcfe1 /src/theory/arith/constraint.h | |
parent | 36addc33791da4b1fbae9fbcec87ac26cfc7a270 (diff) |
(proof-new) proofs for arith-constraint explanations (#5224)
Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:
externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 05845ec76..02bc3c988 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -553,9 +553,7 @@ class Constraint { * This is the minimum fringe of the implication tree s.t. * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). */ - Node externalExplainByAssertions() const { - return externalExplain(AssertionOrderSentinel); - } + TrustNode externalExplainByAssertions() const; /** * Writes an explanation of a constraint into the node builder. @@ -598,22 +596,19 @@ class Constraint { * The constraint must have a proof. * The constraint cannot be an assumption. * - * This is the minimum fringe of the implication tree (excluding the constraint itself) - * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof(). + * This is the minimum fringe of the implication tree (excluding the + * constraint itself) s.t. every constraint is assertedToTheTheory() or + * hasEqualityEngineProof(). + * + * All return conjuncts were asserted before this constraint. */ - Node externalExplainForPropagation() const { - Assert(hasProof()); - Assert(!isAssumption()); - Assert(!isInternalAssumption()); - return externalExplain(d_assertionOrder); - } + TrustNode externalExplainForPropagation() const; /** * Explain the constraint and its negation in terms of assertions. * The constraint must be in conflict. */ - Node externalExplainConflict() const; - + TrustNode externalExplainConflict() const; /** The constraint is known to be true. */ inline bool hasProof() const { @@ -1155,7 +1150,11 @@ private: bool variableDatabaseIsSetup(ArithVar v) const; void removeVariable(ArithVar v); + /** Get an explanation and proof for this constraint from the equality engine + */ TrustNode eeExplain(ConstraintCP c) const; + /** Get an explanation for this constraint from the equality engine */ + void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; /** * Returns a constraint with the variable v, the constraint type t, and a value |