From 84146b42ed0e1c0298b0e2a894c33f357a4483ef Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 16 Mar 2011 22:08:15 +0000 Subject: [PATCH] - Turns on the excluded middle assertions during the miplibTrick. If it is known that x \in {c_i}, then x is not in the interval (c_{i}, c_{i+1}) (assuming the c_i's are sorted). (Compare jobs 1742 and 1739 for the expected performance change on trunk. Compare jobs 1740 and 1738 for the expected performance change with the rewrite-equality patch.) --- src/theory/arith/theory_arith.cpp | 34 +++++++++++++++++++++---------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 09bb48c8a..c0e7057c2 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -291,28 +291,40 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { if(isTaut == Result(Result::VALID)){ Debug("arith::miplib") << var << " found a tautology!"<< endl; - vector::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; + set 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(valueCollection.size()); + (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::iterator valuesIter = values.begin(); + set::iterator valuesEnd = values.end(); + set::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; + } } } } -- 2.30.2