diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 456fdb746..b75140bc7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -27,6 +27,8 @@ #include "util/rational.h" #include "util/integer.h" +#include "theory/rewriter.h" + #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" @@ -79,6 +81,8 @@ TheoryArith::Statistics::Statistics(): d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), + d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0), + d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"), d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0), d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"), d_tableauResets("theory::arith::tableauResets", 0), @@ -93,6 +97,9 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); StatisticsRegistry::registerStat(&d_presolveTime); + StatisticsRegistry::registerStat(&d_miplibtrickApplications); + StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues); + StatisticsRegistry::registerStat(&d_initialTableauDensity); StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart); StatisticsRegistry::registerStat(&d_tableauResets); @@ -109,19 +116,43 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); StatisticsRegistry::unregisterStat(&d_presolveTime); + StatisticsRegistry::unregisterStat(&d_miplibtrickApplications); + StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues); + StatisticsRegistry::unregisterStat(&d_initialTableauDensity); StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart); StatisticsRegistry::unregisterStat(&d_tableauResets); StatisticsRegistry::unregisterStat(&d_restartTimer); } +#include "util/propositional_query.h" void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); + /* + if(Debug.isOn("prop::static")){ + Debug("prop::static") << n << "is " + << prop::PropositionalQuery::isSatisfiable(n) + << endl; + } + */ + vector<TNode> workList; workList.push_back(n); __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + //Contains an underapproximation of nodes that must hold. + __gnu_cxx::hash_set<TNode, TNodeHashFunction> defTrue; + + /* Maps a variable, x, to the set of defTrue nodes of the form + * (=> _ (= x c)) + * where c is a constant. + */ + typedef __gnu_cxx::hash_map<TNode, set<TNode>, TNodeHashFunction> VarToNodeSetMap; + VarToNodeSetMap miplibTrick; + + defTrue.insert(n); + while(!workList.empty()) { n = workList.back(); @@ -133,6 +164,11 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { unprocessedChildren = true; } } + if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){ + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { + defTrue.insert(*i); + } + } if(unprocessedChildren) { continue; @@ -202,6 +238,105 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl; learned << nGeqMin << nLeqMax; } + // == 3-FINITE VALUE SET : Collect information == + if(n.getKind() == IMPLIES && + n[1].getKind() == EQUAL && + n[1][0].getMetaKind() == metakind::VARIABLE && + 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]; + if(miplibTrick.find(var) == miplibTrick.end()){ + //[MGD] commented out following line as per TAK's instructions + //miplibTrick.insert(make_pair(var, set<TNode>())); + } + //[MGD] commented out following line as per TAK's instructions + //miplibTrick[var].insert(n); + Debug("arith::miplib") << "insert " << var << " const " << n << endl; + } + } + } + + // == 3-FINITE VALUE SET == + VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end(); + for(; i != endMipLibTrick; ++i){ + TNode var = i->first; + const set<TNode>& imps = i->second; + + Assert(!imps.empty()); + vector<Node> conditions; + vector<Rational> valueCollection; + set<TNode>::const_iterator j=imps.begin(), impsEnd=imps.end(); + for(; j != impsEnd; ++j){ + TNode imp = *j; + Assert(imp.getKind() == IMPLIES); + Assert(defTrue.find(imp) != defTrue.end()); + 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]); + valueCollection.push_back(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)){ + Debug("arith::miplib") << var << " found a tautology!"<< endl; + + set<Rational> values(valueCollection.begin(), valueCollection.end()); + 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; + } + } } } |