summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/theory_preprocess.cpp3
-rw-r--r--src/theory/theory_engine.cpp20
-rw-r--r--src/theory/theory_engine.h7
-rw-r--r--src/theory/theory_preprocessor.cpp64
-rw-r--r--src/theory/theory_preprocessor.h9
5 files changed, 40 insertions, 63 deletions
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index a4d7db72e..bf9c3e9fe 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -32,12 +32,11 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
TheoryEngine* te = d_preprocContext->getTheoryEngine();
- te->preprocessStart();
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
TNode a = (*assertionsToPreprocess)[i];
Assert(Rewriter::rewrite(a) == a);
- assertionsToPreprocess->replace(i, te->preprocess(a));
+ assertionsToPreprocess->replaceTrusted(i, te->preprocess(a));
a = (*assertionsToPreprocess)[i];
Assert(Rewriter::rewrite(a) == a);
}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 924d045da..706149d86 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -251,7 +251,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_tpp(*this, iteRemover, d_pnm),
+ d_tpp(*this, iteRemover, userContext, d_pnm),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
d_true(),
d_false(),
@@ -824,8 +824,6 @@ void TheoryEngine::shutdown() {
theoryOf(theoryId)->shutdown();
}
}
-
- d_tpp.clearCache();
}
theory::Theory::PPAssertStatus TheoryEngine::solve(
@@ -855,18 +853,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
return solveStatus;
}
-void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
-
-Node TheoryEngine::preprocess(TNode assertion)
+TrustNode TheoryEngine::preprocess(TNode assertion)
{
- TrustNode trn = d_tpp.theoryPreprocess(assertion);
- if (trn.isNull())
- {
- // no change
- return assertion;
- }
- // notice that we could alternatively return the trust node here.
- return trn.getNode();
+ return d_tpp.theoryPreprocess(assertion);
}
void TheoryEngine::notifyPreprocessedAssertions(
@@ -1147,7 +1136,8 @@ Node TheoryEngine::ensureLiteral(TNode n) {
Debug("ensureLiteral") << "rewriting: " << n << std::endl;
Node rewritten = Rewriter::rewrite(n);
Debug("ensureLiteral") << " got: " << rewritten << std::endl;
- Node preprocessed = preprocess(rewritten);
+ TrustNode tp = preprocess(rewritten);
+ Node preprocessed = tp.isNull() ? rewritten : tp.getNode();
Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
d_propEngine->ensureLiteral(preprocessed);
return preprocessed;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3626b623a..e47dbbc6f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -446,16 +446,11 @@ class TheoryEngine {
public:
/**
- * Signal the start of a new round of assertion preprocessing
- */
- void preprocessStart();
-
- /**
* Runs theory specific preprocessing on the non-Boolean parts of
* the formula. This is only called on input assertions, after ITEs
* have been removed.
*/
- Node preprocess(TNode node);
+ theory::TrustNode preprocess(TNode node);
/** Notify (preprocessed) assertions. */
void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index b37a45967..42ac074ce 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -27,15 +27,15 @@ namespace theory {
TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
RemoveTermFormulas& tfr,
+ context::UserContext* userContext,
ProofNodeManager* pnm)
: d_engine(engine),
d_logicInfo(engine.getLogicInfo()),
- d_ppCache(),
+ d_ppCache(userContext),
d_tfr(tfr),
- d_pfContext(),
d_tpg(pnm ? new TConvProofGenerator(
pnm,
- &d_pfContext,
+ userContext,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"TheoryPreprocessor::preprocess_rewrite",
@@ -43,7 +43,7 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
: nullptr),
d_tspg(nullptr),
d_tpgRew(pnm ? new TConvProofGenerator(pnm,
- &d_pfContext,
+ userContext,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"TheoryPreprocessor::rewrite")
@@ -51,15 +51,12 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
d_tspgNoPp(nullptr),
d_lp(pnm ? new LazyCDProof(pnm,
nullptr,
- &d_pfContext,
+ userContext,
"TheoryPreprocessor::LazyCDProof")
: nullptr)
{
if (isProofEnabled())
{
- // push the proof context, since proof steps may be cleared on calls to
- // clearCache() below.
- d_pfContext.push();
// Make the main term conversion sequence generator, which tracks up to
// three conversions made in succession:
// (1) theory preprocessing+rewriting
@@ -71,7 +68,7 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
ts.push_back(d_tfr.getTConvProofGenerator());
ts.push_back(d_tpg.get());
d_tspg.reset(new TConvSeqProofGenerator(
- pnm, ts, &d_pfContext, "TheoryPreprocessor::sequence"));
+ pnm, ts, userContext, "TheoryPreprocessor::sequence"));
// Make the "no preprocess" term conversion sequence generator, which
// applies only steps (2) and (3), where notice (3) must use the
// "pure rewrite" term conversion (d_tpgRew).
@@ -79,24 +76,12 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
tsNoPp.push_back(d_tfr.getTConvProofGenerator());
tsNoPp.push_back(d_tpgRew.get());
d_tspgNoPp.reset(new TConvSeqProofGenerator(
- pnm, tsNoPp, &d_pfContext, "TheoryPreprocessor::sequence_no_pp"));
+ pnm, tsNoPp, userContext, "TheoryPreprocessor::sequence_no_pp"));
}
}
TheoryPreprocessor::~TheoryPreprocessor() {}
-void TheoryPreprocessor::clearCache()
-{
- Trace("tpp-proof-debug") << "TheoryPreprocessor::clearCache" << std::endl;
- d_ppCache.clear();
- // clear proofs from d_tpg, d_tspg and d_lp using internal push/pop context
- if (isProofEnabled())
- {
- d_pfContext.pop();
- d_pfContext.push();
- }
-}
-
TrustNode TheoryPreprocessor::preprocess(TNode node,
std::vector<TrustNode>& newLemmas,
std::vector<Node>& newSkolems,
@@ -115,18 +100,10 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
TrustNode tpp = theoryPreprocess(node);
ppNode = tpp.getNode();
}
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor::preprocess: after preprocessing " << ppNode
- << std::endl;
// Remove the ITEs
- Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl;
TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
- Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl;
Node rtfNode = ttfr.getNode();
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor::preprocess: rtf returned node " << rtfNode
- << std::endl;
if (Debug.isOn("lemma-ites"))
{
@@ -143,9 +120,25 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
// Rewrite the main node, we rewrite and store the proof step, if necessary,
// in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
Node retNode = rewriteWithProof(rtfNode);
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
- << std::endl;
+
+ if (Trace.isOn("tpp-proof-debug"))
+ {
+ if (node != ppNode)
+ {
+ Trace("tpp-proof-debug")
+ << "after preprocessing : " << ppNode << std::endl;
+ }
+ if (rtfNode != ppNode)
+ {
+ Trace("tpp-proof-debug") << "after rtf : " << rtfNode << std::endl;
+ }
+ if (retNode != rtfNode)
+ {
+ Trace("tpp-proof-debug") << "after rewriting : " << retNode << std::endl;
+ }
+ Trace("tpp-proof-debug")
+ << "TheoryPreprocessor::preprocess: finish" << std::endl;
+ }
if (node == retNode)
{
// no change
@@ -284,7 +277,8 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
{
Node ppRewritten = ppTheoryRewrite(current);
d_ppCache[current] = ppRewritten;
- Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
+ Assert(Rewriter::rewrite(d_ppCache[current].get())
+ == d_ppCache[current].get());
continue;
}
@@ -300,7 +294,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
for (unsigned i = 0; i < current.getNumChildren(); ++i)
{
Assert(d_ppCache.find(current[i]) != d_ppCache.end());
- builder << d_ppCache[current[i]];
+ builder << d_ppCache[current[i]].get();
}
// Mark the substitution and continue
Node result = builder;
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 769d548d9..e34b10b1d 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -19,6 +19,8 @@
#include <unordered_map>
+#include "context/cdhashmap.h"
+#include "context/context.h"
#include "expr/lazy_proof.h"
#include "expr/node.h"
#include "expr/tconv_seq_proof_generator.h"
@@ -38,17 +40,16 @@ namespace theory {
*/
class TheoryPreprocessor
{
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
public:
/** Constructs a theory preprocessor */
TheoryPreprocessor(TheoryEngine& engine,
RemoveTermFormulas& tfr,
+ context::UserContext* userContext,
ProofNodeManager* pnm = nullptr);
/** Destroys a theory preprocessor */
~TheoryPreprocessor();
- /** Clear the cache of this class */
- void clearCache();
/**
* Preprocesses the given assertion node. It returns a TrustNode of kind
* TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
@@ -84,8 +85,6 @@ class TheoryPreprocessor
NodeMap d_ppCache;
/** The term formula remover */
RemoveTermFormulas& d_tfr;
- /** The context for the proof generator below */
- context::Context d_pfContext;
/** The term context, which computes hash values for term contexts. */
InQuantTermContext d_iqtc;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback