With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.
No significant behavior changes in this PR.
The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.
IteSkolemMap& imap = assertions->getIteSkolemMap();
// Remove all of the ITE occurrences and normalize
- theory::TheoryPreprocessor* tpp =
- d_preprocContext->getTheoryEngine()->getTheoryPreprocess();
+ prop::PropEngine* pe = d_preprocContext->getPropEngine();
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
Node assertion = (*assertions)[i];
std::vector<theory::TrustNode> newAsserts;
std::vector<Node> newSkolems;
- // TODO (project #42): this will call the prop engine
- TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false);
+ TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false);
if (!trn.isNull())
{
// process
: PreprocessingPass(preprocContext, "theory-preprocess"){};
PreprocessingPassResult TheoryPreprocess::applyInternal(
- AssertionPipeline* assertionsToPreprocess)
+ AssertionPipeline* assertions)
{
- TheoryEngine* te = d_preprocContext->getTheoryEngine();
- for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+
+ IteSkolemMap& imap = assertions->getIteSkolemMap();
+ PropEngine* propEngine = d_preprocContext->getPropEngine();
+ // Remove all of the ITE occurrences and normalize
+ for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
- TNode a = (*assertionsToPreprocess)[i];
- Assert(Rewriter::rewrite(a) == a);
- assertionsToPreprocess->replaceTrusted(i, te->preprocess(a));
- a = (*assertionsToPreprocess)[i];
- Assert(Rewriter::rewrite(a) == a);
+ Node assertion = (*assertions)[i];
+ std::vector<theory::TrustNode> newAsserts;
+ std::vector<Node> newSkolems;
+ TrustNode trn =
+ propEngine->preprocess(assertion, newAsserts, newSkolems, true);
+ if (!trn.isNull())
+ {
+ // process
+ assertions->replaceTrusted(i, trn);
+ // rewritten assertion has a dependence on the node (old pf architecture)
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
+ }
+ }
+ Assert(newSkolems.size() == newAsserts.size());
+ for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+ {
+ imap[newSkolems[j]] = assertions->size();
+ assertions->pushBackTrusted(newAsserts[j]);
+ // new assertions have a dependence on the node (old pf architecture)
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
+ assertion);
+ }
+ }
}
+
return PreprocessingPassResult::NO_CONFLICT;
}
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
#include "util/resource_manager.h"
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::CnfStream(
d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
- d_theoryProxy = new TheoryProxy(
- this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
+
+ d_theoryProxy = new TheoryProxy(this,
+ d_theoryEngine,
+ d_decisionEngine.get(),
+ d_context,
+ userContext,
+ d_cnfStream,
+ pnm);
d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
d_decisionEngine->setSatSolver(d_satSolver);
delete d_theoryProxy;
}
+theory::TrustNode PropEngine::preprocess(
+ TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool doTheoryPreprocess)
+{
+ return d_theoryProxy->preprocess(
+ node, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
void PropEngine::notifyPreprocessedAssertions(
const preprocessing::AssertionPipeline& ap)
{
void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << endl;
- // Assert as non-removable
if (isProofEnabled())
{
d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
}
}
-void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
+Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
{
- Node node = trn.getNode();
- bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
- Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
- // Assert as (possibly) removable
- if (isProofEnabled())
+ bool removable = isLemmaPropertyRemovable(p);
+ bool preprocess = isLemmaPropertyPreprocess(p);
+
+ // call preprocessor
+ std::vector<theory::TrustNode> ppLemmas;
+ std::vector<Node> ppSkolems;
+ theory::TrustNode tplemma =
+ d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess);
+
+ Assert(ppSkolems.size() == ppLemmas.size());
+
+ // do final checks on the lemmas we are about to send
+ if (isProofEnabled() && options::proofNewEagerChecking())
{
- Assert(trn.getGenerator());
- d_pfCnfStream->convertAndAssert(
- node, negated, removable, trn.getGenerator());
+ Assert(tplemma.getGenerator() != nullptr);
+ // ensure closed, make the proof node eagerly here to debug
+ tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+ for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+ {
+ Assert(ppLemmas[i].getGenerator() != nullptr);
+ ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
+ }
}
- else
+
+ if (Trace.isOn("te-lemma"))
{
- d_cnfStream->convertAndAssert(node, removable, negated);
+ Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
+ for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+ {
+ Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
+ << " (skolem is " << ppSkolems[i] << ")" << std::endl;
+ }
}
-}
-void PropEngine::assertLemmas(theory::TrustNode lem,
- std::vector<theory::TrustNode>& ppLemmas,
- std::vector<Node>& ppSkolems,
- bool removable)
-{
- Assert(ppSkolems.size() == ppLemmas.size());
- // assert the lemmas
- assertLemma(lem, removable);
+ // now, assert the lemmas
+ assertLemmaInternal(tplemma, removable);
for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
{
- assertLemma(ppLemmas[i], removable);
+ assertLemmaInternal(ppLemmas[i], removable);
}
// assert to decision engine
{
// also add to the decision engine, where notice we don't need proofs
std::vector<Node> assertions;
- assertions.push_back(lem.getProven());
+ assertions.push_back(tplemma.getProven());
std::vector<Node> ppLemmasF;
for (const theory::TrustNode& tnl : ppLemmas)
{
}
d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
}
+
+ // make the return lemma, which the theory engine will use
+ Node retLemma = tplemma.getProven();
+ if (!ppLemmas.empty())
+ {
+ std::vector<Node> lemmas{retLemma};
+ for (const theory::TrustNode& tnl : ppLemmas)
+ {
+ lemmas.push_back(tnl.getProven());
+ }
+ // the returned lemma is the conjunction of all additional lemmas.
+ retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
+ }
+ return retLemma;
+}
+
+void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
+{
+ Node node = trn.getNode();
+ bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+ Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+ // Assert as (possibly) removable
+ if (isProofEnabled())
+ {
+ Assert(trn.getGenerator());
+ d_pfCnfStream->convertAndAssert(
+ node, negated, removable, trn.getGenerator());
+ }
+ else
+ {
+ d_cnfStream->convertAndAssert(node, removable, negated);
+ }
}
void PropEngine::requirePhase(TNode n, bool phase) {
d_cnfStream->getBooleanVariables(outputVariables);
}
-void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); }
+Node PropEngine::ensureLiteral(TNode n)
+{
+ // must preprocess
+ std::vector<theory::TrustNode> newLemmas;
+ std::vector<Node> newSkolems;
+ theory::TrustNode tpn =
+ d_theoryProxy->preprocess(n, newLemmas, newSkolems, true);
+ // send lemmas corresponding to the skolems introduced by preprocessing n
+ for (const theory::TrustNode& tnl : newLemmas)
+ {
+ Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl;
+ assertLemma(tnl, theory::LemmaProperty::NONE);
+ }
+ Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode();
+ Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
+ << std::endl;
+ d_cnfStream->ensureLiteral(preprocessed);
+ return preprocessed;
+}
void PropEngine::push()
{
*/
void shutdown() {}
+ /**
+ * Preprocess the given node. Return the REWRITE trust node corresponding to
+ * rewriting node. New lemmas and skolems are added to ppLemmas and
+ * ppSkolems respectively.
+ *
+ * @param node The assertion to preprocess,
+ * @param ppLemmas The lemmas to add to the set of assertions,
+ * @param ppSkolems The skolems that newLemmas correspond to,
+ * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+ * @return The (REWRITE) trust node corresponding to rewritten node via
+ * preprocessing.
+ */
+ theory::TrustNode preprocess(TNode node,
+ std::vector<theory::TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems,
+ bool doTheoryPreprocess);
+
/**
* Notify preprocessed assertions. This method is called just before the
* assertions are asserted to this prop engine. This method notifies the
* than the (SAT and SMT) level at which it was asserted.
*
* @param trn the trust node storing the formula to assert
- * @param removable whether this lemma can be quietly removed based
- * on an activity heuristic
+ * @param p the properties of the lemma
+ * @return the (preprocessed) lemma
*/
- void assertLemma(theory::TrustNode trn, bool removable);
-
- /**
- * Assert lemma trn with preprocessing lemmas ppLemmas which correspond
- * to lemmas for skolems in ppSkolems.
- *
- * @param trn the trust node storing the formula to assert
- * @param ppLemmas the lemmas from preprocessing and term formula removal on
- * the proven node of trn
- * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should
- * be the case that ppLemmas.size()==ppSkolems.size().
- * @param removable whether this lemma can be quietly removed based
- * on an activity heuristic
- */
- void assertLemmas(theory::TrustNode trn,
- std::vector<theory::TrustNode>& ppLemmas,
- std::vector<Node>& ppSkolems,
- bool removable);
+ Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
/**
* If ever n is decided upon, it must be in the given phase. This
/**
* Ensure that the given node will have a designated SAT literal
- * that is definitionally equal to it. The result of this function
- * is that the Node can be queried via getSatValue().
+ * that is definitionally equal to it. Note that theory preprocessing is
+ * applied to n. The node returned by this method can be subsequently queried
+ * via getSatValue().
*/
- void ensureLiteral(TNode n);
+ Node ensureLiteral(TNode n);
/**
* Push the context level.
private:
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
+
+ /**
+ * Converts the given formula to CNF and asserts the CNF to the SAT solver.
+ * The formula can be removed by the SAT solver after backtracking lower
+ * than the (SAT and SMT) level at which it was asserted.
+ *
+ * @param trn the trust node storing the formula to assert
+ * @param removable whether this lemma can be quietly removed based
+ * on an activity heuristic
+ */
+ void assertLemmaInternal(theory::TrustNode trn, bool removable);
+
/**
* Indicates that the SAT solver is currently solving something and we should
* not mess with it's internal state.
#include "context/context.h"
#include "decision/decision_engine.h"
#include "options/decision_options.h"
+#include "proof/cnf_proof.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
-#include "proof/cnf_proof.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/statistics_registry.h"
-
namespace CVC4 {
namespace prop {
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream)
+ context::UserContext* userContext,
+ CnfStream* cnfStream,
+ ProofNodeManager* pnm)
: d_propEngine(propEngine),
d_cnfStream(cnfStream),
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
- d_queue(context)
+ d_queue(context),
+ d_tpp(*theoryEngine, userContext, pnm)
{
}
CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
+theory::TrustNode TheoryProxy::preprocessLemma(
+ theory::TrustNode trn,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool doTheoryPreprocess)
+{
+ return d_tpp.preprocessLemma(trn, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
+theory::TrustNode TheoryProxy::preprocess(
+ TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool doTheoryPreprocess)
+{
+ theory::TrustNode pnode =
+ d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess);
+ return pnode;
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
#include <iosfwd>
#include <unordered_set>
+#include "context/cdhashmap.h"
#include "context/cdqueue.h"
#include "expr/node.h"
#include "prop/sat_solver.h"
#include "theory/theory.h"
+#include "theory/theory_preprocessor.h"
+#include "theory/trust_node.h"
#include "util/resource_manager.h"
#include "util/statistics_registry.h"
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream);
+ context::UserContext* userContext,
+ CnfStream* cnfStream,
+ ProofNodeManager* pnm);
~TheoryProxy();
CnfStream* getCnfStream();
+ /**
+ * Call the preprocessor on node, return trust node corresponding to the
+ * rewrite.
+ */
+ theory::TrustNode preprocessLemma(theory::TrustNode trn,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool doTheoryPreprocess);
+ /**
+ * Call the preprocessor on node, return trust node corresponding to the
+ * rewrite.
+ */
+ theory::TrustNode preprocess(TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool doTheoryPreprocess);
+
private:
/** The prop engine we are using. */
PropEngine* d_propEngine;
* all imported and exported lemmas.
*/
std::unordered_set<Node, NodeHashFunction> d_shared;
+
+ /** The theory preprocessor */
+ theory::TheoryPreprocessor d_tpp;
}; /* class TheoryProxy */
}/* CVC4::prop namespace */
// ensure rewritten
d_passes["rewrite"]->apply(&assertions);
- // apply theory preprocess
+ // apply theory preprocess, which includes ITE removal
d_passes["theory-preprocess"]->apply(&assertions);
- // Must remove ITEs again since theory preprocessing may introduce them.
- // Notice that we alternatively could ensure that the theory-preprocess
- // pass above calls TheoryPreprocess::preprocess instead of
- // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal.
- d_passes["ite-removal"]->apply(&assertions);
// This is needed because when solving incrementally, removeITEs may
// introduce skolems that were solved for earlier and thus appear in the
// substitution map.
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_tpp(*this, userContext, d_pnm),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
d_true(),
d_false(),
return solveStatus;
}
-TrustNode TheoryEngine::preprocess(TNode assertion)
-{
- return d_tpp.theoryPreprocess(assertion);
-}
-
void TheoryEngine::notifyPreprocessedAssertions(
const std::vector<Node>& assertions) {
// call all the theories
Node TheoryEngine::ensureLiteral(TNode n) {
Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl;
Node rewritten = Rewriter::rewrite(n);
- Trace("ensureLiteral") << " got: " << rewritten << std::endl;
- std::vector<TrustNode> newLemmas;
- std::vector<Node> newSkolems;
- TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true);
- // send lemmas corresponding to the skolems introduced by preprocessing n
- for (const TrustNode& tnl : newLemmas)
- {
- Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl;
- lemma(tnl, LemmaProperty::NONE);
- }
- Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
- Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
- << std::endl;
- d_propEngine->ensureLiteral(preprocessed);
- return preprocessed;
+ return d_propEngine->ensureLiteral(rewritten);
}
printer.toStreamCmdComment(out, "theory lemma: expect valid");
printer.toStreamCmdCheckSat(out, n);
}
- bool removable = isLemmaPropertyRemovable(p);
- bool preprocess = isLemmaPropertyPreprocess(p);
-
- // ensure closed
- tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
-
- // call preprocessor
- std::vector<TrustNode> newLemmas;
- std::vector<Node> newSkolems;
- TrustNode tplemma =
- d_tpp.preprocessLemma(tlemma, newLemmas, newSkolems, preprocess);
- Assert(newSkolems.size() == newLemmas.size());
+ Node retLemma = d_propEngine->assertLemma(tlemma, p);
// If specified, we must add this lemma to the set of those that need to be
// justified, where note we pass all auxiliary lemmas in lemmas, since these
// by extension must be justified as well.
if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
{
- d_relManager->notifyPreprocessedAssertion(tplemma.getProven());
- for (const theory::TrustNode& tnl : newLemmas)
- {
- d_relManager->notifyPreprocessedAssertion(tnl.getProven());
- }
- }
-
- // do final checks on the lemmas we are about to send
- if (isProofEnabled())
- {
- Assert(tplemma.getGenerator() != nullptr);
- // ensure closed, make the proof node eagerly here to debug
- tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
- for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
- {
- Assert(newLemmas[i].getGenerator() != nullptr);
- newLemmas[i].debugCheckClosed("te-proof-debug",
- "TheoryEngine::lemma_new");
- }
- }
-
- if (Trace.isOn("te-lemma"))
- {
- Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
- for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
- {
- Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
- << " (skolem is " << newSkolems[i] << ")" << std::endl;
- }
+ d_relManager->notifyPreprocessedAssertion(retLemma);
}
- // now, send the lemmas to the prop engine
- d_propEngine->assertLemmas(tplemma, newLemmas, newSkolems, removable);
-
// Mark that we added some lemmas
d_lemmasAdded = true;
- // Lemma analysis isn't online yet; this lemma may only live for this
- // user level.
- Node retLemma = tplemma.getNode();
- if (!newLemmas.empty())
- {
- std::vector<Node> lemmas{retLemma};
- for (const theory::TrustNode& tnl : newLemmas)
- {
- lemmas.push_back(tnl.getProven());
- }
- // the returned lemma is the conjunction of all additional lemmas.
- retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
- }
return theory::LemmaStatus(retLemma, d_userContext->getLevel());
}
/** sort inference module */
SortInference d_sortInfer;
- /** The theory preprocessor */
- theory::TheoryPreprocessor d_tpp;
-
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
bool isProofEnabled() const;
public:
- /**
- * Runs theory specific preprocessing on the non-Boolean parts of
- * the formula. This is only called on input assertions, after ITEs
- * have been removed.
- */
- theory::TrustNode preprocess(TNode node);
- /** Get the theory preprocessor TODO (project #42) remove this */
- theory::TheoryPreprocessor* getTheoryPreprocess() { return &d_tpp; }
/** Notify (preprocessed) assertions. */
void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
bool doTheoryPreprocess);
/**
* Same as above, but transforms the proof of node into a proof of the
- * preprocessed node.
+ * preprocessed node and returns the LEMMA trust node.
*
* @param node The assertion to preprocess,
* @param newLemmas The lemmas to add to the set of assertions,
std::vector<TrustNode>& newLemmas,
std::vector<Node>& newSkolems,
bool doTheoryPreprocess);
+
+ private:
/**
- * Runs theory specific preprocessing on the non-Boolean parts of
- * the formula. This is only called on input assertions, after ITEs
- * have been removed.
+ * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean
+ * parts of the node.
*/
TrustNode theoryPreprocess(TNode node);
-
- private:
/** Reference to owning theory engine */
TheoryEngine& d_engine;
/** Logic info of theory engine */
projects / cvc5.git / commitdiff