diff options
| -rw-r--r-- | src/decision/decision_engine.cpp | 53 | ||||
| -rw-r--r-- | src/decision/decision_engine.h | 40 | ||||
| -rw-r--r-- | src/decision/decision_strategy.h | 30 | ||||
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 30 | ||||
| -rw-r--r-- | src/decision/justification_heuristic.h | 13 | ||||
| -rw-r--r-- | src/preprocessing/assertion_pipeline.h | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 119 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 48 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp | 6 | ||||
| -rw-r--r-- | src/smt/smt_solver.cpp | 29 | ||||
| -rw-r--r-- | 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<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& 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<ITEDecisionStrategy> d_enabledITEStrategy; - vector <ITEDecisionStrategy* > d_needIteSkolemMap; - RelevancyStrategy* d_relevancyStrategy; - - typedef context::CDList<Node> 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<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& 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<ITEDecisionStrategy> 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<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& 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<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& 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<Node>& 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<Node>& assertions, - const std::vector<Node>& ppLemmas, - const std::vector<Node>& 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<size_t, Node>; + /** * 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<Node>& 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<Node> ppLemmas; - std::vector<Node> ppSkolems; - for (const std::pair<const Node, unsigned>& 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<Node> assertions; - assertions.push_back(tplemma.getProven()); - std::vector<Node> 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<theory::TrustNode>& ppLemmas, + const std::vector<Node>& 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<Node> 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<Node>& 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<theory::TrustNode>& ppLemmas, + const std::vector<Node>& 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<Node>& 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<Node, unsigned, NodeHashFunction> IteSkolemMap; - class RemoveTermFormulas { public: RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr); |