diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-21 21:21:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-21 21:21:42 -0500 |
commit | 0e7ebfa3ba5d5049c81b2c5ac113af62c35f5c64 (patch) | |
tree | c5a9d62c560592003f9fd0003faece8585c7c30a /src/theory/theory_engine.cpp | |
parent | a99f5aaa46702a4894aaddeed3a7ff5cbf69bdfd (diff) |
(proof-new) Make theory preprocessor user-context dependent (#5296)
Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.
This PR also makes the theory preprocess pass proof producing.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 20 |
1 files changed, 5 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 924d045da..706149d86 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -251,7 +251,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_tpp(*this, iteRemover, d_pnm), + d_tpp(*this, iteRemover, userContext, d_pnm), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), @@ -824,8 +824,6 @@ void TheoryEngine::shutdown() { theoryOf(theoryId)->shutdown(); } } - - d_tpp.clearCache(); } theory::Theory::PPAssertStatus TheoryEngine::solve( @@ -855,18 +853,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } -void TheoryEngine::preprocessStart() { d_tpp.clearCache(); } - -Node TheoryEngine::preprocess(TNode assertion) +TrustNode TheoryEngine::preprocess(TNode assertion) { - TrustNode trn = d_tpp.theoryPreprocess(assertion); - if (trn.isNull()) - { - // no change - return assertion; - } - // notice that we could alternatively return the trust node here. - return trn.getNode(); + return d_tpp.theoryPreprocess(assertion); } void TheoryEngine::notifyPreprocessedAssertions( @@ -1147,7 +1136,8 @@ Node TheoryEngine::ensureLiteral(TNode n) { Debug("ensureLiteral") << "rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); Debug("ensureLiteral") << " got: " << rewritten << std::endl; - Node preprocessed = preprocess(rewritten); + TrustNode tp = preprocess(rewritten); + Node preprocessed = tp.isNull() ? rewritten : tp.getNode(); Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl; d_propEngine->ensureLiteral(preprocessed); return preprocessed; |