diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-23 19:12:32 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-23 19:12:32 -0600 |
commit | 854ab7e1adce90ebd822cc29ffabf5546d13f5cc (patch) | |
tree | 96bcb318ada0448c73d293c0b99db7b98eb1e4c4 /src/theory/valuation.cpp | |
parent | 4c0dbb8ec7871ff114a9e66233cd8c8dd853f0b4 (diff) |
Add interface to TheoryState for sort inference and facts (#5967)
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 1926c836e..0dd576a04 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -124,6 +124,15 @@ TheoryModel* Valuation::getModel() { } return d_engine->getModel(); } +SortInference* Valuation::getSortInference() +{ + if (d_engine == nullptr) + { + // no theory engine, thus we don't have a sort inference object + return nullptr; + } + return d_engine->getSortInference(); +} void Valuation::setUnevaluatedKind(Kind k) { @@ -198,5 +207,18 @@ bool Valuation::needCheck() const{ bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); } +context::CDList<Assertion>::const_iterator Valuation::factsBegin(TheoryId tid) +{ + Theory* theory = d_engine->theoryOf(tid); + Assert(theory != nullptr); + return theory->facts_begin(); +} +context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid) +{ + Theory* theory = d_engine->theoryOf(tid); + Assert(theory != nullptr); + return theory->facts_end(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |