diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 21:24:42 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-01 19:24:42 -0700 |
commit | ea426344ed44b28dcdbe4e631b52250ecef0551f (patch) | |
tree | 2d418d4691f49412761990e591092f304b92e380 /src | |
parent | 551f82a1398c97a5cd1f75b2c411b6fe464cc6ec (diff) |
Improvements and fixes in cegqi arithmetic (#2247)
This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.
It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.
This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 61 |
1 files changed, 49 insertions, 12 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 5cd7a6892..f1235d185 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -20,6 +20,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/term_util.h" +#include "util/random.h" using namespace std; using namespace CVC4::kind; @@ -118,7 +119,7 @@ bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, Node pv, CegInstEffort effort) { - return true; + return effort != CEG_INST_EFFORT_FULL; } Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, @@ -128,10 +129,9 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, CegInstEffort effort) { Node atom = lit.getKind() == NOT ? lit[0] : lit; - bool pol = lit.getKind() != NOT; // arithmetic inequalities and disequalities if (atom.getKind() == GEQ - || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) + || (atom.getKind() == EQUAL && atom[0].getType().isReal())) { return lit; } @@ -150,7 +150,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, bool pol = lit.getKind() != NOT; // arithmetic inequalities and disequalities Assert(atom.getKind() == GEQ - || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())); + || (atom.getKind() == EQUAL && atom[0].getType().isReal())); // get model value for pv Node pv_value = ci->getModelValue(pv); // cannot contain infinity? @@ -165,8 +165,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { return false; } - // disequalities are either strict upper or lower bounds - unsigned rmax = (atom.getKind() == GEQ || options::cbqiModel()) ? 1 : 2; + // compute how many bounds we will consider + unsigned rmax = 1; + if (atom.getKind() == EQUAL && (pol || !options::cbqiModel())) + { + rmax = 2; + } for (unsigned r = 0; r < rmax; r++) { int uires = ires; @@ -190,8 +194,14 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } } } + else if (pol) + { + // equalities are both non-strict upper and lower bounds + uires = r == 0 ? 1 : -1; + } else { + // disequalities are either strict upper or lower bounds bool is_upper; if (options::cbqiModel()) { @@ -226,11 +236,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); cmp = Rewriter::rewrite(cmp); Assert(cmp.isConst()); - is_upper = (cmp != ci->getQuantifiersEngine()->getTermUtil()->d_true); + is_upper = !cmp.isConst() || !cmp.getConst<bool>(); } } else { + // since we are not using the model, we try both. is_upper = (r == 0); } Assert(atom.getKind() == EQUAL && !pol); @@ -319,7 +330,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, bool use_inf = ci->useVtsInfinity() && (d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal()); - bool upper_first = false; + bool upper_first = Random::getRandom().pickWithProb(0.5); if (options::cbqiMinBounds()) { upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); @@ -353,6 +364,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } else @@ -389,6 +404,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, t_values[rr].push_back(Node::null()); // check if it is better than the current best bound : lexicographic // order infinite/finite/infinitesimal parts + bool new_best_set = false; bool new_best = true; for (unsigned t = 0; t < 3; t++) { @@ -435,8 +451,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, value[t]); value[t] = Rewriter::rewrite(value[t]); } - // check if new best - if (best != -1) + // check if new best, if we have not already set it. + if (best != -1 && !new_best_set) { Assert(!value[t].isNull() && !best_bound_value[t].isNull()); if (value[t] != best_bound_value[t]) @@ -444,12 +460,17 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Kind k = rr == 0 ? GEQ : LEQ; Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); cmp_bound = Rewriter::rewrite(cmp_bound); - if (cmp_bound - != ci->getQuantifiersEngine()->getTermUtil()->d_true) + // Should be comparing two constant values which should rewrite + // to a constant. If a step failed, we assume that this is not + // the new best bound. + Assert(cmp_bound.isConst()); + if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>()) { new_best = false; break; } + // indicate that the value of new_best is now established. + new_best_set = true; } } } @@ -504,6 +525,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } } @@ -531,6 +556,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } if (options::cbqiMidpoint() && !d_type.isInteger()) @@ -598,6 +627,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } // generally should not make it to this point, unless we are using a @@ -637,6 +670,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } + else if (!options::cbqiMultiInst()) + { + return false; + } } } } |