summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/preprocessing/passes/ite_removal.cpp27
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp2
-rw-r--r--src/preprocessing/preprocessing_pass_context.h5
-rw-r--r--src/smt/check_models.cpp5
-rw-r--r--src/smt/preprocessor.cpp13
-rw-r--r--src/smt/preprocessor.h14
-rw-r--r--src/smt/smt_solver.cpp1
-rw-r--r--src/smt/term_formula_removal.cpp61
-rw-r--r--src/smt/term_formula_removal.h12
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--src/theory/theory_engine.h8
-rw-r--r--src/theory/theory_preprocessor.cpp5
-rw-r--r--src/theory/theory_preprocessor.h4
13 files changed, 54 insertions, 106 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index a75b6f5ad..3531497e8 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -18,6 +18,7 @@
#include "preprocessing/passes/ite_removal.h"
#include "theory/rewriter.h"
+#include "theory/theory_preprocessor.h"
namespace CVC4 {
namespace preprocessing {
@@ -25,6 +26,7 @@ namespace passes {
using namespace CVC4::theory;
+// TODO (project #42): note this preprocessing pass is deprecated
IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "ite-removal")
{
@@ -36,19 +38,36 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
IteSkolemMap& imap = assertions->getIteSkolemMap();
// Remove all of the ITE occurrences and normalize
+ theory::TheoryPreprocessor* tpp =
+ d_preprocContext->getTheoryEngine()->getTheoryPreprocess();
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
+ Node assertion = (*assertions)[i];
std::vector<theory::TrustNode> newAsserts;
std::vector<Node> newSkolems;
- TrustNode trn = d_preprocContext->getIteRemover()->run(
- (*assertions)[i], newAsserts, newSkolems, true);
- // process
- assertions->replaceTrusted(i, trn);
+ // TODO (project #42): this will call the prop engine
+ TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false);
+ 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);
+ }
}
}
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index ff4a0e6ca..707d1314c 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -23,12 +23,10 @@ namespace preprocessing {
PreprocessingPassContext::PreprocessingPassContext(
SmtEngine* smt,
- RemoveTermFormulas* iteRemover,
theory::booleans::CircuitPropagator* circuitPropagator,
ProofNodeManager* pnm)
: d_smt(smt),
d_resourceManager(smt->getResourceManager()),
- d_iteRemover(iteRemover),
d_topLevelSubstitutions(smt->getUserContext(), pnm),
d_circuitPropagator(circuitPropagator),
d_pnm(pnm),
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 824197bc5..c22a69255 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -40,7 +40,6 @@ class PreprocessingPassContext
public:
PreprocessingPassContext(
SmtEngine* smt,
- RemoveTermFormulas* iteRemover,
theory::booleans::CircuitPropagator* circuitPropagator,
ProofNodeManager* pnm);
@@ -49,7 +48,6 @@ class PreprocessingPassContext
prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
context::Context* getUserContext() { return d_smt->getUserContext(); }
context::Context* getDecisionContext() { return d_smt->getContext(); }
- RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
theory::booleans::CircuitPropagator* getCircuitPropagator()
{
@@ -95,9 +93,6 @@ class PreprocessingPassContext
/** Pointer to the ResourceManager for this context. */
ResourceManager* d_resourceManager;
- /** Instance of the ITE remover */
- RemoveTermFormulas* d_iteRemover;
-
/* The top level substitutions */
theory::TrustSubstitutionMap d_topLevelSubstitutions;
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index a41c750ec..2338ebd61 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -184,9 +184,8 @@ void CheckModels::checkModel(Model* m,
n = m->getValue(n);
Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
- // Simplify the result and replace the already-known ITEs (this is important
- // for ground ITEs under quantifiers).
- n = pp->simplify(n, true);
+ // Simplify the result
+ n = pp->simplify(n);
Notice()
<< "SmtEngine::checkModel(): -- simplifies with ite replacement to "
<< n << std::endl;
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index c2b8f73f1..ec7751a54 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -38,7 +38,6 @@ Preprocessor::Preprocessor(SmtEngine& smt,
d_assertionsProcessed(u, false),
d_exDefs(smt, *smt.getResourceManager(), stats),
d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
- d_rtf(u),
d_pnm(nullptr)
{
}
@@ -55,7 +54,7 @@ Preprocessor::~Preprocessor()
void Preprocessor::finishInit()
{
d_ppContext.reset(new preprocessing::PreprocessingPassContext(
- &d_smt, &d_rtf, &d_propagator, d_pnm));
+ &d_smt, &d_propagator, d_pnm));
// initialize the preprocessing passes
d_processor.finishInit(d_ppContext.get());
@@ -104,8 +103,6 @@ void Preprocessor::clearLearnedLiterals()
void Preprocessor::cleanup() { d_processor.cleanup(); }
-RemoveTermFormulas& Preprocessor::getTermFormulaRemover() { return d_rtf; }
-
Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
{
std::unordered_map<Node, Node, NodeHashFunction> cache;
@@ -129,7 +126,7 @@ Node Preprocessor::expandDefinitions(
return d_exDefs.expandDefinitions(n, cache, expandOnly);
}
-Node Preprocessor::simplify(const Node& node, bool removeItes)
+Node Preprocessor::simplify(const Node& node)
{
Trace("smt") << "SMT simplify(" << node << ")" << endl;
if (Dump.isOn("benchmark"))
@@ -147,11 +144,6 @@ Node Preprocessor::simplify(const Node& node, bool removeItes)
Node n = d_exDefs.expandDefinitions(nas, cache);
TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
Node ns = ts.isNull() ? n : ts.getNode();
- if (removeItes)
- {
- // also remove ites if asked
- ns = d_rtf.replace(ns);
- }
return ns;
}
@@ -161,7 +153,6 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
d_pnm = pppg->getManager();
d_exDefs.setProofNodeManager(d_pnm);
d_propagator.setProof(d_pnm, d_context, pppg);
- d_rtf.setProofNodeManager(d_pnm);
}
} // namespace smt
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 220a433fe..367490306 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -22,7 +22,6 @@
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/expand_definitions.h"
#include "smt/process_assertions.h"
-#include "smt/term_formula_removal.h"
#include "theory/booleans/circuit_propagator.h"
namespace CVC4 {
@@ -79,11 +78,9 @@ class Preprocessor
* has been constructed. It also involves theory normalization.
*
* @param n The node to simplify
- * @param removeItes Whether to remove ITE (and other terms with formulas in
- * term positions) from the result.
* @return The simplified term.
*/
- Node simplify(const Node& n, bool removeItes = false);
+ Node simplify(const Node& n);
/**
* Expand the definitions in a term or formula n. No other
* simplification or normalization is done.
@@ -99,10 +96,6 @@ class Preprocessor
const Node& n,
std::unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly = false);
- /**
- * Get the underlying term formula remover utility.
- */
- RemoveTermFormulas& getTermFormulaRemover();
/**
* Set proof node manager. Enables proofs in this preprocessor.
@@ -133,11 +126,6 @@ class Preprocessor
* passes.
*/
ProcessAssertions d_processor;
- /**
- * The term formula remover, responsible for eliminating formulas that occur
- * in term contexts.
- */
- RemoveTermFormulas d_rtf;
/** Proof node manager */
ProofNodeManager* d_pnm;
};
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index e53401f79..3e8d0f147 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -50,7 +50,6 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
d_smt.getUserContext(),
d_rm,
- d_pp.getTermFormulaRemover(),
logicInfo,
d_smt.getOutputManager(),
d_pnm));
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index f3e0d0bd6..60b850a31 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -26,13 +26,23 @@ using namespace std;
namespace CVC4 {
-RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
- : d_tfCache(u),
- d_skolem_cache(u),
- d_pnm(nullptr),
- d_tpg(nullptr),
- d_lp(nullptr)
+RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
+ ProofNodeManager* pnm)
+ : d_tfCache(u), d_skolem_cache(u), d_pnm(pnm), d_tpg(nullptr), d_lp(nullptr)
{
+ // enable proofs if necessary
+ if (d_pnm != nullptr)
+ {
+ d_tpg.reset(
+ new TConvProofGenerator(d_pnm,
+ nullptr,
+ TConvPolicy::FIXPOINT,
+ TConvCachePolicy::NEVER,
+ "RemoveTermFormulas::TConvProofGenerator",
+ &d_rtfc));
+ d_lp.reset(new LazyCDProof(
+ d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
+ }
}
RemoveTermFormulas::~RemoveTermFormulas() {}
@@ -40,29 +50,9 @@ RemoveTermFormulas::~RemoveTermFormulas() {}
theory::TrustNode RemoveTermFormulas::run(
Node assertion,
std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool reportDeps)
+ std::vector<Node>& newSkolems)
{
Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
- // In some calling contexts, not necessary to report dependence information.
- if (reportDeps && options::unsatCores())
- {
- // new assertions have a dependence on the node
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(itesRemoved, assertion);
- }
- unsigned n = 0;
- while (n < newAsserts.size())
- {
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(newAsserts[n].getProven(),
- assertion);
- }
- ++n;
- }
- }
// The rewriting of assertion can be justified by the term conversion proof
// generator d_tpg.
return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
@@ -536,23 +526,6 @@ Node RemoveTermFormulas::getAxiomFor(Node n)
return Node::null();
}
-void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
-{
- if (d_tpg == nullptr)
- {
- d_pnm = pnm;
- d_tpg.reset(
- new TConvProofGenerator(d_pnm,
- nullptr,
- TConvPolicy::FIXPOINT,
- TConvCachePolicy::NEVER,
- "RemoveTermFormulas::TConvProofGenerator",
- &d_rtfc));
- d_lp.reset(new LazyCDProof(
- d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
- }
-}
-
ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
{
return d_tpg.get();
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 25dcd0295..fc10e19c9 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -38,7 +38,7 @@ typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveTermFormulas {
public:
- RemoveTermFormulas(context::UserContext* u);
+ RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
~RemoveTermFormulas();
/**
@@ -83,15 +83,13 @@ class RemoveTermFormulas {
* @param newAsserts The new assertions corresponding to axioms for newly
* introduced skolems.
* @param newSkolems The skolems corresponding to each of the newAsserts.
- * @param reportDeps Used for unsat cores in the old proof infrastructure.
* @return a trust node of kind TrustNodeKind::REWRITE whose
* right hand side is assertion after removing term formulas, and the proof
* generator (if provided) that can prove the equivalence.
*/
theory::TrustNode run(Node assertion,
std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool reportDeps = false);
+ std::vector<Node>& newSkolems);
/**
* Substitute under node using pre-existing cache. Do not remove
@@ -106,12 +104,6 @@ class RemoveTermFormulas {
void garbageCollect();
/**
- * Set proof node manager, which signals this class to enable proofs using the
- * given proof node manager.
- */
- void setProofNodeManager(ProofNodeManager* pnm);
-
- /**
* Get proof generator that is responsible for all proofs for removing term
* formulas from nodes. When proofs are enabled, the returned trust node
* of the run method use this proof generator (the trust nodes in newAsserts
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7b38bd844..ecb15fbe9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -218,7 +218,6 @@ ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
ResourceManager* rm,
- RemoveTermFormulas& iteRemover,
const LogicInfo& logicInfo,
OutputManager& outMgr,
ProofNodeManager* pnm)
@@ -250,7 +249,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_tpp(*this, iteRemover, userContext, d_pnm),
+ d_tpp(*this, userContext, d_pnm),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
d_true(),
d_false(),
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1412d7464..bdc79931f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -95,13 +95,8 @@ class RelevanceManager;
namespace eq {
class EqualityEngine;
} // namespace eq
-
-class EntailmentCheckParameters;
-class EntailmentCheckSideEffects;
}/* CVC4::theory namespace */
-class RemoveTermFormulas;
-
/**
* This is essentially an abstraction for a collection of theories. A
* TheoryEngine provides services to a PropEngine, making various
@@ -313,7 +308,6 @@ class TheoryEngine {
TheoryEngine(context::Context* context,
context::UserContext* userContext,
ResourceManager* rm,
- RemoveTermFormulas& iteRemover,
const LogicInfo& logic,
OutputManager& outMgr,
ProofNodeManager* pnm);
@@ -454,6 +448,8 @@ class TheoryEngine {
* 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);
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index ad9250a78..179ecc130 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -26,13 +26,12 @@ namespace CVC4 {
namespace theory {
TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
- RemoveTermFormulas& tfr,
context::UserContext* userContext,
ProofNodeManager* pnm)
: d_engine(engine),
d_logicInfo(engine.getLogicInfo()),
d_ppCache(userContext),
- d_tfr(tfr),
+ d_tfr(userContext, pnm),
d_tpg(pnm ? new TConvProofGenerator(
pnm,
userContext,
@@ -102,7 +101,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
}
// Remove the ITEs
- TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
+ TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems);
Node rtfNode = ttfr.getNode();
if (Debug.isOn("lemma-ites"))
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 147c17f4a..349e7917e 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -25,6 +25,7 @@
#include "expr/node.h"
#include "expr/tconv_seq_proof_generator.h"
#include "expr/term_conversion_proof_generator.h"
+#include "smt/term_formula_removal.h"
#include "theory/trust_node.h"
namespace CVC4 {
@@ -45,7 +46,6 @@ class TheoryPreprocessor
public:
/** Constructs a theory preprocessor */
TheoryPreprocessor(TheoryEngine& engine,
- RemoveTermFormulas& tfr,
context::UserContext* userContext,
ProofNodeManager* pnm = nullptr);
/** Destroys a theory preprocessor */
@@ -100,7 +100,7 @@ class TheoryPreprocessor
/** Cache for theory-preprocessing of assertions */
NodeMap d_ppCache;
/** The term formula remover */
- RemoveTermFormulas& d_tfr;
+ RemoveTermFormulas d_tfr;
/** 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