diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-31 14:29:12 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:38:16 -0500 |
commit | 458d47b2330418fb0045197e12edc9c730034180 (patch) | |
tree | 13c767477c56aff45a5dadaf85eb1a399381d05a /src/theory | |
parent | 651d533ab9f0ef9c8ffa89fa056be5714e16b227 (diff) |
Remove old miplibtrick from arith static learner
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 131 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 18 |
2 files changed, 1 insertions, 148 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 4ee176cf1..124fa8e2a 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -21,8 +21,6 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/options.h" -#include "util/propositional_query.h" - #include "expr/expr.h" #include "expr/convenience_node_builders.h" @@ -37,7 +35,6 @@ namespace arith { ArithStaticLearner::ArithStaticLearner(context::Context* userContext) : - d_miplibTrick(userContext), d_minMap(userContext), d_maxMap(userContext), d_statistics() @@ -45,30 +42,17 @@ ArithStaticLearner::ArithStaticLearner(context::Context* userContext) : ArithStaticLearner::Statistics::Statistics(): d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0), - d_iteConstantApplications("theory::arith::iteConstantApplications", 0), - d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0), - d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues") + d_iteConstantApplications("theory::arith::iteConstantApplications", 0) { StatisticsRegistry::registerStat(&d_iteMinMaxApplications); StatisticsRegistry::registerStat(&d_iteConstantApplications); - StatisticsRegistry::registerStat(&d_miplibtrickApplications); - StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues); } ArithStaticLearner::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications); StatisticsRegistry::unregisterStat(&d_iteConstantApplications); - StatisticsRegistry::unregisterStat(&d_miplibtrickApplications); - StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues); -} - -void ArithStaticLearner::miplibTrickInsert(Node key, Node value){ - if(options::arithMLTrick()){ - d_miplibTrick.insert(key, value); - } } - void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ vector<TNode> workList; @@ -111,8 +95,6 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ process(n,learned, defTrue); } - - postProcess(learned); } @@ -134,24 +116,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet iteConstant(n, learned); } break; - case IMPLIES: - // == 3-FINITE VALUE SET : Collect information == - if(n[1].getKind() == EQUAL && - n[1][0].isVar() && - defTrue.find(n) != defTrue.end()){ - Node eqTo = n[1][1]; - Node rewriteEqTo = Rewriter::rewrite(eqTo); - if(rewriteEqTo.getKind() == CONST_RATIONAL){ - - TNode var = n[1][0]; - Node current = (d_miplibTrick.find(var) == d_miplibTrick.end()) ? - mkBoolNode(false) : d_miplibTrick[var]; - - miplibTrickInsert(var, n.orNode(current)); - Debug("arith::miplib") << "insert " << var << " const " << n << endl; - } - } - break; case CONST_RATIONAL: // Mark constants as minmax d_minMap.insert(n, n.getConst<Rational>()); @@ -300,99 +264,6 @@ std::set<Node> listToSet(TNode l){ return ret; } -void ArithStaticLearner::postProcess(NodeBuilder<>& learned){ - // == 3-FINITE VALUE SET == - CDNodeToNodeListMap::const_iterator keyIter = d_miplibTrick.begin(); - CDNodeToNodeListMap::const_iterator endKeys = d_miplibTrick.end(); - while(keyIter != endKeys) { - TNode var = (*keyIter).first; - Node list = (*keyIter).second; - const set<Node> imps = listToSet(list); - - if(imps.empty()){ - ++keyIter; - continue; - } - - Assert(!imps.empty()); - vector<Node> conditions; - set<Rational> values; - set<Node>::const_iterator j=imps.begin(), impsEnd=imps.end(); - for(; j != impsEnd; ++j){ - TNode imp = *j; - Assert(imp.getKind() == IMPLIES); - Assert(imp[1].getKind() == EQUAL); - - Node eqTo = imp[1][1]; - Node rewriteEqTo = Rewriter::rewrite(eqTo); - Assert(rewriteEqTo.getKind() == CONST_RATIONAL); - - conditions.push_back(imp[0]); - values.insert(rewriteEqTo.getConst<Rational>()); - } - - Node possibleTaut = Node::null(); - if(conditions.size() == 1){ - possibleTaut = conditions.front(); - }else{ - NodeBuilder<> orBuilder(OR); - orBuilder.append(conditions); - possibleTaut = orBuilder; - } - - - Debug("arith::miplib") << "var: " << var << endl; - Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl; - - Result isTaut = PropositionalQuery::isTautology(possibleTaut); - if(isTaut == Result(Result::VALID)){ - miplibTrick(var, values, learned); - miplibTrickInsert(var, mkBoolNode(false)); - } - ++keyIter; - } -} - - -void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuilder<>& learned){ - - Debug("arith::miplib") << var << " found a tautology!"<< endl; - - const Rational& min = *(values.begin()); - const Rational& max = *(values.rbegin()); - - Debug("arith::miplib") << "min: " << min << endl; - Debug("arith::miplib") << "max: " << max << endl; - - Assert(min <= max); - ++(d_statistics.d_miplibtrickApplications); - (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size()); - - Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min); - Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max); - Debug("arith::miplib") << nGeqMin << nLeqMax << endl; - learned << nGeqMin << nLeqMax; - set<Rational>::iterator valuesIter = values.begin(); - set<Rational>::iterator valuesEnd = values.end(); - set<Rational>::iterator valuesPrev = valuesIter; - ++valuesIter; - for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){ - const Rational& prev = *valuesPrev; - const Rational& curr = *valuesIter; - Assert(prev < curr); - - //The interval (last,curr) can be excluded: - //(not (and (> var prev) (< var curr)) - //<=> (or (not (> var prev)) (not (< var curr))) - //<=> (or (<= var prev) (>= var curr)) - Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev); - Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr); - Node excludedMiddle = NodeBuilder<2>(OR) << leqPrev << geqCurr; - Debug("arith::miplib") << excludedMiddle << endl; - learned << excludedMiddle; - } -} - void ArithStaticLearner::addBound(TNode n) { CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]); diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 041ae6339..48ee6a3bb 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -37,16 +37,6 @@ namespace arith { class ArithStaticLearner { private: - /* Maps a variable, x, to the set of defTrue nodes of the form - * (=> _ (= x c)) - * where c is a constant. - */ - typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap; - // The domain is an implicit list OR(x, OR(y, ..., FALSE )) - // or FALSE - CDNodeToNodeListMap d_miplibTrick; - void miplibTrickInsert(Node key, Node value); - /** * Map from a node to it's minimum and maximum. */ @@ -63,23 +53,15 @@ public: private: void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue); - void postProcess(NodeBuilder<>& learned); - void iteMinMax(TNode n, NodeBuilder<>& learned); void iteConstant(TNode n, NodeBuilder<>& learned); - void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); - - /** These fields are designed to be accessible to ArithStaticLearner methods. */ class Statistics { public: IntStat d_iteMinMaxApplications; IntStat d_iteConstantApplications; - IntStat d_miplibtrickApplications; - AverageStat d_avgNumMiplibtrickValues; - Statistics(); ~Statistics(); }; |