From d47a8708171f1cf488fe9ce05f56f2566db53093 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 12 Feb 2021 03:45:29 -0600 Subject: [PATCH] Simplify and fix decision engine's handling of skolem definitions (#5888) This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver. With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to. This also simplifies related interfaces within decision engine. We should test this PR with --decision=justification on SMT-LIB. --- src/decision/decision_engine.cpp | 53 ++------ src/decision/decision_engine.h | 40 ++---- src/decision/decision_strategy.h | 30 ++--- src/decision/justification_heuristic.cpp | 30 ++--- src/decision/justification_heuristic.h | 13 +- src/preprocessing/assertion_pipeline.h | 2 + src/preprocessing/passes/ite_removal.cpp | 2 +- .../passes/theory_preprocess.cpp | 2 +- src/prop/prop_engine.cpp | 119 +++++++++--------- src/prop/prop_engine.h | 48 ++++++- src/prop/theory_proxy.cpp | 6 +- src/smt/smt_solver.cpp | 29 ++++- src/smt/term_formula_removal.h | 2 - 13 files changed, 184 insertions(+), 192 deletions(-) diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index ec8943f4a..e1327c0a7 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -28,17 +28,14 @@ namespace CVC4 { DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc, ResourceManager* rm) - : d_enabledITEStrategy(nullptr), - d_needIteSkolemMap(), - d_relevancyStrategy(nullptr), - d_assertions(uc), - d_cnfStream(nullptr), + : d_cnfStream(nullptr), d_satSolver(nullptr), d_satContext(sc), d_userContext(uc), d_result(sc, SAT_VALUE_UNKNOWN), d_engineState(0), - d_resourceManager(rm) + d_resourceManager(rm), + d_enabledITEStrategy(nullptr) { Trace("decision") << "Creating decision engine" << std::endl; } @@ -58,7 +55,6 @@ void DecisionEngine::init() { d_enabledITEStrategy.reset(new decision::JustificationHeuristic( this, d_userContext, d_satContext)); - d_needIteSkolemMap.push_back(d_enabledITEStrategy.get()); } } @@ -69,7 +65,6 @@ void DecisionEngine::shutdown() Assert(d_engineState == 1); d_engineState = 2; d_enabledITEStrategy.reset(nullptr); - d_needIteSkolemMap.clear(); } SatLiteral DecisionEngine::getNext(bool& stopSearch) @@ -85,49 +80,23 @@ SatLiteral DecisionEngine::getNext(bool& stopSearch) : d_enabledITEStrategy->getNext(stopSearch); } -bool DecisionEngine::isRelevant(SatVariable var) +void DecisionEngine::addAssertion(TNode assertion) { - Debug("decision") << "isRelevant(" << var <<")" << std::endl; - if (d_relevancyStrategy != nullptr) - { - //Assert(d_cnfStream->hasNode(var)); - return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) ); - } - else - { - return true; - } -} - -SatValue DecisionEngine::getPolarity(SatVariable var) -{ - Debug("decision") << "getPolarity(" << var <<")" << std::endl; - if (d_relevancyStrategy != nullptr) - { - Assert(isRelevant(var)); - return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) ); - } - else + // new assertions, reset whatever result we knew + d_result = SAT_VALUE_UNKNOWN; + if (d_enabledITEStrategy != nullptr) { - return SAT_VALUE_UNKNOWN; + d_enabledITEStrategy->addAssertion(assertion); } } -void DecisionEngine::addAssertions(const std::vector& assertions, - const std::vector& ppLemmas, - const std::vector& ppSkolems) +void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; - - for (const Node& assertion : assertions) - { - d_assertions.push_back(assertion); - } - - for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) + if (d_enabledITEStrategy != nullptr) { - d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems); + d_enabledITEStrategy->addSkolemDefinition(lem, skolem); } } diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 15dbf0d79..914636fe9 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -37,12 +37,6 @@ using namespace CVC4::decision; namespace CVC4 { class DecisionEngine { - std::unique_ptr d_enabledITEStrategy; - vector d_needIteSkolemMap; - RelevancyStrategy* d_relevancyStrategy; - - typedef context::CDList AssertionsList; - AssertionsList d_assertions; // PropEngine* d_propEngine; CnfStream* d_cnfStream; @@ -105,15 +99,6 @@ class DecisionEngine { /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool& stopSearch); - /** Is a sat variable relevant */ - bool isRelevant(SatVariable var); - - /** - * Try to get tell SAT solver what polarity to try for a - * decision. Return SAT_VALUE_UNKNOWN if it can't help - */ - SatValue getPolarity(SatVariable var); - /** Is the DecisionEngine in a state where it has solved everything? */ bool isDone() { Trace("decision") << "DecisionEngine::isDone() returning " @@ -142,23 +127,18 @@ class DecisionEngine { // External World helping us help the Strategies /** - * Add a list of assertions, as well as lemmas coming from preprocessing - * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). + * Notify this class that assertion is an (input) assertion, not corresponding + * to a skolem definition. */ - void addAssertions(const std::vector& assertions, - const std::vector& ppLemmas, - const std::vector& ppSkolems); - - // Interface for Strategies to use stuff stored in Decision Engine - // (which was possibly requested by them on initialization) - + void addAssertion(TNode assertion); /** - * Get the assertions. Strategies are notified when these are available. + * Notify this class that lem is the skolem definition for skolem, which is + * a part of the current assertions. */ - AssertionsList& getAssertions() { - return d_assertions; - } + void addSkolemDefinition(TNode lem, TNode skolem); + // Interface for Strategies to use stuff stored in Decision Engine + // (which was possibly requested by them on initialization) // Interface for Strategies to get information about External World @@ -177,6 +157,10 @@ class DecisionEngine { Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } + + private: + /** The ITE decision strategy we have allocated */ + std::unique_ptr d_enabledITEStrategy; };/* DecisionEngine class */ }/* CVC4 namespace */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index ebddc659d..5e8adb0b8 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -46,10 +46,6 @@ public: virtual ~DecisionStrategy() { } virtual prop::SatLiteral getNext(bool&) = 0; - - virtual bool needIteSkolemMap() { return false; } - - virtual void notifyAssertionsAvailable() { return; } };/* class DecisionStrategy */ class ITEDecisionStrategy : public DecisionStrategy { @@ -57,28 +53,18 @@ public: ITEDecisionStrategy(DecisionEngine* de, context::Context *c) : DecisionStrategy(de, c) { } - - bool needIteSkolemMap() override { return true; } - /** - * Add a list of assertions, as well as lemmas coming from preprocessing - * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). + * Add that assertion is an (input) assertion, not corresponding to a + * skolem definition. + */ + virtual void addAssertion(TNode assertion) = 0; + /** + * Add that lem is the skolem definition for skolem, which is a part of + * the current assertions. */ - virtual void addAssertions(const std::vector& assertions, - const std::vector& ppLemmas, - const std::vector& ppSkolems) = 0; + virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0; };/* class ITEDecisionStrategy */ -class RelevancyStrategy : public ITEDecisionStrategy { -public: - RelevancyStrategy(DecisionEngine* de, context::Context *c) : - ITEDecisionStrategy(de, c) { - } - - virtual bool isRelevant(TNode n) = 0; - virtual prop::SatValue getPolarity(TNode n) = 0; -};/* class RelevancyStrategy */ - }/* CVC4::decision namespace */ }/* CVC4 namespace */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index afbff18c1..1d0b386e3 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -164,16 +164,8 @@ inline void computeXorIffDesiredValues } } -void JustificationHeuristic::addAssertions(const std::vector& assertions, - const std::vector& ppLemmas, - const std::vector& ppSkolems) +void JustificationHeuristic::addAssertion(TNode assertion) { - Assert(ppSkolems.size() == ppLemmas.size()); - Trace("decision") - << "JustificationHeuristic::addAssertions()" - << " size = " << assertions.size() - << std::endl; - // Save all assertions locally, including the assertions generated by term // removal. We have to make sure that we assign a value to all the Boolean // term variables. To illustrate why this is, consider the case where we have @@ -191,20 +183,14 @@ void JustificationHeuristic::addAssertions(const std::vector& assertions, // assertion to be satisifed. However, we also have to make sure that we pick // a value for `b` that is not in conflict with the other assignments (we can // only choose `b` to be `true` otherwise the model is incorrect). - for (const Node& assertion : assertions) - { - d_assertions.push_back(assertion); - } - - // Save mapping between ite skolems and ite assertions - for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++) - { - Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to " - << ppLemmas[i] << std::endl; - d_skolemAssertions[ppSkolems[i]] = ppLemmas[i]; - } + d_assertions.push_back(assertion); +} - // Automatic weight computation +void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem) +{ + Trace("decision::jh::ite") + << " jh-ite: " << skolem << " maps to " << lem << std::endl; + d_skolemAssertions[skolem] = lem; } SatLiteral JustificationHeuristic::findSplitter(TNode node, diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 81b08f1a6..f4e30417c 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -121,9 +121,16 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions(const std::vector& assertions, - const std::vector& ppLemmas, - const std::vector& ppSkolems) override; + /** + * Notify this class that assertion is an (input) assertion, not corresponding + * to a skolem definition. + */ + void addAssertion(TNode assertion) override; + /** + * Notify this class that lem is the skolem definition for skolem, which is + * a part of the current assertions. + */ + void addSkolemDefinition(TNode lem, TNode skolem) override; private: /* getNext with an option to specify threshold */ diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index fcfce0e87..9d65329b0 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -30,6 +30,8 @@ namespace CVC4 { namespace preprocessing { +using IteSkolemMap = std::unordered_map; + /** * Assertion Pipeline stores a list of assertions modified by preprocessing * passes. It is assumed that all assertions after d_realAssertionsEnd were diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index c8b713894..0a35e32eb 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -54,7 +54,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { - imap[newSkolems[j]] = assertions->size(); + imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) if (options::unsatCores() && !options::proofNew()) diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 50831f585..22ae14762 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -51,7 +51,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { - imap[newSkolems[j]] = assertions->size(); + imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) if (options::unsatCores()) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index da19480f9..e99e11eb2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -171,40 +171,25 @@ theory::TrustNode PropEngine::removeItes( } void PropEngine::notifyPreprocessedAssertions( - const preprocessing::AssertionPipeline& ap) + const std::vector& assertions) { // notify the theory engine of preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); - - // Add assertions to decision engine, which manually extracts what assertions - // corresponded to term formula removal. Note that alternatively we could - // delay all theory preprocessing and term formula removal to this point, in - // which case this method could simply take a vector of Node and not rely on - // assertion pipeline or its ITE skolem map. - std::vector ppLemmas; - std::vector ppSkolems; - for (const std::pair& i : ap.getIteSkolemMap()) - { - Assert(i.second >= ap.getRealAssertionsEnd() && i.second < ap.size()); - ppSkolems.push_back(i.first); - ppLemmas.push_back(ap[i.second]); - } - d_decisionEngine->addAssertions(ap.ref(), ppLemmas, ppSkolems); + d_theoryEngine->notifyPreprocessedAssertions(assertions); } void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; - if (isProofEnabled()) - { - d_pfCnfStream->convertAndAssert(node, false, false, nullptr); - // register in proof manager - d_ppm->registerAssertion(node); - } - else - { - d_cnfStream->convertAndAssert(node, false, false, true); - } + d_decisionEngine->addAssertion(node); + assertInternal(node, false, false, true); +} + +void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) +{ + Assert(!d_inCheckSat) << "Sat solver in solve()!"; + Debug("prop") << "assertFormula(" << node << ")" << endl; + d_decisionEngine->addSkolemDefinition(node, skolem); + assertInternal(node, false, false, true); } void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) @@ -243,42 +228,66 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) } // now, assert the lemmas - assertLemmaInternal(tplemma, removable); - for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) - { - assertLemmaInternal(ppLemmas[i], removable); - } - - // assert to decision engine - if (!removable) - { - // also add to the decision engine, where notice we don't need proofs - std::vector assertions; - assertions.push_back(tplemma.getProven()); - std::vector ppLemmasF; - for (const theory::TrustNode& tnl : ppLemmas) - { - ppLemmasF.push_back(tnl.getProven()); - } - d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); - } + assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable); } -void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable) +void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, + bool removable) { Node node = trn.getNode(); - bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; + Assert(!isProofEnabled() || trn.getGenerator() != nullptr); + assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); +} + +void PropEngine::assertInternal( + TNode node, bool negated, bool removable, bool input, ProofGenerator* pg) +{ // Assert as (possibly) removable if (isProofEnabled()) { - Assert(trn.getGenerator()); - d_pfCnfStream->convertAndAssert( - node, negated, removable, trn.getGenerator()); + d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + // if input, register the assertion + if (input) + { + d_ppm->registerAssertion(node); + } } else { - d_cnfStream->convertAndAssert(node, removable, negated); + d_cnfStream->convertAndAssert(node, removable, negated, input); + } +} +void PropEngine::assertLemmasInternal( + theory::TrustNode trn, + const std::vector& ppLemmas, + const std::vector& ppSkolems, + bool removable) +{ + if (!trn.isNull()) + { + assertTrustedLemmaInternal(trn, removable); + } + for (const theory::TrustNode& tnl : ppLemmas) + { + assertTrustedLemmaInternal(tnl, removable); + } + // assert to decision engine + if (!removable) + { + // also add to the decision engine, where notice we don't need proofs + if (!trn.isNull()) + { + // notify the theory proxy of the lemma + d_decisionEngine->addAssertion(trn.getProven()); + } + Assert(ppSkolems.size() == ppLemmas.size()); + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Node lem = ppLemmas[i].getProven(); + d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]); + } } } @@ -441,10 +450,8 @@ Node PropEngine::getPreprocessedTerm(TNode n) std::vector newSkolems; theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems); // send lemmas corresponding to the skolems introduced by preprocessing n - for (const theory::TrustNode& tnl : newLemmas) - { - assertLemma(tnl, theory::LemmaProperty::NONE); - } + theory::TrustNode trnNull; + assertLemmasInternal(trnNull, newLemmas, newSkolems, false); return tpn.isNull() ? Node(n) : tpn.getNode(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f7561d945..ac90d0c36 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -26,7 +26,6 @@ #include "base/modal_exception.h" #include "expr/node.h" #include "options/options.h" -#include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -127,16 +126,31 @@ class PropEngine /** * Notify preprocessed assertions. This method is called just before the * assertions are asserted to this prop engine. This method notifies the - * decision engine and the theory engine of the assertions in ap. + * theory engine of the given assertions. Notice this vector includes + * both the input formulas and the skolem definitions. */ - void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap); + void notifyPreprocessedAssertions(const std::vector& assertions); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. - * The formula is asserted permanently for the current context. + * The formula is asserted permanently for the current context. Note the + * formula should correspond to an input formula and not a lemma introduced + * by term formula removal (which instead should use the interface below). * @param node the formula to assert */ void assertFormula(TNode node); + /** + * Same as above, but node corresponds to the skolem definition of the given + * skolem. + * @param node the formula to assert + * @param skolem the skolem that this lemma defines. + * + * For example, if k is introduced by ITE removal of (ite C x y), then node + * is the formula (ite C (= k x) (= k y)). It is important to distinguish + * these kinds of lemmas from input assertions, as the justification decision + * heuristic treates them specially. + */ + void assertSkolemDefinition(TNode node, TNode skolem); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -304,7 +318,31 @@ class PropEngine * @param removable whether this lemma can be quietly removed based * on an activity heuristic */ - void assertLemmaInternal(theory::TrustNode trn, bool removable); + void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable); + /** + * Assert node as a formula to the CNF stream + * @param node The formula to assert + * @param negated Whether to assert the negation of node + * @param removable Whether the formula is removable + * @param input Whether the formula came from the input + * @param pg Pointer to a proof generator that can provide a proof of node + * (or its negation if negated is true). + */ + void assertInternal(TNode node, + bool negated, + bool removable, + bool input, + ProofGenerator* pg = nullptr); + /** + * Assert lemmas internal, where trn is a trust node corresponding to a + * formula to assert to the CNF stream, ppLemmas and ppSkolems are the + * skolem definitions and skolems obtained from preprocessing it, and + * removable is whether the lemma is removable. + */ + void assertLemmasInternal(theory::TrustNode trn, + const std::vector& ppLemmas, + const std::vector& ppSkolems, + bool removable); /** * Indicates that the SAT solver is currently solving something and we should diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 06e729714..beb2651bf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -156,16 +156,14 @@ void TheoryProxy::spendResource(ResourceManager::Resource r) d_theoryEngine->spendResource(r); } -bool TheoryProxy::isDecisionRelevant(SatVariable var) { - return d_decisionEngine->isRelevant(var); -} +bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; } bool TheoryProxy::isDecisionEngineDone() { return d_decisionEngine->isDone(); } SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { - return d_decisionEngine->getPolarity(var); + return SAT_VALUE_UNKNOWN; } CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 83f2146f4..996a51e90 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -226,11 +226,11 @@ void SmtSolver::processAssertions(Assertions& as) // process the assertions with the preprocessor bool noConflict = d_pp.process(as); - // Push the formula to decision engine + // Notify the input formulas to theory engine if (noConflict) { - Chat() << "notifying theory engine and decision engine..." << std::endl; - d_propEngine->notifyPreprocessedAssertions(ap); + Chat() << "notifying theory engine..." << std::endl; + d_propEngine->notifyPreprocessedAssertions(ap.ref()); } // end: INVARIANT to maintain: no reordering of assertions or @@ -240,10 +240,27 @@ void SmtSolver::processAssertions(Assertions& as) { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime); - for (const Node& assertion : ap.ref()) + const std::vector& assertions = ap.ref(); + // It is important to distinguish the input assertions from the skolem + // definitions, as the decision justification heuristic treates the latter + // specially. + preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap(); + preprocessing::IteSkolemMap::iterator it; + for (size_t i = 0, asize = assertions.size(); i < asize; i++) { - Chat() << "+ " << assertion << std::endl; - d_propEngine->assertFormula(assertion); + // is the assertion a skolem definition? + it = ism.find(i); + if (it == ism.end()) + { + Chat() << "+ input " << assertions[i] << std::endl; + d_propEngine->assertFormula(assertions[i]); + } + else + { + Chat() << "+ skolem definition " << assertions[i] << " (from " + << it->second << ")" << std::endl; + d_propEngine->assertSkolemDefinition(assertions[i], it->second); + } } } diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 54dc488bf..803021fc3 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -34,8 +34,6 @@ namespace CVC4 { -typedef std::unordered_map IteSkolemMap; - class RemoveTermFormulas { public: RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr); -- 2.30.2