diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 14:01:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-28 14:01:26 -0600 |
commit | e234ff58f561ac97642df15c698962faa9d1e5e4 (patch) | |
tree | cfac18adaeb0fccc348b81e84c854400d38a01fe /src/prop/theory_proxy.cpp | |
parent | 3234db430074e278258e6d687c07146a59769a92 (diff) |
Simplify lemma interface (#5819)
This makes it so that TheoryEngine::lemma returns void not LemmaStatus.
Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.
It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index c604c47f7..a6d570bc2 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -194,6 +194,20 @@ theory::TrustNode TheoryProxy::removeItes( return rtf.run(node, newLemmas, newSkolems, true); } +void TheoryProxy::getSkolems(TNode node, + std::vector<theory::TrustNode>& skAsserts, + std::vector<Node>& sks) +{ + RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); + std::unordered_set<Node, NodeHashFunction> skolems; + rtf.getSkolems(node, skolems); + for (const Node& k : skolems) + { + sks.push_back(k); + skAsserts.push_back(rtf.getLemmaForSkolem(k)); + } +} + void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } }/* CVC4::prop namespace */ |