diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-31 23:35:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-31 21:35:57 -0700 |
commit | 9b7f2b6b541f192acf2dc525076a4aa0e995be14 (patch) | |
tree | e4773cdf7a312e90eeaa850d412b05a53ebd942c /src/theory/theory_inference_manager.cpp | |
parent | fa05eb5599e2ac0b2d4c1e0e943fee6353b52430 (diff) |
Add the inference manager for datatypes (#4968)
This is in preparation for converting datatypes to the new standard. It adds a specialized version of inference manager buffered that datatypes uses. This required adding several utility methods to its base classes.
A follow up PR will connect this to TheoryDatatypes.
Diffstat (limited to 'src/theory/theory_inference_manager.cpp')
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 68 |
1 files changed, 62 insertions, 6 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index a42c33814..20c1fbf37 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -30,7 +30,10 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_out(t.getOutputChannel()), d_ee(nullptr), d_pnm(pnm), - d_keep(t.getSatContext()) + d_keep(t.getSatContext()), + d_lemmasSent(t.getUserContext()), + d_numCurrentLemmas(0), + d_numCurrentFacts(0) { } @@ -47,6 +50,12 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) } } +void TheoryInferenceManager::reset() +{ + d_numCurrentLemmas = 0; + d_numCurrentFacts = 0; +} + void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) { if (!d_theoryState.isInConflict()) @@ -125,15 +134,41 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a, << " mkTrustedConflictEqConstantMerge"; } -LemmaStatus TheoryInferenceManager::lemma(TNode lem, LemmaProperty p) +bool TheoryInferenceManager::lemma(TNode lem, LemmaProperty p, bool doCache) +{ + TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr); + return trustedLemma(tlem, p, doCache); +} + +bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, + LemmaProperty p, + bool doCache) +{ + if (doCache) + { + if (!cacheLemma(tlem.getNode(), p)) + { + return false; + } + } + d_numCurrentLemmas++; + d_out.trustedLemma(tlem, p); + return true; +} + +bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) +{ + return d_lemmasSent.find(lem) != d_lemmasSent.end(); +} + +uint32_t TheoryInferenceManager::numAddedLemmas() const { - return d_out.lemma(lem, p); + return d_numCurrentLemmas; } -LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem, - LemmaProperty p) +bool TheoryInferenceManager::hasAddedLemma() const { - return d_out.trustedLemma(tlem, p); + return d_numCurrentLemmas != 0; } void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp) @@ -178,6 +213,7 @@ void TheoryInferenceManager::processInternalFact(TNode atom, Assert(d_ee != nullptr); Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: " << expn << std::endl; + d_numCurrentFacts++; // Now, assert the fact. How to do so depends on whether proofs are enabled. // If no proof production, or no proof rule was given if (d_pfee == nullptr || id == PfRule::UNKNOWN) @@ -244,5 +280,25 @@ Node TheoryInferenceManager::mkExplain(TNode n) return NodeManager::currentNM()->mkAnd(assumptions); } +uint32_t TheoryInferenceManager::numAddedFacts() const +{ + return d_numCurrentFacts; +} + +bool TheoryInferenceManager::hasAddedFact() const +{ + return d_numCurrentFacts != 0; +} + +bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p) +{ + if (d_lemmasSent.find(lem) != d_lemmasSent.end()) + { + return false; + } + d_lemmasSent.insert(lem); + return true; +} + } // namespace theory } // namespace CVC4 |