diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-06 10:02:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-06 10:02:54 -0500 |
commit | 2d8889f935ca78ef4a5555f0e6bbed76dbc559d7 (patch) | |
tree | 2d83522cd3d1e0d711773a45de0d2be2952dbb7c /src/theory/theory_engine.cpp | |
parent | 6d663abe421c07976755c224180b1a1ee93442f6 (diff) |
(proof-new) Add interface for trusted substitution and update ppAssert (#5193)
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.
This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.
This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 47dca7d66..4722251a3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -823,10 +823,13 @@ void TheoryEngine::shutdown() { d_tpp.clearCache(); } -theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { +theory::Theory::PPAssertStatus TheoryEngine::solve( + TrustNode tliteral, TrustSubstitutionMap& substitutionOut) +{ // Reset the interrupt flag d_interrupted = false; + TNode literal = tliteral.getNode(); TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; @@ -841,7 +844,8 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa throw LogicException(ss.str()); } - Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut); + Theory::PPAssertStatus solveStatus = + theoryOf(atom)->ppAssert(tliteral, substitutionOut); Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; return solveStatus; } |