This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.
As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.
I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.
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)
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.
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);
}
}
/** 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());
}
// 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
// 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
projects / cvc5.git / commitdiff