#include "smt/smt_statistics_registry.h"
#include "smt_util/nary_builder.h"
#include "theory/arith/arith_ite_utils.h"
-#include "theory/rewriter.h"
#include "theory/theory_engine.h"
using namespace std;
namespace {
-Node simpITE(util::ITEUtilities* ite_utils, TNode assertion)
-{
- if (!ite_utils->containsTermITE(assertion))
- {
- return assertion;
- }
- else
- {
- Node result = ite_utils->simpITE(assertion);
- Node res_rewritten = Rewriter::rewrite(result);
-
- if (options::simplifyWithCareEnabled())
- {
- Chat() << "starting simplifyWithCare()" << endl;
- Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
- Chat() << "ending simplifyWithCare()"
- << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
- result = Rewriter::rewrite(postSimpWithCare);
- }
- else
- {
- result = res_rewritten;
- }
- return result;
- }
-}
-
/**
* Ensures the assertions asserted after index 'before' now effectively come
* before 'real_assertions_end'.
{
}
+Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion)
+{
+ if (!ite_utils->containsTermITE(assertion))
+ {
+ return assertion;
+ }
+ else
+ {
+ Node result = ite_utils->simpITE(assertion);
+ Node res_rewritten = rewrite(result);
+
+ if (options::simplifyWithCareEnabled())
+ {
+ Chat() << "starting simplifyWithCare()" << endl;
+ Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
+ Chat() << "ending simplifyWithCare()"
+ << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
+ result = rewrite(postSimpWithCare);
+ }
+ else
+ {
+ result = res_rewritten;
+ }
+ return result;
+ }
+}
+
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
bool result = true;
Chat() << "....node manager contains " << nm->poolSize()
<< " nodes before cleanup" << endl;
d_iteUtilities.clear();
- d_preprocContext->getRewriter()->clearCaches();
+ d_env.getRewriter()->clearCaches();
nm->reclaimZombiesUntil(options::zombieHuntThreshold());
Chat() << "....node manager contains " << nm->poolSize()
<< " nodes after cleanup" << endl;
}
// Do theory specific preprocessing passes
- TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine();
- if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
+ if (d_env.getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
&& !options::incrementalSolving())
{
if (!simpDidALotOfWork)
{
Node more = aiteu.reduceConstantIteByGCD(res);
Debug("arith::ite::red") << " gcd->" << more << endl;
- Node morer = Rewriter::rewrite(more);
+ Node morer = rewrite(more);
assertionsToPreprocess->replace(i, morer);
}
}
for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
{
Node curr = (*assertionsToPreprocess)[i];
- Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
+ Node next = rewrite(aiteu.applySubstitutions(curr));
Node res = aiteu.reduceVariablesInItes(next);
Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
<< " ->" << res << endl;
++i)
{
Node curr = (*assertionsToPreprocess)[i];
- Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
+ Node next = rewrite(aiteu.applySubstitutions(curr));
Node res = aiteu.reduceVariablesInItes(next);
Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
<< " ->" << res << endl;
Node more = aiteu.reduceConstantIteByGCD(res);
Debug("arith::ite::red") << " gcd->" << more << endl;
- Node morer = Rewriter::rewrite(more);
+ Node morer = rewrite(more);
assertionsToPreprocess->replace(i, morer);
}
}
/* -------------------------------------------------------------------------- */
ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "ite-simp")
+ : PreprocessingPass(preprocContext, "ite-simp"), d_iteUtilities(d_env)
{
}
Statistics();
};
+ Node simpITE(util::ITEUtilities* ite_utils, TNode assertion);
bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss);
/** A collection of ite preprocessing passes. */
PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
const std::string& name)
- : d_name(name),
+ : EnvObj(preprocContext->getEnv()),
+ d_preprocContext(preprocContext),
+ d_name(name),
d_timer(smtStatisticsRegistry().registerTimer("preprocessing::" + name))
{
- d_preprocContext = preprocContext;
}
PreprocessingPass::~PreprocessingPass() {
#include <string>
+#include "smt/env_obj.h"
#include "util/statistics_stats.h"
namespace cvc5 {
*/
enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
-class PreprocessingPass {
+class PreprocessingPass : public EnvObj
+{
public:
/* Preprocesses a list of assertions assertionsToPreprocess */
PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
/** Get the associated SmtEngine. */
SmtEngine* getSmt() const { return d_smt; }
-
+ /** Get the associated Environment. */
+ Env& getEnv() { return d_env; }
/** Get the associated TheoryEngine. */
TheoryEngine* getTheoryEngine() const;
/** Get the associated Propengine. */
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/passes/rewrite.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/rewriter.h"
#include "theory/theory.h"
#include "util/rational.h"
} // namespace ite
-ITEUtilities::ITEUtilities()
- : d_containsVisitor(new ContainsTermITEVisitor()),
+ITEUtilities::ITEUtilities(Env& env)
+ : EnvObj(env),
+ d_containsVisitor(new ContainsTermITEVisitor()),
d_compressor(NULL),
d_simplifier(NULL),
d_careSimp(NULL)
{
if (d_simplifier == NULL)
{
- d_simplifier = new ITESimplifier(d_containsVisitor.get());
+ d_simplifier = new ITESimplifier(d_env, d_containsVisitor.get());
}
return d_simplifier->simpITE(assertion);
}
{
if (d_compressor == NULL)
{
- d_compressor = new ITECompressor(d_containsVisitor.get());
+ d_compressor = new ITECompressor(d_env, d_containsVisitor.get());
}
return d_compressor->compress(assertionsToPreprocess);
}
void IncomingArcCounter::clear() { d_reachCount.clear(); }
/** ITECompressor. */
-ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
- : d_contains(contains), d_assertions(NULL), d_incoming(true, true)
+ITECompressor::ITECompressor(Env& env, ContainsTermITEVisitor* contains)
+ : EnvObj(env),
+ d_contains(contains),
+ d_assertions(NULL),
+ d_incoming(true, true)
{
Assert(d_contains != NULL);
Node ITECompressor::push_back_boolean(Node original, Node compressed)
{
- Node rewritten = theory::Rewriter::rewrite(compressed);
+ Node rewritten = rewrite(compressed);
// There is a bug if the rewritter takes a pure boolean expression
// and changes its theory
if (rewritten.isConst())
{
Node assertion = assertions[i];
Node compressed = compressBoolean(assertion);
- Node rewritten = theory::Rewriter::rewrite(compressed);
+ Node rewritten = rewrite(compressed);
// replace
assertionsToPreprocess->replace(i, rewritten);
Assert(!d_contains->containsTermITE(rewritten));
return returnValue;
}
-ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
- : d_containsVisitor(contains),
+ITESimplifier::ITESimplifier(Env& env, ContainsTermITEVisitor* contains)
+ : EnvObj(env),
+ d_containsVisitor(contains),
d_termITEHeight(),
d_constantLeaves(),
d_allocatedConstantLeaves(),
}
// Mark the substitution and continue
Node result = builder;
- result = theory::Rewriter::rewrite(result);
+ result = rewrite(result);
d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
return result;
}
if (!containsTermITE(iteNode))
{
- Node n =
- theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+ Node n = rewrite(simpContext.substitute(simpVar, iteNode));
d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
return n;
}
Debug("ite::atom") << " finished " << instance << endl;
if (!attempt.isNull())
{
- Node rewritten = theory::Rewriter::rewrite(attempt);
+ Node rewritten = rewrite(attempt);
Debug("ite::print-success")
<< instance << " "
<< "rewriting " << countReachable(rewritten, kind::ITE) << " from "
<< "how about?" << atom << endl;
Debug("ite::simpite") << instance << " "
<< "\t" << simpContext << endl;
- return theory::Rewriter::rewrite(simpContext);
+ return rewrite(simpContext);
}
Node n = simpConstants(simpContext, iteNode, simpVar);
if (!n.isNull())
// //cout << instance << " " << result << current << endl;
// }
- result = theory::Rewriter::rewrite(result);
+ result = rewrite(result);
d_simpITECache[current] = result;
++(d_statistics.d_simpITEVisits);
toVisit.pop_back();
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "util/hash.h"
#include "util/statistics_stats.h"
namespace cvc5 {
+
namespace preprocessing {
class AssertionPipeline;
NodeBoolMap d_cache;
};
-class ITEUtilities
+class ITEUtilities : public EnvObj
{
public:
- ITEUtilities();
+ ITEUtilities(Env& env);
~ITEUtilities();
Node simpITE(TNode assertion);
* A routine designed to undo the potentially large blow up
* due to expansion caused by the ite simplifier.
*/
-class ITECompressor
+class ITECompressor : public EnvObj
{
public:
- ITECompressor(ContainsTermITEVisitor* contains);
+ ITECompressor(Env& env, ContainsTermITEVisitor* contains);
~ITECompressor();
/* returns false if an assertion is discovered to be equal to false. */
void garbageCollect();
private:
- Node d_true; /* Copy of true. */
- Node d_false; /* Copy of false. */
- ContainsTermITEVisitor* d_contains;
- AssertionPipeline* d_assertions;
- IncomingArcCounter d_incoming;
-
- typedef std::unordered_map<Node, Node> NodeMap;
- NodeMap d_compressed;
+ class Statistics
+ {
+ public:
+ IntStat d_compressCalls;
+ IntStat d_skolemsAdded;
+ Statistics();
+ };
void reset();
Node compressTerm(Node toCompress);
Node compressBoolean(Node toCompress);
- class Statistics
- {
- public:
- IntStat d_compressCalls;
- IntStat d_skolemsAdded;
- Statistics();
- };
+ Node d_true; /* Copy of true. */
+ Node d_false; /* Copy of false. */
+
+ ContainsTermITEVisitor* d_contains;
+ AssertionPipeline* d_assertions;
+ IncomingArcCounter d_incoming;
+
+ typedef std::unordered_map<Node, Node> NodeMap;
+ NodeMap d_compressed;
+
Statistics d_statistics;
}; /* class ITECompressor */
-class ITESimplifier
+class ITESimplifier : public EnvObj
{
public:
- ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
+ ITESimplifier(Env& env, ContainsTermITEVisitor* d_containsVisitor);
~ITESimplifier();
Node simpITE(TNode assertion);
void clearSimpITECaches();
private:
- Node d_true;
- Node d_false;
+ using NodeVec = std::vector<Node>;
+ using ConstantLeavesMap = std::unordered_map<Node, NodeVec*>;
+ using NodePair = std::pair<Node, Node>;
+ using NodePairHashFunction =
+ PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>;
+ using NodePairMap = std::unordered_map<NodePair, Node, NodePairHashFunction>;
+
+ class Statistics
+ {
+ public:
+ IntStat d_maxNonConstantsFolded;
+ IntStat d_unexpected;
+ IntStat d_unsimplified;
+ IntStat d_exactMatchFold;
+ IntStat d_binaryPredFold;
+ IntStat d_specialEqualityFolds;
+ IntStat d_simpITEVisits;
+
+ HistogramStat<uint32_t> d_inSmaller;
+
+ Statistics();
+ };
- ContainsTermITEVisitor* d_containsVisitor;
inline bool containsTermITE(TNode n)
{
return d_containsVisitor->containsTermITE(n);
}
- TermITEHeightCounter d_termITEHeight;
+
inline uint32_t termITEHeight(TNode e)
{
return d_termITEHeight.termITEHeight(e);
}
- // ConstantIte is a small inductive sublanguage:
- // constant
- // or termITE(cnd, ConstantIte, ConstantIte)
- typedef std::vector<Node> NodeVec;
- typedef std::unordered_map<Node, NodeVec*> ConstantLeavesMap;
- ConstantLeavesMap d_constantLeaves;
-
// d_constantLeaves satisfies the following invariants:
// not containsTermITE(x) then !isKey(x)
// containsTermITE(x):
* returns a sorted NodeVec of the leaves. */
NodeVec* computeConstantLeaves(TNode ite);
- // Lists all of the vectors in d_constantLeaves for fast deletion.
- std::vector<NodeVec*> d_allocatedConstantLeaves;
-
/* transforms */
Node transformAtom(TNode atom);
Node attemptConstantRemoval(TNode atom);
// Given ConstantIte tree cite and a constant c,
// return a boolean expression equivalent to (= lcite c)
Node constantIteEqualsConstant(TNode cite, TNode c);
+
+ Node replaceOver(Node n, Node replaceWith, Node simpVar);
+ Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
+
+ bool leavesAreConst(TNode e, theory::TheoryId tid);
+ bool leavesAreConst(TNode e);
+
+ Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
+
+ Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
+
+ Node d_true;
+ Node d_false;
+
+ ContainsTermITEVisitor* d_containsVisitor;
+
+ TermITEHeightCounter d_termITEHeight;
+
+ // ConstantIte is a small inductive sublanguage:
+ // constant
+ // or termITE(cnd, ConstantIte, ConstantIte)
+ ConstantLeavesMap d_constantLeaves;
+
+ // Lists all of the vectors in d_constantLeaves for fast deletion.
+ std::vector<NodeVec*> d_allocatedConstantLeaves;
+
uint32_t d_citeEqConstApplications;
- typedef std::pair<Node, Node> NodePair;
- using NodePairHashFunction =
- PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>;
- typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
NodePairMap d_constantIteEqualsConstantCache;
NodePairMap d_replaceOverCache;
NodePairMap d_replaceOverTermIteCache;
- Node replaceOver(Node n, Node replaceWith, Node simpVar);
- Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
std::unordered_map<Node, bool> d_leavesConstCache;
- bool leavesAreConst(TNode e, theory::TheoryId tid);
- bool leavesAreConst(TNode e);
NodePairMap d_simpConstCache;
- Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
std::unordered_map<TypeNode, Node> d_simpVars;
Node getSimpVar(TypeNode t);
typedef std::unordered_map<Node, Node> NodeMap;
NodeMap d_simpContextCache;
- Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
NodeMap d_simpITECache;
Node simpITEAtom(TNode atom);
- private:
- class Statistics
- {
- public:
- IntStat d_maxNonConstantsFolded;
- IntStat d_unexpected;
- IntStat d_unsimplified;
- IntStat d_exactMatchFold;
- IntStat d_binaryPredFold;
- IntStat d_specialEqualityFolds;
- IntStat d_simpITEVisits;
-
- HistogramStat<uint32_t> d_inSmaller;
-
- Statistics();
- };
-
Statistics d_statistics;
};
#include "expr/node_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "test_smt.h"
{
TestSmt::SetUp();
+ d_preprocContext.reset(new preprocessing::PreprocessingPassContext(
+ d_smtEngine.get(), d_smtEngine->getEnv(), nullptr));
+
d_zero = bv::utils::mkZero(16);
d_p = bv::utils::mkConcat(
}
}
+ std::unique_ptr<PreprocessingPassContext> d_preprocContext;
+
Node d_p;
Node d_x;
Node d_y;
AssertionPipeline apipe;
apipe.push_back(a);
- passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
+ passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
apipe.push_back(a);
apipe.push_back(eq4);
apipe.push_back(eq5);
- passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
+ passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
AssertionPipeline apipe;
apipe.push_back(eq1);
apipe.push_back(eq2);
- passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
+ passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
projects / cvc5.git / commitdiff