summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/prop_engine.cpp130
-rw-r--r--src/prop/prop_engine.h59
-rw-r--r--src/prop/theory_proxy.cpp30
-rw-r--r--src/prop/theory_proxy.h27
4 files changed, 192 insertions, 54 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a8a92096c..8352373c5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
#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"
@@ -94,8 +95,14 @@ PropEngine::PropEngine(TheoryEngine* te,
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);
@@ -143,6 +150,16 @@ PropEngine::~PropEngine() {
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)
{
@@ -168,7 +185,6 @@ void PropEngine::notifyPreprocessedAssertions(
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);
@@ -181,35 +197,47 @@ void PropEngine::assertFormula(TNode node) {
}
}
-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
@@ -217,7 +245,7 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
{
// 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)
{
@@ -225,6 +253,38 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
}
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) {
@@ -361,7 +421,25 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
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()
{
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 55a42c2a7..ac2b35ad6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -95,6 +95,23 @@ class PropEngine
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
* decision engine and the theory engine of the assertions in ap.
@@ -114,27 +131,10 @@ class PropEngine
* 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
@@ -185,10 +185,11 @@ class PropEngine
/**
* 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.
@@ -261,6 +262,18 @@ class PropEngine
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.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 1b9e78d80..23405675a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,15 +19,14 @@
#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 {
@@ -35,12 +34,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
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)
{
}
@@ -165,5 +167,25 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
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 */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index e16728d0d..4d460434d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,10 +26,13 @@
#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"
@@ -53,7 +56,9 @@ class TheoryProxy
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream);
+ context::UserContext* userContext,
+ CnfStream* cnfStream,
+ ProofNodeManager* pnm);
~TheoryProxy();
@@ -90,6 +95,23 @@ class 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;
@@ -111,6 +133,9 @@ class TheoryProxy
* all imported and exported lemmas.
*/
std::unordered_set<Node, NodeHashFunction> d_shared;
+
+ /** The theory preprocessor */
+ theory::TheoryPreprocessor d_tpp;
}; /* class TheoryProxy */
}/* CVC4::prop namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback