This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.
This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.
The next step will move the TheoryPreprocessor inside prop::TheoryProxy.
There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.
#include "preprocessing/passes/ite_removal.h"
#include "theory/rewriter.h"
+#include "theory/theory_preprocessor.h"
namespace CVC4 {
namespace preprocessing {
using namespace CVC4::theory;
+// TODO (project #42): note this preprocessing pass is deprecated
IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "ite-removal")
{
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)
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),
public:
PreprocessingPassContext(
SmtEngine* smt,
- RemoveTermFormulas* iteRemover,
theory::booleans::CircuitPropagator* circuitPropagator,
ProofNodeManager* pnm);
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()
{
/** 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;
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;
d_assertionsProcessed(u, false),
d_exDefs(smt, *smt.getResourceManager(), stats),
d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
- d_rtf(u),
d_pnm(nullptr)
{
}
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());
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;
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"))
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;
}
d_pnm = pppg->getManager();
d_exDefs.setProofNodeManager(d_pnm);
d_propagator.setProof(d_pnm, d_context, pppg);
- d_rtf.setProofNodeManager(d_pnm);
}
} // namespace smt
#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 {
* 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.
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.
* 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;
};
d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
d_smt.getUserContext(),
d_rm,
- d_pp.getTermFormulaRemover(),
logicInfo,
d_smt.getOutputManager(),
d_pnm));
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() {}
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());
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();
class RemoveTermFormulas {
public:
- RemoveTermFormulas(context::UserContext* u);
+ RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
~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
/** Garbage collects non-context dependent data-structures. */
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
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
ResourceManager* rm,
- RemoveTermFormulas& iteRemover,
const LogicInfo& logicInfo,
OutputManager& outMgr,
ProofNodeManager* pnm)
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(),
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
TheoryEngine(context::Context* context,
context::UserContext* userContext,
ResourceManager* rm,
- RemoveTermFormulas& iteRemover,
const LogicInfo& logic,
OutputManager& outMgr,
ProofNodeManager* pnm);
* 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);
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,
}
// 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"))
#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 {
public:
/** Constructs a theory preprocessor */
TheoryPreprocessor(TheoryEngine& engine,
- RemoveTermFormulas& tfr,
context::UserContext* userContext,
ProofNodeManager* pnm = nullptr);
/** Destroys a theory preprocessor */
/** 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;
/**
projects / cvc5.git / commitdiff