diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-16 15:36:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-16 15:36:45 +0000 |
commit | ecff741b43b7c5493a7e1ef801cbe7ff68f8ff54 (patch) | |
tree | 002caa8263ff2b9ccb4873db1e0b0e1d55aedf7e | |
parent | 4ee5a74967c9cd273ca3449b948ac8a12834991c (diff) |
- Turns on the miplibTrick. This detects during the static learning phase a set of nodes that are asserted to the theory of the form (=> p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2, ...}. (This tautology check currently requires CUDD to be installed.) Right now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare jobs 1728 to 1626 for how this affects the miplib examples.)
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 47 |
1 files changed, 12 insertions, 35 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b75140bc7..09bb48c8a 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -129,14 +129,6 @@ TheoryArith::Statistics::~Statistics(){ 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; @@ -249,11 +241,9 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { 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>())); + miplibTrick.insert(make_pair(var, set<TNode>())); } - //[MGD] commented out following line as per TAK's instructions - //miplibTrick[var].insert(n); + miplibTrick[var].insert(n); Debug("arith::miplib") << "insert " << var << " const " << n << endl; } } @@ -301,9 +291,15 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { 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()); + vector<Rational>::iterator minIter, maxIter; + minIter = std::min_element(valueCollection.begin(), valueCollection.end()); + maxIter = std::max_element(valueCollection.begin(), valueCollection.end()); + + Assert(minIter != valueCollection.end()); + Assert(maxIter != valueCollection.end()); + + const Rational& min = *minIter; + const Rational& max = *maxIter; Debug("arith::miplib") << "min: " << min << endl; Debug("arith::miplib") << "max: " << max << endl; @@ -311,31 +307,12 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { Assert(min <= max); ++(d_statistics.d_miplibtrickApplications); - (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size()); + (d_statistics.d_avgNumMiplibtrickValues).addEntry(valueCollection.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; - } } } } |