From ea426344ed44b28dcdbe4e631b52250ecef0551f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Aug 2018 21:24:42 -0500 Subject: [PATCH] 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. --- .../cegqi/ceg_arith_instantiator.cpp | 61 +++++++++++++++---- test/regress/Makefile.tests | 2 + .../quantifiers/RND_4_1-existing-inst.smt2 | 15 +++++ .../quantifiers/repair-const-nterm.smt2 | 12 ++++ 4 files changed, 78 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 create mode 100644 test/regress/regress1/quantifiers/repair-const-nterm.smt2 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(); } } 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()) { 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; + } } } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0b9e415fa..017e4f9bd 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1251,6 +1251,7 @@ REG1_TESTS = \ regress1/quantifiers/NUM878.smt2 \ regress1/quantifiers/RND-small.smt2 \ regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \ + regress1/quantifiers/RND_4_1-existing-inst.smt2 \ regress1/quantifiers/RND_4_16.smt2 \ regress1/quantifiers/anti-sk-simp.smt2 \ regress1/quantifiers/ari118-bv-2occ-x.smt2 \ @@ -1308,6 +1309,7 @@ REG1_TESTS = \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ + regress1/quantifiers/repair-const-nterm.smt2 \ regress1/quantifiers/recfact.cvc \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ diff --git a/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 new file mode 100644 index 000000000..73c278522 --- /dev/null +++ b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 @@ -0,0 +1,15 @@ +(set-logic LRA) +(set-info :status unsat) +(declare-fun a () Real) +(assert + (forall ((?y2 Real) (?y3 Real)) + (or + (= ?y3 1) + (> ?y3 0) + (and + (< ?y2 0) + (< ?y3 49) + ))) +) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/repair-const-nterm.smt2 b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 new file mode 100644 index 000000000..f9b1d6829 --- /dev/null +++ b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status unsat) + +(declare-fun k_20 () Int) +(declare-fun k_72 () Int) +(declare-fun k_73 () Int) + +(assert +(forall ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) (not (>= (+ (* 3 x7) (* (- 1) (ite (= x7 k_20) k_72 k_73))) 1)) ) +) + +(check-sat) -- 2.30.2