diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-10-06 12:15:46 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-06 14:15:46 -0500 |
| commit | e10c381b821337c239479d86fbf1d2eb617c590a (patch) | |
| tree | 042ac35f86a74d7584b5917d1e96d0b6c0b6ad94 /src/theory/arith/constraint.h | |
| parent | 2d8889f935ca78ef4a5555f0e6bbed76dbc559d7 (diff) | |
(proof-new) proofs for ArithCongMan -> ee facts (#5207)
Threads proof production through the ArithCongruenceManager's pipeline
of information to the equality engine.
The idea is to define a method:
ArithCongruenceManager::assertLitToEqualityEngine(literal, reason, pf)
This method asserts a literal to the equality engine with the given
proof and reason. It stores the proof of the literal for the equality
engine's future reference, and is smart about symmetric literals.
This machinery uses proofs that are not closed over the reason, as the
equality engine requires.
Other functions in the pipeline:
assertionToEqualityEngine
equalsCostant
construct proofs and call assertLitToEqualityEngine.
Future commits will address the ee -> ArithCongruenceManager pipeline,
and the relationship between ArithCongruenceManager and the rest of
arithmetic.
Diffstat (limited to 'src/theory/arith/constraint.h')
| -rw-r--r-- | src/theory/arith/constraint.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index f78d8d22f..05845ec76 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -568,8 +568,10 @@ class Constraint { * This is not appropriate for propagation! * Use explainForPropagation() instead. */ - void externalExplainByAssertions(NodeBuilder<>& nb) const{ - externalExplain(nb, AssertionOrderSentinel); + std::shared_ptr<ProofNode> externalExplainByAssertions( + NodeBuilder<>& nb) const + { + return externalExplain(nb, AssertionOrderSentinel); } /* Equivalent to calling externalExplainByAssertions on all constraints in b */ |