summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am2
-rw-r--r--src/preprocessing/passes/ite_removal.cpp49
-rw-r--r--src/preprocessing/passes/ite_removal.h46
-rw-r--r--src/preprocessing/preprocessing_pass.h10
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp6
-rw-r--r--src/preprocessing/preprocessing_pass_context.h10
-rw-r--r--src/smt/smt_engine.cpp85
7 files changed, 148 insertions, 60 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 992f229d6..59a2a64c0 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \
preprocessing/passes/extended_rewriter_pass.h \
preprocessing/passes/int_to_bv.cpp \
preprocessing/passes/int_to_bv.h \
+ preprocessing/passes/ite_removal.cpp \
+ preprocessing/passes/ite_removal.h \
preprocessing/passes/pseudo_boolean_processor.cpp \
preprocessing/passes/pseudo_boolean_processor.h \
preprocessing/passes/bool_to_bv.cpp \
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
new file mode 100644
index 000000000..86c40a793
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -0,0 +1,49 @@
+/********************* */
+/*! \file ite_removal.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "preprocessing/passes/ite_removal.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "ite-removal")
+{
+}
+
+PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
+{
+ d_preprocContext->spendResource(options::preprocessStep());
+
+ // Remove all of the ITE occurrences and normalize
+ d_preprocContext->getIteRemover()->run(
+ assertions->ref(), assertions->getIteSkolemMap(), true);
+ for (unsigned i = 0, size = assertions->size(); i < size; ++i)
+ {
+ assertions->replace(i, Rewriter::rewrite((*assertions)[i]));
+ }
+
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
new file mode 100644
index 000000000..27ec4f095
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.h
@@ -0,0 +1,46 @@
+/********************* */
+/*! \file ite_removal.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class IteRemoval : public PreprocessingPass
+{
+ public:
+ IteRemoval(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(AssertionPipeline* assertions) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 441d1c7cd..6f76b60e9 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -38,6 +38,7 @@
#include "expr/node.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
#include "theory/substitutions.h"
namespace CVC4 {
@@ -86,6 +87,8 @@ class AssertionPipeline
*/
void replace(size_t i, const std::vector<Node>& ns);
+ IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+
context::CDO<unsigned>& getSubstitutionsIndex()
{
return d_substitutionsIndex;
@@ -99,12 +102,17 @@ class AssertionPipeline
private:
std::vector<Node> d_nodes;
+ /**
+ * Map from skolem variables to index in d_assertions containing
+ * corresponding introduced Boolean ite
+ */
+ IteSkolemMap d_iteSkolemMap;
+
/* Index for where to store substitutions */
context::CDO<unsigned> d_substitutionsIndex;
/* The top level substitutions */
theory::SubstitutionMap d_topLevelSubstitutions;
-
}; /* class AssertionPipeline */
/**
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 1f3d245d7..31987b00b 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -20,8 +20,10 @@ namespace CVC4 {
namespace preprocessing {
PreprocessingPassContext::PreprocessingPassContext(
- SmtEngine* smt, ResourceManager* resourceManager)
- : d_smt(smt), d_resourceManager(resourceManager)
+ SmtEngine* smt,
+ ResourceManager* resourceManager,
+ RemoveTermFormulas* iteRemover)
+ : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover)
{
}
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 9927cd8fb..b50421e6c 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -24,6 +24,7 @@
#include "context/context.h"
#include "decision/decision_engine.h"
#include "smt/smt_engine.h"
+#include "smt/term_formula_removal.h"
#include "theory/theory_engine.h"
#include "util/resource_manager.h"
@@ -33,12 +34,16 @@ namespace preprocessing {
class PreprocessingPassContext
{
public:
- PreprocessingPassContext(SmtEngine* smt, ResourceManager* resourceManager);
+ PreprocessingPassContext(SmtEngine* smt,
+ ResourceManager* resourceManager,
+ RemoveTermFormulas* iteRemover);
SmtEngine* getSmt() { return d_smt; }
TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
context::Context* getUserContext() { return d_smt->d_userContext; }
+ RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
+
void spendResource(unsigned amount)
{
d_resourceManager->spendResource(amount);
@@ -51,6 +56,9 @@ class PreprocessingPassContext
/* Pointer to the SmtEngine that this context was created in. */
SmtEngine* d_smt;
ResourceManager* d_resourceManager;
+
+ /** Instance of the ITE remover */
+ RemoveTermFormulas* d_iteRemover;
}; // class PreprocessingPassContext
} // namespace preprocessing
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b5d758bca..d2e9c2f36 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,6 +79,7 @@
#include "preprocessing/passes/bv_to_bool.h"
#include "preprocessing/passes/extended_rewriter_pass.h"
#include "preprocessing/passes/int_to_bv.h"
+#include "preprocessing/passes/ite_removal.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/real_to_int.h"
#include "preprocessing/passes/rewrite.h"
@@ -204,8 +205,6 @@ struct SmtEngineStatistics {
TimerStat d_simpITETime;
/** time spent in simplifying ITEs */
TimerStat d_unconstrainedSimpTime;
- /** time spent removing ITEs */
- TimerStat d_iteRemovalTime;
/** time spent in theory preprocessing */
TimerStat d_theoryPreprocessTime;
/** time spent in theory preprocessing */
@@ -243,7 +242,6 @@ struct SmtEngineStatistics {
d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
d_simpITETime("smt::SmtEngine::simpITETime"),
d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
- d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
@@ -267,7 +265,6 @@ struct SmtEngineStatistics {
smtStatisticsRegistry()->registerStat(&d_numConstantProps);
smtStatisticsRegistry()->registerStat(&d_simpITETime);
smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
- smtStatisticsRegistry()->registerStat(&d_iteRemovalTime);
smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime);
smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
@@ -292,7 +289,6 @@ struct SmtEngineStatistics {
smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
- smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime);
smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime);
smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
@@ -563,12 +559,8 @@ class SmtEnginePrivate : public NodeManagerListener {
/** mapping from expressions to name */
context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
//------------------------------- end expression names
-public:
- /**
- * Map from skolem variables to index in d_assertions containing
- * corresponding introduced Boolean ite
- */
- IteSkolemMap d_iteSkolemMap;
+ public:
+ IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
/** Instance of the ITE remover */
RemoveTermFormulas d_iteRemover;
@@ -595,11 +587,6 @@ public:
*/
void staticLearning();
- /**
- * Remove ITEs from the assertions.
- */
- void removeITEs();
-
Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
@@ -638,8 +625,8 @@ public:
* Remove conjuncts in toRemove from conjunction n. Return # of removed
* conjuncts.
*/
- size_t removeFromConjunction(Node& n,
- const std::unordered_set<unsigned long>& toRemove);
+ size_t removeFromConjunction(
+ Node& n, const std::unordered_set<unsigned long>& toRemove);
/** Scrub miplib encodings. */
void doMiplibTrick();
@@ -673,7 +660,6 @@ public:
d_simplifyAssertionsDepth(0),
// d_needsExpandDefs(true), //TODO?
d_exprNames(smt.d_userContext),
- d_iteSkolemMap(),
d_iteRemover(smt.d_userContext)
{
d_smt.d_nodeManager->subscribeEvents(this);
@@ -839,7 +825,7 @@ public:
d_assertions.clear();
d_nonClausalLearnedLiterals.clear();
d_realAssertionsEnd = 0;
- d_iteSkolemMap.clear();
+ getIteSkolemMap().clear();
}
/**
@@ -988,7 +974,8 @@ SmtEngine::SmtEngine(ExprManager* em)
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context, d_userContext,
+ d_theoryEngine = new TheoryEngine(d_context,
+ d_userContext,
d_private->d_iteRemover,
const_cast<const LogicInfo&>(d_logic),
d_channels);
@@ -2654,7 +2641,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){
void SmtEnginePrivate::finishInit()
{
d_preprocessingPassContext.reset(
- new PreprocessingPassContext(&d_smt, d_resourceManager));
+ new PreprocessingPassContext(&d_smt, d_resourceManager, &d_iteRemover));
// TODO: register passes here (this will likely change when we add support for
// actually assembling preprocessing pipelines).
std::unique_ptr<ApplySubsts> applySubsts(
@@ -2679,6 +2666,8 @@ void SmtEnginePrivate::finishInit()
new IntToBV(d_preprocessingPassContext.get()));
std::unique_ptr<PseudoBooleanProcessor> pbProc(
new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
+ std::unique_ptr<IteRemoval> iteRemoval(
+ new IteRemoval(d_preprocessingPassContext.get()));
std::unique_ptr<RealToInt> realToInt(
new RealToInt(d_preprocessingPassContext.get()));
std::unique_ptr<Rewrite> rewrite(
@@ -2711,6 +2700,8 @@ void SmtEnginePrivate::finishInit()
d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
std::move(pbProc));
+ d_preprocessingPassRegistry.registerPass("ite-removal",
+ std::move(iteRemoval));
d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
@@ -2968,20 +2959,6 @@ Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, s
return ret;
}
-void SmtEnginePrivate::removeITEs() {
- d_smt.finalOptionsAreSet();
- spendResource(options::preprocessStep());
- Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
-
- // Remove all of the ITE occurrences and normalize
- d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
- }
-}
-
-
-
// do dumping (before/after any preprocessing pass)
static void dumpAssertions(const char* key,
const AssertionPipeline& assertionList) {
@@ -3937,7 +3914,8 @@ Result SmtEngine::check() {
(not d_logic.isQuantified() &&
d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
)){
- if(d_private->d_iteSkolemMap.empty()){
+ if (d_private->getIteSkolemMap().empty())
+ {
options::decisionStopOnly.set(false);
d_decisionEngine->clearStrategies();
Trace("smt") << "SmtEngine::check(): turning off stop only" << endl;
@@ -3976,8 +3954,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_
size_t sz = n.getNumChildren();
if (sz == 0) {
- IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
- if (it != d_iteSkolemMap.end()) {
+ IteSkolemMap::iterator it = getIteSkolemMap().find(n);
+ if (it != getIteSkolemMap().end())
+ {
skolemSet.insert(n);
}
cache[n] = true;
@@ -4002,9 +3981,10 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<N
size_t sz = n.getNumChildren();
if (sz == 0) {
- IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
+ IteSkolemMap::iterator it = getIteSkolemMap().find(n);
bool bad = false;
- if (it != d_iteSkolemMap.end()) {
+ if (it != getIteSkolemMap().end())
+ {
if (!((*it).first < n)) {
bad = true;
}
@@ -4326,22 +4306,15 @@ void SmtEnginePrivate::processAssertions() {
}
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl;
- dumpAssertions("pre-ite-removal", d_assertions);
{
- Chat() << "removing term ITEs..." << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
- // Remove ITEs, updating d_iteSkolemMap
d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
- removeITEs();
+ d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_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_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
}
- Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl;
- dumpAssertions("post-ite-removal", d_assertions);
dumpAssertions("pre-repeat-simplify", d_assertions);
if(options::repeatSimp()) {
@@ -4372,8 +4345,8 @@ void SmtEnginePrivate::processAssertions() {
// 1. iteExpr has the form (ite cond (sk = t) (sk = e))
// 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
// If either of these is violated, we must add iteExpr as a proper assertion
- IteSkolemMap::iterator it = d_iteSkolemMap.begin();
- IteSkolemMap::iterator iend = d_iteSkolemMap.end();
+ IteSkolemMap::iterator it = getIteSkolemMap().begin();
+ IteSkolemMap::iterator iend = getIteSkolemMap().end();
NodeBuilder<> builder(kind::AND);
builder << d_assertions[d_realAssertionsEnd - 1];
vector<TNode> toErase;
@@ -4401,14 +4374,14 @@ void SmtEnginePrivate::processAssertions() {
}
if(builder.getNumChildren() > 1) {
while (!toErase.empty()) {
- d_iteSkolemMap.erase(toErase.back());
+ getIteSkolemMap().erase(toErase.back());
toErase.pop_back();
}
d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
}
// TODO(b/1256): For some reason this is needed for some benchmarks, such as
// QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
- removeITEs();
+ d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions);
d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
// Assert(iteRewriteAssertionsEnd == d_assertions.size());
}
@@ -4468,8 +4441,8 @@ void SmtEnginePrivate::processAssertions() {
if(noConflict) {
Chat() << "pushing to decision engine..." << endl;
Assert(iteRewriteAssertionsEnd == d_assertions.size());
- d_smt.d_decisionEngine->addAssertions
- (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap);
+ d_smt.d_decisionEngine->addAssertions(
+ d_assertions.ref(), d_realAssertionsEnd, getIteSkolemMap());
}
// end: INVARIANT to maintain: no reordering of assertions or
@@ -4491,7 +4464,7 @@ void SmtEnginePrivate::processAssertions() {
d_assertionsProcessed = true;
d_assertions.clear();
- d_iteSkolemMap.clear();
+ getIteSkolemMap().clear();
}
void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback