diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/prop/prop_engine.cpp | 46 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 34 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp | 18 | ||||
| -rw-r--r-- | src/prop/theory_proxy.h | 3 | ||||
| -rw-r--r-- | src/smt/smt_solver.cpp | 27 |
5 files changed, 43 insertions, 85 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index efe599106..65d20d9a0 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -171,27 +171,35 @@ theory::TrustNode PropEngine::removeItes( return d_theoryProxy->removeItes(node, newLemmas, newSkolems); } -void PropEngine::notifyPreprocessedAssertions( - const std::vector<Node>& assertions) -{ - // notify the theory proxy of preprocessed assertions - d_theoryProxy->notifyPreprocessedAssertions(assertions); -} - -void PropEngine::assertFormula(TNode node) { - Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << std::endl; - // NOTE: we do not notify the theory proxy here, since we've already - // notified the theory proxy during notifyPreprocessedAssertions - assertInternal(node, false, false, true); -} - -void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) +void PropEngine::assertInputFormulas( + const std::vector<Node>& assertions, + std::unordered_map<size_t, Node>& skolemMap) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << std::endl; - d_theoryProxy->notifyAssertion(node, skolem); - assertInternal(node, false, false, true); + // notify the theory engine of preprocessed assertions + d_theoryEngine->notifyPreprocessedAssertions(assertions); + // Now, notify the theory proxy of the assertions and skolem definitions. + // Notice we do this before asserting the formulas to the CNF stream below, + // since (preregistration) lemmas may occur during calls to assertInternal. + // These lemmas we want to be notified about after the theory proxy has + // been notified about all input assertions. + std::unordered_map<size_t, Node>::iterator it; + for (size_t i = 0, asize = assertions.size(); i < asize; i++) + { + // is the assertion a skolem definition? + it = skolemMap.find(i); + Node skolem; + if (it != skolemMap.end()) + { + skolem = it->second; + } + d_theoryProxy->notifyAssertion(assertions[i], skolem); + } + for (const Node& node : assertions) + { + Debug("prop") << "assertFormula(" << node << ")" << std::endl; + assertInternal(node, false, false, true); + } } void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 99c615211..773b27de4 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -111,34 +111,20 @@ class PropEngine theory::TrustNode removeItes(TNode node, std::vector<theory::TrustNode>& ppLemmas, std::vector<Node>& ppSkolems); - /** - * Notify preprocessed assertions. This method is called just before the - * assertions are asserted to this prop engine. This method notifies the - * theory engine of the given assertions. Notice this vector includes - * both the input formulas and the skolem definitions. - */ - 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. 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. + * Converts the given formulas to CNF and assert the CNF to the SAT solver. + * These formulas are asserted permanently for the current context. + * Information about which assertions correspond to skolem definitions is + * contained in skolemMap. * - * 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. + * @param assertions the formulas to assert + * @param skolemMap a map which says which skolem (if any) each assertion + * corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th + * assertion, then skolemMap may contain the entry { i -> k }. */ - void assertSkolemDefinition(TNode node, TNode skolem); + void assertInputFormulas(const std::vector<Node>& assertions, + std::unordered_map<size_t, Node>& skolemMap); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 4a95591b4..e509bf182 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -53,26 +53,16 @@ TheoryProxy::~TheoryProxy() { void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; } -void TheoryProxy::notifyPreprocessedAssertions( - const std::vector<Node>& assertions) -{ - d_theoryEngine->notifyPreprocessedAssertions(assertions); - for (const Node& assertion : assertions) - { - d_decisionEngine->addAssertion(assertion); - } -} - -void TheoryProxy::notifyAssertion(Node lem, TNode skolem) +void TheoryProxy::notifyAssertion(Node a, TNode skolem) { if (skolem.isNull()) { - d_decisionEngine->addAssertion(lem); + d_decisionEngine->addAssertion(a); } else { - d_skdm->notifySkolemDefinition(skolem, lem); - d_decisionEngine->addSkolemDefinition(lem, skolem); + d_skdm->notifySkolemDefinition(skolem, a); + d_decisionEngine->addSkolemDefinition(a, skolem); } } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index e4924ded4..9affec6d0 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -63,9 +63,6 @@ class TheoryProxy : public Registrar /** Finish initialize */ void finishInit(CnfStream* cnfStream); - /** Notify (preprocessed) assertions. */ - void notifyPreprocessedAssertions(const std::vector<Node>& assertions); - /** Notify a lemma, possibly corresponding to a skolem definition */ void notifyAssertion(Node lem, TNode skolem = TNode::null()); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index fbb21034a..3a1c6b12c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -232,14 +232,7 @@ void SmtSolver::processAssertions(Assertions& as) } // process the assertions with the preprocessor - bool noConflict = d_pp.process(as); - - // Notify the input formulas to theory engine - if (noConflict) - { - Chat() << "notifying theory engine..." << std::endl; - d_propEngine->notifyPreprocessedAssertions(ap.ref()); - } + d_pp.process(as); // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -253,23 +246,7 @@ void SmtSolver::processAssertions(Assertions& as) // 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++) - { - // 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); - } - } + d_propEngine->assertInputFormulas(assertions, ism); } // clear the current assertions |