diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-25 21:09:22 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-25 23:09:22 -0500 |
commit | b70ccff4de0a23bdf11c70002d10a2cc0795a91c (patch) | |
tree | 9898234cdf62e2e58941ba1dd9bed2dca5de8e50 /src/theory/theory_engine.cpp | |
parent | c66033a67511b10b5ee22b7072b9ceab45552a79 (diff) |
Refactor unconstrained simplification pass (#2374)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c87a4be02..d75f7843d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,7 +49,6 @@ #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -#include "theory/unconstrained_simplifier.h" #include "util/resource_manager.h" using namespace std; @@ -315,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) @@ -360,9 +358,6 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); - - delete d_unconstrainedSimp; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2146,11 +2141,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector }); } -void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) -{ - d_unconstrainedSimp->processAssertions(assertions); -} - void TheoryEngine::setUserAttribute(const std::string& attr, Node n, const std::vector<Node>& node_values, |