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/theory/quantifiers/cegqi | |
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/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 118e7023c..8a8678749 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -373,13 +373,20 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { ce_vars.push_back(tutil->getInstantiationConstant(q, i)); } - CegInstantiator* cinst = getInstantiator(q); - LemmaStatus status = - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); - Node ppLem = status.getRewrittenLemma(); + // send the lemma + d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + // get the preprocessed form of the lemma we just sent + std::vector<Node> skolems; + std::vector<Node> skAsserts; + Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm( + lem, skAsserts, skolems); + std::vector<Node> lemp{ppLem}; + lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end()); + ppLem = NodeManager::currentNM()->mkAnd(lemp); Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem << std::endl; std::vector<Node> auxLems; + CegInstantiator* cinst = getInstantiator(q); cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems); for (unsigned i = 0, size = auxLems.size(); i < size; i++) { |