From: Andrew Reynolds Date: Thu, 28 Jun 2018 15:43:08 +0000 (-0500) Subject: Split and document ceg theory instantiators (#2094) X-Git-Tag: cvc5-1.0.0~4938 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d83f8bebccffdb677652706f4eb3a2fff056587c;p=cvc5.git Split and document ceg theory instantiators (#2094) --- diff --git a/src/Makefile.am b/src/Makefile.am index b81d93081..b60cede21 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -391,8 +391,14 @@ libcvc4_la_SOURCES = \ theory/quantifiers/candidate_rewrite_database.h \ theory/quantifiers/cegqi/ceg_instantiator.cpp \ theory/quantifiers/cegqi/ceg_instantiator.h \ - theory/quantifiers/cegqi/ceg_t_instantiator.cpp \ - theory/quantifiers/cegqi/ceg_t_instantiator.h \ + theory/quantifiers/cegqi/ceg_arith_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_arith_instantiator.h \ + theory/quantifiers/cegqi/ceg_bv_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_bv_instantiator.h \ + theory/quantifiers/cegqi/ceg_dt_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_dt_instantiator.h \ + theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_epr_instantiator.h \ theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \ theory/quantifiers/cegqi/inst_strategy_cbqi.h \ theory/quantifiers/conjecture_generator.cpp \ diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp new file mode 100644 index 000000000..5cd7a6892 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -0,0 +1,997 @@ +/********************* */ +/*! \file ceg_arith_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of ceg_arith_instantiator + **/ + +#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h" + +#include "options/quantifiers_options.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/quantifiers/term_util.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +ArithInstantiator::ArithInstantiator(QuantifiersEngine* qe, TypeNode tn) + : Instantiator(qe, tn) +{ + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); +} + +void ArithInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( + d_type, false, false); + d_vts_sym[1] = + ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(false, false); + for (unsigned i = 0; i < 2; i++) + { + d_mbp_bounds[i].clear(); + d_mbp_coeff[i].clear(); + for (unsigned j = 0; j < 2; j++) + { + d_mbp_vts_coeff[i][j].clear(); + } + d_mbp_lit[i].clear(); + } +} + +bool ArithInstantiator::hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return true; +} + +bool ArithInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + CegInstEffort effort) +{ + NodeManager* nm = NodeManager::currentNM(); + Node eq_lhs = terms[0]; + Node eq_rhs = terms[1]; + Node lhs_coeff = term_props[0].d_coeff; + Node rhs_coeff = term_props[1].d_coeff; + // make the same coefficient + if (rhs_coeff != lhs_coeff) + { + if (!rhs_coeff.isNull()) + { + Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; + eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs); + eq_lhs = Rewriter::rewrite(eq_lhs); + } + if (!lhs_coeff.isNull()) + { + Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; + eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs); + eq_rhs = Rewriter::rewrite(eq_rhs); + } + } + Node eq = eq_lhs.eqNode(eq_rhs); + eq = Rewriter::rewrite(eq); + Node val; + TermProperties pv_prop; + Node vts_coeff_inf; + Node vts_coeff_delta; + // isolate pv in the equality + int ires = solve_arith( + ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); + if (ires != 0) + { + pv_prop.d_type = 0; + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { + return true; + } + } + return false; +} + +bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return true; +} + +Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + 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())) + { + return lit; + } + return Node::null(); +} + +bool ArithInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + NodeManager* nm = NodeManager::currentNM(); + Node atom = lit.getKind() == NOT ? lit[0] : lit; + bool pol = lit.getKind() != NOT; + // arithmetic inequalities and disequalities + Assert(atom.getKind() == GEQ + || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())); + // get model value for pv + Node pv_value = ci->getModelValue(pv); + // cannot contain infinity? + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + TermProperties pv_prop; + // isolate pv in the inequality + int ires = solve_arith( + ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); + if (ires == 0) + { + return false; + } + // disequalities are either strict upper or lower bounds + unsigned rmax = (atom.getKind() == GEQ || options::cbqiModel()) ? 1 : 2; + for (unsigned r = 0; r < rmax; r++) + { + int uires = ires; + Node uval = val; + if (atom.getKind() == GEQ) + { + // push negation downwards + if (!pol) + { + uires = -ires; + if (d_type.isInteger()) + { + uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires))); + uval = Rewriter::rewrite(uval); + } + else + { + Assert(d_type.isReal()); + // now is strict inequality + uires = uires * 2; + } + } + } + else + { + bool is_upper; + if (options::cbqiModel()) + { + // disequality is a disjunction : only consider the bound in the + // direction of the model + // first check if there is an infinity... + if (!vts_coeff_inf.isNull()) + { + // coefficient or val won't make a difference, just compare with zero + Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " + << vts_coeff_inf << std::endl; + Assert(vts_coeff_inf.isConst()); + is_upper = (vts_coeff_inf.getConst().sgn() == 1); + } + else + { + Node rhs_value = ci->getModelValue(val); + Node lhs_value = pv_prop.getModifiedTerm(pv_value); + if (!pv_prop.isBasic()) + { + lhs_value = pv_prop.getModifiedTerm(pv_value); + lhs_value = Rewriter::rewrite(lhs_value); + } + Trace("cegqi-arith-debug") + << "Disequality : check model values " << lhs_value << " " + << rhs_value << std::endl; + // it generally should be the case that lhs_value!=rhs_value + // however, this assertion is violated e.g. if non-linear is enabled + // since the quantifier-free arithmetic solver may pass full + // effort with no lemmas even when we are not guaranteed to have a + // model. By convention, we use GEQ to compare the values here. + Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); + cmp = Rewriter::rewrite(cmp); + Assert(cmp.isConst()); + is_upper = (cmp != ci->getQuantifiersEngine()->getTermUtil()->d_true); + } + } + else + { + is_upper = (r == 0); + } + Assert(atom.getKind() == EQUAL && !pol); + if (d_type.isInteger()) + { + uires = is_upper ? -1 : 1; + uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires))); + uval = Rewriter::rewrite(uval); + } + else + { + Assert(d_type.isReal()); + uires = is_upper ? -2 : 2; + } + } + if (Trace.isOn("cegqi-arith-bound-inf")) + { + Node pvmod = pv_prop.getModifiedTerm(pv); + Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : "; + Trace("cegqi-arith-bound-inf") + << pvmod << " -> " << uval << ", styp = " << uires << std::endl; + } + // take into account delta + if (ci->useVtsDelta() && (uires == 2 || uires == -2)) + { + if (options::cbqiModel()) + { + Node delta_coeff = nm->mkConst(Rational(uires > 0 ? 1 : -1)); + if (vts_coeff_delta.isNull()) + { + vts_coeff_delta = delta_coeff; + } + else + { + vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff); + vts_coeff_delta = Rewriter::rewrite(vts_coeff_delta); + } + } + else + { + Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(); + uval = nm->mkNode(uires == 2 ? PLUS : MINUS, uval, delta); + uval = Rewriter::rewrite(uval); + } + } + if (options::cbqiModel()) + { + // just store bounds, will choose based on tighest bound + unsigned index = uires > 0 ? 0 : 1; + d_mbp_bounds[index].push_back(uval); + d_mbp_coeff[index].push_back(pv_prop.d_coeff); + Trace("cegqi-arith-debug") + << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff + << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit + << std::endl; + for (unsigned t = 0; t < 2; t++) + { + d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf + : vts_coeff_delta); + } + d_mbp_lit[index].push_back(lit); + } + else + { + // try this bound + pv_prop.d_type = uires > 0 ? 1 : -1; + if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) + { + return true; + } + } + } + return false; +} + +bool ArithInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + if (!options::cbqiModel()) + { + return false; + } + NodeManager* nm = NodeManager::currentNM(); + bool use_inf = ci->useVtsInfinity() + && (d_type.isInteger() ? options::cbqiUseInfInt() + : options::cbqiUseInfReal()); + bool upper_first = false; + if (options::cbqiMinBounds()) + { + upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); + } + int best_used[2]; + std::vector t_values[3]; + Node pv_value = ci->getModelValue(pv); + // try optimal bounds + for (unsigned r = 0; r < 2; r++) + { + int rr = upper_first ? (1 - r) : r; + best_used[rr] = -1; + if (d_mbp_bounds[rr].empty()) + { + if (use_inf) + { + Trace("cegqi-arith-bound") + << "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv + << " (type=" << d_type << ")" << std::endl; + // no bounds, we do +- infinity + Node val = + ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(d_type); + // could get rho value for infinity here + if (rr == 0) + { + val = nm->mkNode(UMINUS, val); + val = Rewriter::rewrite(val); + } + TermProperties pv_prop_no_bound; + if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) + { + return true; + } + } + } + else + { + Trace("cegqi-arith-bound") + << (rr == 0 ? "Lower" : "Upper") << " bounds for " << pv + << " (type=" << d_type << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) + { + Node value[3]; + if (Trace.isOn("cegqi-arith-bound")) + { + Assert(!d_mbp_bounds[rr][j].isNull()); + Trace("cegqi-arith-bound") + << " " << j << ": " << d_mbp_bounds[rr][j]; + if (!d_mbp_vts_coeff[rr][0][j].isNull()) + { + Trace("cegqi-arith-bound") + << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if (!d_mbp_vts_coeff[rr][1][j].isNull()) + { + Trace("cegqi-arith-bound") + << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if (!d_mbp_coeff[rr][j].isNull()) + { + Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")"; + } + Trace("cegqi-arith-bound") << ", value = "; + } + 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 = true; + for (unsigned t = 0; t < 3; t++) + { + // get the value + if (t == 0) + { + value[0] = d_mbp_vts_coeff[rr][0][j]; + if (!value[0].isNull()) + { + Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + "; + } + else + { + value[0] = d_zero; + } + } + else if (t == 1) + { + Node t_value = ci->getModelValue(d_mbp_bounds[rr][j]); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cegqi-arith-bound") << value[1]; + } + else + { + value[2] = d_mbp_vts_coeff[rr][1][j]; + if (!value[2].isNull()) + { + Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; + } + else + { + value[2] = d_zero; + } + } + // multiply by coefficient + if (value[t] != d_zero && !d_mbp_coeff[rr][j].isNull()) + { + Assert(d_mbp_coeff[rr][j].isConst()); + value[t] = nm->mkNode( + MULT, + nm->mkConst(Rational(1) + / d_mbp_coeff[rr][j].getConst()), + value[t]); + value[t] = Rewriter::rewrite(value[t]); + } + // check if new best + if (best != -1) + { + Assert(!value[t].isNull() && !best_bound_value[t].isNull()); + if (value[t] != best_bound_value[t]) + { + 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) + { + new_best = false; + break; + } + } + } + } + Trace("cegqi-arith-bound") << std::endl; + if (new_best) + { + for (unsigned t = 0; t < 3; t++) + { + best_bound_value[t] = value[t]; + } + best = j; + } + } + if (best != -1) + { + Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; + if (best_bound_value[0] != d_zero) + { + Trace("cegqi-arith-bound") + << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cegqi-arith-bound") << best_bound_value[1]; + if (best_bound_value[2] != d_zero) + { + Trace("cegqi-arith-bound") + << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cegqi-arith-bound") << std::endl; + best_used[rr] = best; + // if using cbqiMidpoint, only add the instance based on one bound if + // the bound is non-strict + if (!options::cbqiMidpoint() || d_type.isInteger() + || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull())) + { + Node val = d_mbp_bounds[rr][best]; + val = getModelBasedProjectionValue(ci, + pv, + val, + rr == 0, + d_mbp_coeff[rr][best], + pv_value, + t_values[rr][best], + sf.getTheta(), + d_mbp_vts_coeff[rr][0][best], + d_mbp_vts_coeff[rr][1][best]); + if (!val.isNull()) + { + TermProperties pv_prop_bound; + pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; + pv_prop_bound.d_type = rr == 0 ? 1 : -1; + if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) + { + return true; + } + } + } + } + } + } + // if not using infinity, use model value of zero + if (!use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty()) + { + Node val = d_zero; + TermProperties pv_prop_zero; + Node theta = sf.getTheta(); + val = getModelBasedProjectionValue(ci, + pv, + val, + true, + pv_prop_zero.d_coeff, + pv_value, + d_zero, + sf.getTheta(), + Node::null(), + Node::null()); + if (!val.isNull()) + { + if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) + { + return true; + } + } + } + if (options::cbqiMidpoint() && !d_type.isInteger()) + { + Node vals[2]; + bool bothBounds = true; + Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; + for (unsigned rr = 0; rr < 2; rr++) + { + int best = best_used[rr]; + if (best == -1) + { + bothBounds = false; + } + else + { + vals[rr] = d_mbp_bounds[rr][best]; + vals[rr] = getModelBasedProjectionValue(ci, + pv, + vals[rr], + rr == 0, + Node::null(), + pv_value, + t_values[rr][best], + sf.getTheta(), + d_mbp_vts_coeff[rr][0][best], + Node::null()); + } + Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; + } + Node val; + if (bothBounds) + { + Assert(!vals[0].isNull() && !vals[1].isNull()); + if (vals[0] == vals[1]) + { + val = vals[0]; + } + else + { + val = nm->mkNode(MULT, + nm->mkNode(PLUS, vals[0], vals[1]), + nm->mkConst(Rational(1) / Rational(2))); + val = Rewriter::rewrite(val); + } + } + else + { + if (!vals[0].isNull()) + { + val = nm->mkNode(PLUS, vals[0], d_one); + val = Rewriter::rewrite(val); + } + else if (!vals[1].isNull()) + { + val = nm->mkNode(MINUS, vals[1], d_one); + val = Rewriter::rewrite(val); + } + } + Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; + if (!val.isNull()) + { + TermProperties pv_prop_midpoint; + if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) + { + return true; + } + } + } + // generally should not make it to this point, unless we are using a + // non-monotonic selection function + + if (!options::cbqiNopt()) + { + // if not trying non-optimal bounds, return + return false; + } + // try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; + for (unsigned r = 0; r < 2; r++) + { + int rr = upper_first ? (1 - r) : r; + for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) + { + if ((int)j != best_used[rr] + && (!options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull())) + { + Node val = getModelBasedProjectionValue(ci, + pv, + d_mbp_bounds[rr][j], + rr == 0, + d_mbp_coeff[rr][j], + pv_value, + t_values[rr][j], + sf.getTheta(), + d_mbp_vts_coeff[rr][0][j], + d_mbp_vts_coeff[rr][1][j]); + if (!val.isNull()) + { + TermProperties pv_prop_nopt_bound; + pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; + pv_prop_nopt_bound.d_type = rr == 0 ? 1 : -1; + if (ci->constructInstantiationInc(pv, val, pv_prop_nopt_bound, sf)) + { + return true; + } + } + } + } + } + return false; +} + +bool ArithInstantiator::needsPostProcessInstantiationForVariable( + CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) +{ + return std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) + != sf.d_non_basic.end(); +} + +bool ArithInstantiator::postProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector& lemmas) +{ + Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) + != sf.d_non_basic.end()); + Assert(std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) != sf.d_vars.end()); + unsigned index = + std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) - sf.d_vars.begin(); + Assert(!sf.d_props[index].isBasic()); + Node eq_lhs = sf.d_props[index].getModifiedTerm(sf.d_vars[index]); + if (Trace.isOn("cegqi-arith-debug")) + { + Trace("cegqi-arith-debug") << "Normalize substitution for "; + Trace("cegqi-arith-debug") + << eq_lhs << " = " << sf.d_subs[index] << std::endl; + } + Assert(sf.d_vars[index].getType().isInteger()); + // must ensure that divisibility constraints are met + // solve updated rewritten equality for vars[index], if coefficient is one, + // then we are successful + Node eq_rhs = sf.d_subs[index]; + Node eq = eq_lhs.eqNode(eq_rhs); + eq = Rewriter::rewrite(eq); + Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; + std::map msum; + if (!ArithMSum::getMonomialSumLit(eq, msum)) + { + Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; + return false; + } + Node veq; + if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) == 0) + { + Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; + return false; + } + Node veq_c; + if (veq[0] != sf.d_vars[index]) + { + Node veq_v; + if (ArithMSum::getMonomial(veq[0], veq_c, veq_v)) + { + Assert(veq_v == sf.d_vars[index]); + } + } + sf.d_subs[index] = veq[1]; + if (!veq_c.isNull()) + { + NodeManager* nm = NodeManager::currentNM(); + sf.d_subs[index] = nm->mkNode(INTS_DIVISION_TOTAL, veq[1], veq_c); + Trace("cegqi-arith-debug") + << "...bound type is : " << sf.d_props[index].d_type << std::endl; + // intger division rounding up if from a lower bound + if (sf.d_props[index].d_type == 1 && options::cbqiRoundUpLowerLia()) + { + sf.d_subs[index] = nm->mkNode( + PLUS, + sf.d_subs[index], + nm->mkNode( + ITE, + nm->mkNode( + EQUAL, nm->mkNode(INTS_MODULUS_TOTAL, veq[1], veq_c), d_zero), + d_zero, + d_one)); + } + } + Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] + << " -> " << sf.d_subs[index] << std::endl; + return true; +} + +int ArithInstantiator::solve_arith(CegInstantiator* ci, + Node pv, + Node atom, + Node& veq_c, + Node& val, + Node& vts_coeff_inf, + Node& vts_coeff_delta) +{ + NodeManager* nm = NodeManager::currentNM(); + int ires = 0; + Trace("cegqi-arith-debug") + << "isolate for " << pv << " in " << atom << std::endl; + std::map msum; + if (!ArithMSum::getMonomialSumLit(atom, msum)) + { + Trace("cegqi-arith-debug") + << "fail : could not get monomial sum" << std::endl; + return 0; + } + Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; + if (Trace.isOn("cegqi-arith-debug")) + { + ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug"); + } + TypeNode pvtn = pv.getType(); + // remove vts symbols from polynomial + Node vts_coeff[2]; + for (unsigned t = 0; t < 2; t++) + { + if (!d_vts_sym[t].isNull()) + { + std::map::iterator itminf = msum.find(d_vts_sym[t]); + if (itminf != msum.end()) + { + vts_coeff[t] = itminf->second; + if (vts_coeff[t].isNull()) + { + vts_coeff[t] = nm->mkConst(Rational(1)); + } + // negate if coefficient on variable is positive + std::map::iterator itv = msum.find(pv); + if (itv != msum.end()) + { + // multiply by the coefficient we will isolate for + if (itv->second.isNull()) + { + vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); + } + else + { + if (!pvtn.isInteger()) + { + vts_coeff[t] = nm->mkNode( + MULT, + nm->mkConst(Rational(-1) / itv->second.getConst()), + vts_coeff[t]); + vts_coeff[t] = Rewriter::rewrite(vts_coeff[t]); + } + else if (itv->second.getConst().sgn() == 1) + { + vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); + } + } + } + Trace("cegqi-arith-debug") + << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase(d_vts_sym[t]); + } + } + } + + ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); + if (ires == 0) + { + Trace("cegqi-arith-debug") << "fail : isolate" << std::endl; + return 0; + } + if (Trace.isOn("cegqi-arith-debug")) + { + Trace("cegqi-arith-debug") << "Isolate : "; + if (!veq_c.isNull()) + { + Trace("cegqi-arith-debug") << veq_c << " * "; + } + Trace("cegqi-arith-debug") + << pv << " " << atom.getKind() << " " << val << std::endl; + } + // when not pure LIA/LRA, we must check whether the lhs contains pv + if (val.hasSubterm(pv)) + { + Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; + return 0; + } + // if its type is integer but the substitution is not integer + if (pvtn.isInteger() + && ((!veq_c.isNull() && !veq_c.getType().isInteger()) + || !val.getType().isInteger())) + { + // redo, split integer/non-integer parts + bool useCoeff = false; + Integer coeff = ci->getQuantifiersEngine() + ->getTermUtil() + ->d_one.getConst() + .getNumerator(); + for (std::map::iterator it = msum.begin(); it != msum.end(); + ++it) + { + if (it->first.isNull() || it->first.getType().isInteger()) + { + if (!it->second.isNull()) + { + coeff = coeff.lcm(it->second.getConst().getDenominator()); + useCoeff = true; + } + } + } + // multiply everything by this coefficient + Node rcoeff = nm->mkConst(Rational(coeff)); + std::vector real_part; + for (std::map::iterator it = msum.begin(); it != msum.end(); + ++it) + { + if (useCoeff) + { + if (it->second.isNull()) + { + msum[it->first] = rcoeff; + } + else + { + msum[it->first] = + Rewriter::rewrite(nm->mkNode(MULT, it->second, rcoeff)); + } + } + if (!it->first.isNull() && !it->first.getType().isInteger()) + { + real_part.push_back(msum[it->first].isNull() + ? it->first + : nm->mkNode(MULT, msum[it->first], it->first)); + } + } + // remove delta + vts_coeff[1] = Node::null(); + // multiply inf + if (!vts_coeff[0].isNull()) + { + vts_coeff[0] = Rewriter::rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0])); + } + Node realPart = real_part.empty() + ? d_zero + : (real_part.size() == 1 ? real_part[0] + : nm->mkNode(PLUS, real_part)); + Assert(ci->getOutput()->isEligibleForInstantiation(realPart)); + // re-isolate + Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; + veq_c = Node::null(); + ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); + Trace("cegqi-arith-debug") + << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " + << atom.getKind() << " " << val << std::endl; + Trace("cegqi-arith-debug") + << " real part : " << realPart << std::endl; + if (ires != 0) + { + int ires_use = + (msum[pv].isNull() || msum[pv].getConst().sgn() == 1) ? 1 + : -1; + val = Rewriter::rewrite( + nm->mkNode(ires_use == -1 ? PLUS : MINUS, + nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart), + nm->mkNode(TO_INTEGER, realPart))); + // could round up for upper bounds here + Trace("cegqi-arith-debug") << "result : " << val << std::endl; + Assert(val.getType().isInteger()); + } + } + vts_coeff_inf = vts_coeff[0]; + vts_coeff_delta = vts_coeff[1]; + Trace("cegqi-arith-debug") + << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " + << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" + << std::endl; + return ires; +} + +Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, + Node e, + Node t, + bool isLower, + Node c, + Node me, + Node mt, + Node theta, + Node inf_coeff, + Node delta_coeff) +{ + NodeManager* nm = NodeManager::currentNM(); + Node val = t; + Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; + Assert(!e.getType().isInteger() || t.getType().isInteger()); + Assert(!e.getType().isInteger() || mt.getType().isInteger()); + // add rho value + // get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if (!c.isNull()) + { + Assert(c.getType().isInteger()); + ceValue = nm->mkNode(MULT, ceValue, c); + ceValue = Rewriter::rewrite(ceValue); + if (new_theta.isNull()) + { + new_theta = c; + } + else + { + new_theta = nm->mkNode(MULT, new_theta, c); + new_theta = Rewriter::rewrite(new_theta); + } + Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; + } + if (!new_theta.isNull() && e.getType().isInteger()) + { + Node rho; + if (isLower) + { + rho = nm->mkNode(MINUS, ceValue, mt); + } + else + { + rho = nm->mkNode(MINUS, mt, ceValue); + } + rho = Rewriter::rewrite(rho); + Trace("cegqi-arith-bound2") + << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cegqi-arith-bound2") + << "..." << rho << " mod " << new_theta << " = "; + rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); + rho = Rewriter::rewrite(rho); + Trace("cegqi-arith-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = nm->mkNode(rk, val, rho); + val = Rewriter::rewrite(val); + Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; + } + if (!inf_coeff.isNull()) + { + Assert(!d_vts_sym[0].isNull()); + val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); + val = Rewriter::rewrite(val); + } + if (!delta_coeff.isNull()) + { + // create delta here if necessary + val = nm->mkNode( + PLUS, + val, + nm->mkNode(MULT, + delta_coeff, + ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta())); + val = Rewriter::rewrite(val); + } + return val; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h new file mode 100644 index 000000000..b6e22329d --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -0,0 +1,206 @@ +/********************* */ +/*! \file ceg_arith_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ceg_arith_instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H + +#include +#include "expr/node.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Arithmetic instantiator + * + * This implements a selection function for arithmetic, which is based on + * variants of: + * - Loos/Weispfenning's method (virtual term substitution) for linear real + * arithmetic, + * - Ferrante/Rackoff's method (interior points) for linear real arithmetic, + * - Cooper's method for linear arithmetic. + * For details, see Reynolds et al, "Solving Linear Arithmetic Using + * Counterexample-Guided Instantiation", FMSD 2017. + * + * This class contains all necessary information for instantiating a single + * real or integer typed variable of a single quantified formula. + */ +class ArithInstantiator : public Instantiator +{ + public: + ArithInstantiator(QuantifiersEngine* qe, TypeNode tn); + virtual ~ArithInstantiator() {} + /** reset */ + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** this instantiator processes equalities */ + bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** + * Process the equality term[0]=term[1]. If this equality is equivalent to one + * of the form c * pv = t, then we add the substitution c * pv -> t to sf and + * recurse. + */ + bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + CegInstEffort effort) override; + /** this instantiator processes assertions */ + bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** this instantiator processes literals lit of kinds EQUAL and GEQ */ + Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) override; + /** process assertion lit + * + * If lit can be turned into a bound of the form c * pv <> t, then we store + * information about this bound (see d_mbp_bounds). + * + * If cbqiModel is false (not the default), we recursively try adding the + * substitution { c * pv -> t } to sf and recursing. + */ + bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) override; + /** process assertions + * + * This is called after processAssertion has been called on all current bounds + * for pv. This method selects the "best" bound of those we have seen, which + * can be one of the following: + * - Maximal lower bound, + * - Minimal upper bound, + * - Midpoint of maximal lower and minimal upper bounds, [if pv is not Int, + * and --cbqi-midpoint] + * - (+-) Infinity, [if no upper (resp. lower) bounds, and --cbqi-use-vts-inf] + * - Zero, [if no bounds] + * - Non-optimal bounds. [if the above bounds fail, and --cbqi-nopt] + */ + bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** + * This instantiator needs to postprocess variables that have substitutions + * with coefficients, i.e. c*x -> t. + */ + bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** post-process instantiation for variable + * + * If the solved form for integer variable pv is a substitution with + * coefficients c*x -> t, this turns its solved form into x -> div(t,c), where + * div is integer division. + */ + bool postProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector& lemmas) override; + std::string identify() const override { return "Arith"; } + + private: + /** zero/one */ + Node d_zero; + Node d_one; + //--------------------------------------current bounds + /** Virtual term symbols (vts), where 0: infinity, 1: delta. */ + Node d_vts_sym[2]; + /** Current 0:lower, 1:upper bounds for the variable to instantiate */ + std::vector d_mbp_bounds[2]; + /** Coefficients for the lower/upper bounds for the variable to instantiate */ + std::vector d_mbp_coeff[2]; + /** Coefficients for virtual terms for each bound. */ + std::vector d_mbp_vts_coeff[2][2]; + /** The source literal (explanation) for each bound. */ + std::vector d_mbp_lit[2]; + //--------------------------------------end current bounds + /** solve arith + * + * Given variable to instantiate pv, this isolates the atom into solved form: + * veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf + * where we ensure val has Int type if pv has Int type, and val does not + * contain vts symbols. + */ + int solve_arith(CegInstantiator* ci, + Node v, + Node atom, + Node& veq_c, + Node& val, + Node& vts_coeff_inf, + Node& vts_coeff_delta); + /** get model based projection value + * + * Given a implied (non-strict) bound: + * c*e <=/>= t + inf_coeff*INF + delta_coeff*DELTA + * this method returns ret, the minimal (resp. maximal) term such that: + * c*ret <> t + inf_coeff*INF + delta_coeff*DELTA + * is satisfied in the current model M, and such that the divisibilty + * constraint is also satisfied: + * ret^M mod c*theta = (c*e)^M mod c*theta + * where the input theta is a constant (which is assumed to be 1 if null). The + * values of me and mt are the current model values of e and t respectively. + * + * For example, if e has Real type and: + * isLower = false, e^M = 0, t^M = 2, inf_coeff = 0, delta_coeff = 2 + * Then, this function returns t+2*delta. + * + * For example, if e has Int type and: + * isLower = true, e^M = 4, t^M = 2, theta = 3 + * Then, this function returns t+2, noting that (t+2)^M mod 3 = e^M mod 3 = 2. + * + * For example, if e has Int type and: + * isLower = false, e^M = 1, t^M = 5, theta = 3 + * Then, this function returns t-1, noting that (t-1)^M mod 3 = e^M mod 3 = 1. + * + * The value that is added or substracted from t in the return value when e + * is an integer is the value of "rho" from Figure 6 of Reynolds et al, + * "Solving Linear Arithmetic Using Counterexample-Guided Instantiation", + * FMSD 2017. + */ + Node getModelBasedProjectionValue(CegInstantiator* ci, + Node e, + Node t, + bool isLower, + Node c, + Node me, + Node mt, + Node theta, + Node inf_coeff, + Node delta_coeff); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp new file mode 100644 index 000000000..678691ef4 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -0,0 +1,1139 @@ +/********************* */ +/*! \file ceg_bv_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of ceg_bv_instantiator + **/ + +#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" + +#include +#include "options/quantifiers_options.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" +#include "util/random.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +struct BvLinearAttributeId +{ +}; +using BvLinearAttribute = expr::Attribute; + +// this class can be used to query the model value through the CegInstaniator +// class +class CegInstantiatorBvInverterQuery : public BvInverterQuery +{ + public: + CegInstantiatorBvInverterQuery(CegInstantiator* ci) + : BvInverterQuery(), d_ci(ci) + { + } + ~CegInstantiatorBvInverterQuery() {} + /** return the model value of n */ + Node getModelValue(Node n) override { return d_ci->getModelValue(n); } + /** get bound variable of type tn */ + Node getBoundVariable(TypeNode tn) override + { + return d_ci->getBoundVariable(tn); + } + + protected: + // pointer to class that is able to query model values + CegInstantiator* d_ci; +}; + +BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) + : Instantiator(qe, tn), d_tried_assertion_inst(false) +{ + // get the global inverter utility + // this must be global since we need to: + // * process Skolem functions properly across multiple variables within the + // same quantifier + // * cache Skolem variables uniformly across multiple quantified formulas + d_inverter = qe->getBvInverter(); +} + +BvInstantiator::~BvInstantiator() {} +void BvInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_inst_id_counter = 0; + d_var_to_inst_id.clear(); + d_inst_id_to_term.clear(); + d_inst_id_to_alit.clear(); + d_var_to_curr_inst_id.clear(); + d_alit_to_model_slack.clear(); + d_tried_assertion_inst = false; +} + +void BvInstantiator::processLiteral(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + Assert(d_inverter != NULL); + // find path to pv + std::vector path; + Node sv = d_inverter->getSolveVariable(pv.getType()); + Node pvs = ci->getModelValue(pv); + Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl; + Node slit = + d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl()); + if (!slit.isNull()) + { + CegInstantiatorBvInverterQuery m(ci); + unsigned iid = d_inst_id_counter; + Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl; + Node inst = d_inverter->solveBvLit(sv, slit, path, &m); + if (!inst.isNull()) + { + inst = Rewriter::rewrite(inst); + if (inst.isConst() || !ci->hasNestedQuantification()) + { + Trace("cegqi-bv") << "...solved form is " << inst << std::endl; + // store information for id and increment + d_var_to_inst_id[pv].push_back(iid); + d_inst_id_to_term[iid] = inst; + d_inst_id_to_alit[iid] = alit; + d_inst_id_counter++; + } + } + else + { + Trace("cegqi-bv") << "...failed to solve." << std::endl; + } + } + else + { + Trace("cegqi-bv") << "...no path." << std::endl; + } +} + +bool BvInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return true; +} + +Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) +{ + if (effort == CEG_INST_EFFORT_FULL) + { + // always use model values at full effort + return Node::null(); + } + Node atom = lit.getKind() == NOT ? lit[0] : lit; + bool pol = lit.getKind() != NOT; + Kind k = atom.getKind(); + if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT) + { + // others are unhandled + return Node::null(); + } + else if (!atom[0].getType().isBitVector()) + { + return Node::null(); + } + else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP + || (pol && k == EQUAL)) + { + return lit; + } + NodeManager* nm = NodeManager::currentNM(); + Node s = atom[0]; + Node t = atom[1]; + + Node sm = ci->getModelValue(s); + Node tm = ci->getModelValue(t); + Assert(!sm.isNull() && sm.isConst()); + Assert(!tm.isNull() && tm.isConst()); + Trace("cegqi-bv") << "Model value: " << std::endl; + Trace("cegqi-bv") << " " << s << " " << k << " " << t << " is " + << std::endl; + Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; + + Node ret; + if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) + { + // if using slack, we convert constraints to a positive equality based on + // the current model M, e.g.: + // (not) s ~ t ---> s = t + ( s^M - t^M ) + if (sm != tm) + { + Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); + Assert(slack.isConst()); + // remember the slack value for the asserted literal + d_alit_to_model_slack[lit] = slack; + ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack)); + Trace("cegqi-bv") << "Slack is " << slack << std::endl; + } + else + { + ret = s.eqNode(t); + } + } + else + { + // turn disequality into an inequality + // e.g. s != t becomes s < t or t < s + if (k == EQUAL) + { + if (Random::getRandom().pickWithProb(0.5)) + { + std::swap(s, t); + } + pol = true; + } + // otherwise, we optimistically solve for the boundary point of an + // inequality, for example: + // for s < t, we solve s+1 = t + // for ~( s < t ), we solve s = t + // notice that this equality does not necessarily hold in the model, and + // hence the corresponding instantiation strategy is not guaranteed to be + // monotonic. + if (!pol) + { + ret = s.eqNode(t); + } + else + { + Node bv_one = bv::utils::mkOne(bv::utils::getSize(s)); + ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t); + } + } + Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; + return ret; +} + +bool BvInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + // if option enabled, use approach for word-level inversion for BV + // instantiation + if (options::cbqiBv()) + { + // get the best rewritten form of lit for solving for pv + // this should remove instances of non-invertible operators, and + // "linearize" lit with respect to pv as much as possible + Node rlit = rewriteAssertionForSolvePv(ci, pv, lit); + if (Trace.isOn("cegqi-bv")) + { + Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv + << " in " << lit << std::endl; + if (lit != rlit) + { + Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl; + } + } + if (!rlit.isNull()) + { + processLiteral(ci, sf, pv, rlit, alit, effort); + } + } + return false; +} + +bool BvInstantiator::useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return !d_tried_assertion_inst + && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort()); +} + +bool BvInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + std::unordered_map, NodeHashFunction>::iterator + iti = d_var_to_inst_id.find(pv); + if (iti == d_var_to_inst_id.end()) + { + // no bounds + return false; + } + Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv + << std::endl; + // if interleaving, do not do inversion half the time + if (options::cbqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5)) + { + Trace("cegqi-bv") << "...do not do instantiation for " << pv + << " (skip, based on heuristic)" << std::endl; + } + bool firstVar = sf.empty(); + // get inst id list + if (Trace.isOn("cegqi-bv")) + { + Trace("cegqi-bv") << " " << iti->second.size() + << " candidate instantiations for " << pv << " : " + << std::endl; + if (firstVar) + { + Trace("cegqi-bv") << " ...this is the first variable" << std::endl; + } + } + // until we have a model-preserving selection function for BV, this must + // be heuristic (we only pick one literal) + // hence we randomize the list + // this helps robustness, since picking the same literal every time may + // lead to a stream of value instantiations, whereas with randomization + // we may find an invertible literal that leads to a useful instantiation. + std::random_shuffle(iti->second.begin(), iti->second.end()); + + if (Trace.isOn("cegqi-bv")) + { + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; + Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); + Node inst_term = d_inst_id_to_term[inst_id]; + Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); + Node alit = d_inst_id_to_alit[inst_id]; + + // get the slack value introduced for the asserted literal + Node curr_slack_val; + std::unordered_map::iterator itms = + d_alit_to_model_slack.find(alit); + if (itms != d_alit_to_model_slack.end()) + { + curr_slack_val = itms->second; + } + + // debug printing + Trace("cegqi-bv") << " [" << j << "] : "; + Trace("cegqi-bv") << inst_term << std::endl; + if (!curr_slack_val.isNull()) + { + Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val + << std::endl; + } + Trace("cegqi-bv-debug") << " ...from : " << alit << std::endl; + Trace("cegqi-bv") << std::endl; + } + } + + // Now, try all instantiation ids we want to try + // Typically we try only one, otherwise worst-case performance + // for constructing instantiations is exponential on the number of + // variables in this quantifier prefix. + bool ret = false; + bool tryMultipleInst = firstVar && options::cbqiMultiInst(); + bool revertOnSuccess = tryMultipleInst; + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; + Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); + Node inst_term = d_inst_id_to_term[inst_id]; + Node alit = d_inst_id_to_alit[inst_id]; + // try instantiation pv -> inst_term + TermProperties pv_prop_bv; + Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; + d_var_to_curr_inst_id[pv] = inst_id; + d_tried_assertion_inst = true; + ci->markSolved(alit); + if (ci->constructInstantiationInc( + pv, inst_term, pv_prop_bv, sf, revertOnSuccess)) + { + ret = true; + } + ci->markSolved(alit, false); + // we are done unless we try multiple instances + if (!tryMultipleInst) + { + break; + } + } + if (ret) + { + return true; + } + Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl; + d_var_to_curr_inst_id.erase(pv); + + return false; +} + +Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, + Node pv, + Node lit) +{ + // result of rewriting the visited term + std::stack > visited; + visited.push(std::unordered_map()); + // whether the visited term contains pv + std::unordered_map visited_contains_pv; + std::unordered_map::iterator it; + std::unordered_map curr_subs; + std::stack > visit; + TNode cur; + visit.push(std::stack()); + visit.top().push(lit); + do + { + cur = visit.top().top(); + visit.top().pop(); + it = visited.top().find(cur); + + if (it == visited.top().end()) + { + std::unordered_map::iterator itc = + curr_subs.find(cur); + if (itc != curr_subs.end()) + { + visited.top()[cur] = itc->second; + } + else + { + if (cur.getKind() == CHOICE) + { + // must replace variables of choice functions + // with new variables to avoid variable + // capture when considering substitutions + // with multiple literals. + Node bv = ci->getBoundVariable(cur[0][0].getType()); + // should not have captured variables + Assert(curr_subs.find(cur[0][0]) == curr_subs.end()); + curr_subs[cur[0][0]] = bv; + // we cannot cache the results of subterms + // of this choice expression since we are + // now in the context { cur[0][0] -> bv }, + // hence we push a context here + visited.push(std::unordered_map()); + visit.push(std::stack()); + } + visited.top()[cur] = Node::null(); + visit.top().push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.top().push(cur[i]); + } + } + } + else if (it->second.isNull()) + { + Node ret; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + bool contains_pv = (cur == pv); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + it = visited.top().find(cur[i]); + Assert(it != visited.top().end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur[i] != it->second; + children.push_back(it->second); + contains_pv = contains_pv || visited_contains_pv[cur[i]]; + } + // careful that rewrites above do not affect whether this term contains pv + visited_contains_pv[cur] = contains_pv; + + // rewrite the term + ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv); + + // return original if the above function does not produce a result + if (ret.isNull()) + { + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); + } + else + { + ret = cur; + } + } + + /* We need to update contains_pv also for rewritten nodes, since + * the normalizePv* functions rely on the information if pv occurs in a + * rewritten node or not. */ + if (ret != cur) + { + contains_pv = (ret == pv); + for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i) + { + contains_pv = contains_pv || visited_contains_pv[ret[i]]; + } + visited_contains_pv[ret] = contains_pv; + } + + // if was choice, pop context + if (cur.getKind() == CHOICE) + { + Assert(curr_subs.find(cur[0][0]) != curr_subs.end()); + curr_subs.erase(cur[0][0]); + visited.pop(); + visit.pop(); + Assert(visited.size() == visit.size()); + Assert(!visit.empty()); + } + + visited.top()[cur] = ret; + } + } while (!visit.top().empty()); + Assert(visited.size() == 1); + Assert(visited.top().find(lit) != visited.top().end()); + Assert(!visited.top().find(lit)->second.isNull()); + + Node result = visited.top()[lit]; + + if (Trace.isOn("cegqi-bv-nl")) + { + std::vector trace_visit; + std::unordered_set trace_visited; + + trace_visit.push_back(result); + do + { + cur = trace_visit.back(); + trace_visit.pop_back(); + + if (trace_visited.find(cur) == trace_visited.end()) + { + trace_visited.insert(cur); + trace_visit.insert(trace_visit.end(), cur.begin(), cur.end()); + } + else if (cur == pv) + { + Trace("cegqi-bv-nl") + << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl; + } + } while (!trace_visit.empty()); + } + + return result; +} + +/** + * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, + * or -pv * t. Extracting the coefficient of multiplications only succeeds if + * the multiplication are normalized with normalizePvMult. + * + * If sucessful it returns + * 1 if n == pv, + * -1 if n == -pv, + * t if n == pv * t, + * -t if n == -pv * t. + * If n is not a linear term, a null node is returned. + */ +static Node getPvCoeff(TNode pv, TNode n) +{ + bool neg = false; + Node coeff; + + if (n.getKind() == BITVECTOR_NEG) + { + neg = true; + n = n[0]; + } + + if (n == pv) + { + coeff = bv::utils::mkOne(bv::utils::getSize(pv)); + } + /* All multiplications are normalized to pv * (t1 * t2). */ + else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) + { + Assert(n.getNumChildren() == 2); + Assert(n[0] == pv); + coeff = n[1]; + } + else /* n is in no form to extract the coefficient for pv */ + { + Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " + << n << std::endl; + return Node::null(); + } + Assert(!coeff.isNull()); + + if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); + return coeff; +} + +/** + * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * -pv * b * c + * + * is rewritten to + * + * pv * -(a * b * c) + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns a + * multiplication over children. + */ +static Node normalizePvMult( + TNode pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + bool neg, neg_coeff = false; + bool found_pv = false; + NodeManager* nm; + NodeBuilder<> nb(BITVECTOR_MULT); + BvLinearAttribute is_linear; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (!found_pv && nc == pv) + { + found_pv = true; + neg_coeff = neg; + continue; + } + else if (!found_pv && nc.getKind() == BITVECTOR_MULT + && nc.getAttribute(is_linear)) + { + Assert(nc.getNumChildren() == 2); + Assert(nc[0] == pv); + Assert(!contains_pv[nc[1]]); + found_pv = true; + neg_coeff = neg; + nb << nc[1]; + continue; + } + return Node::null(); /* non-linear */ + } + Assert(nb.getNumChildren() > 0); + + Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); + if (neg_coeff) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + coeff = Rewriter::rewrite(coeff); + unsigned size_coeff = bv::utils::getSize(coeff); + Node zero = bv::utils::mkZero(size_coeff); + if (coeff == zero) + { + return zero; + } + Node result; + if (found_pv) + { + if (coeff == bv::utils::mkOne(size_coeff)) + { + return pv; + } + result = nm->mkNode(BITVECTOR_MULT, pv, coeff); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + else + { + result = coeff; + } + return result; +} + +#ifdef CVC4_ASSERTIONS +static bool isLinearPlus( + TNode n, + TNode pv, + std::unordered_map& contains_pv) +{ + Node coeff; + Assert(n.getAttribute(BvLinearAttribute())); + Assert(n.getNumChildren() == 2); + if (n[0] != pv) + { + Assert(n[0].getKind() == BITVECTOR_MULT); + Assert(n[0].getNumChildren() == 2); + Assert(n[0][0] == pv); + Assert(!contains_pv[n[0][1]]); + } + Assert(!contains_pv[n[1]]); + coeff = getPvCoeff(pv, n[0]); + Assert(!coeff.isNull()); + Assert(!contains_pv[coeff]); + return true; +} +#endif + +/** + * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * pv + b + c * -pv + * + * is rewritten to + * + * pv * (a - c) + b + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns an + * addition over children. + */ +static Node normalizePvPlus( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + NodeManager* nm; + NodeBuilder<> nb_c(BITVECTOR_PLUS); + NodeBuilder<> nb_l(BITVECTOR_PLUS); + BvLinearAttribute is_linear; + bool neg; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb_l << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (nc == pv + || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) + { + Node coeff = getPvCoeff(pv, nc); + Assert(!coeff.isNull()); + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + nb_c << coeff; + continue; + } + else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) + { + Assert(isLinearPlus(nc, pv, contains_pv)); + Node coeff = getPvCoeff(pv, nc[0]); + Assert(!coeff.isNull()); + Node leaf = nc[1]; + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + leaf = nm->mkNode(BITVECTOR_NEG, leaf); + } + nb_c << coeff; + nb_l << leaf; + continue; + } + /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ + return Node::null(); + } + Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); + + Node pv_mult_coeffs, result; + if (nb_c.getNumChildren() > 0) + { + Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); + coeffs = Rewriter::rewrite(coeffs); + result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv); + } + + if (nb_l.getNumChildren() > 0) + { + Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); + leafs = Rewriter::rewrite(leafs); + Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); + /* pv * 0 + t --> t */ + if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) + { + result = leafs; + } + else + { + result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + } + Assert(!result.isNull()); + return result; +} + +/** + * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv + * marks terms in which pv occurs. + * For example, equality + * + * -pv * a + b = c + pv + * + * rewrites to + * + * pv * (-a - 1) = c - b. + */ +static Node normalizePvEqual( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + Assert(children.size() == 2); + + NodeManager* nm = NodeManager::currentNM(); + BvLinearAttribute is_linear; + Node coeffs[2], leafs[2]; + bool neg; + TNode child; + + for (unsigned i = 0; i < 2; ++i) + { + child = children[i]; + neg = false; + if (child.getKind() == BITVECTOR_NEG) + { + neg = true; + child = child[0]; + } + if (child.getAttribute(is_linear) || child == pv) + { + if (child.getKind() == BITVECTOR_PLUS) + { + Assert(isLinearPlus(child, pv, contains_pv)); + coeffs[i] = getPvCoeff(pv, child[0]); + leafs[i] = child[1]; + } + else + { + Assert(child.getKind() == BITVECTOR_MULT || child == pv); + coeffs[i] = getPvCoeff(pv, child); + } + } + if (neg) + { + if (!coeffs[i].isNull()) + { + coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); + } + if (!leafs[i].isNull()) + { + leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); + } + } + } + + if (coeffs[0].isNull() || coeffs[1].isNull()) + { + return Node::null(); + } + + Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); + coeff = Rewriter::rewrite(coeff); + std::vector mult_children = {pv, coeff}; + Node lhs = normalizePvMult(pv, mult_children, contains_pv); + + Node rhs; + if (!leafs[0].isNull() && !leafs[1].isNull()) + { + rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); + } + else if (!leafs[0].isNull()) + { + rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); + } + else if (!leafs[1].isNull()) + { + rhs = leafs[1]; + } + else + { + rhs = bv::utils::mkZero(bv::utils::getSize(pv)); + } + rhs = Rewriter::rewrite(rhs); + + if (lhs == rhs) + { + return bv::utils::mkTrue(); + } + + Node result = lhs.eqNode(rhs); + contains_pv[result] = true; + return result; +} + +Node BvInstantiator::rewriteTermForSolvePv( + Node pv, + Node n, + std::vector& children, + std::unordered_map& contains_pv) +{ + NodeManager* nm = NodeManager::currentNM(); + + // [1] rewrite cases of non-invertible operators + + if (n.getKind() == EQUAL) + { + TNode lhs = children[0]; + TNode rhs = children[1]; + + /* rewrite: x * x = x -> x < 2 */ + if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv + && rhs[1] == pv) + || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv + && lhs[1] == pv)) + { + return nm->mkNode( + BITVECTOR_ULT, + pv, + bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); + } + + if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) + { + Node result = normalizePvEqual(pv, children, contains_pv); + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + return result; + } + } + else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) + { + if (options::cbqiBvLinearize() && contains_pv[n]) + { + Node result; + if (n.getKind() == BITVECTOR_MULT) + { + result = normalizePvMult(pv, children, contains_pv); + } + else + { + result = normalizePvPlus(pv, children, contains_pv); + } + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + return result; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + } + } + + // [2] try to rewrite non-linear literals -> linear literals + + return Node::null(); +} + +/** sort bv extract interval + * + * This sorts lists of bitvector extract terms where + * ((_ extract i1 i2) t) < ((_ extract j1 j2) t) + * if i1>j1 or i1=j1 and i2>j2. + */ +struct SortBvExtractInterval +{ + bool operator()(Node i, Node j) + { + Assert(i.getKind() == BITVECTOR_EXTRACT); + Assert(j.getKind() == BITVECTOR_EXTRACT); + BitVectorExtract ie = i.getOperator().getConst(); + BitVectorExtract je = j.getOperator().getConst(); + if (ie.high > je.high) + { + return true; + } + else if (ie.high == je.high) + { + Assert(ie.low != je.low); + return ie.low > je.low; + } + return false; + } +}; + +void BvInstantiatorPreprocess::registerCounterexampleLemma( + std::vector& lems, std::vector& ce_vars) +{ + // new variables + std::vector vars; + // new lemmas + std::vector new_lems; + + if (options::cbqiBvRmExtract()) + { + NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; + // map from terms to bitvector extracts applied to that term + std::map > extract_map; + std::unordered_set visited; + for (unsigned i = 0, size = lems.size(); i < size; i++) + { + Trace("cegqi-bv-pp-debug2") + << "Register ce lemma # " << i << " : " << lems[i] << std::endl; + collectExtracts(lems[i], extract_map, visited); + } + for (std::pair >& es : extract_map) + { + // sort based on the extract start position + std::vector& curr_vec = es.second; + + SortBvExtractInterval sbei; + std::sort(curr_vec.begin(), curr_vec.end(), sbei); + + unsigned width = es.first.getType().getBitVectorSize(); + + // list of points b such that: + // b>0 and we must start a segment at (b-1) or b==0 + std::vector boundaries; + boundaries.push_back(width); + boundaries.push_back(0); + + Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl; + for (unsigned i = 0, size = curr_vec.size(); i < size; i++) + { + Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i] << std::endl; + BitVectorExtract e = + curr_vec[i].getOperator().getConst(); + if (std::find(boundaries.begin(), boundaries.end(), e.high + 1) + == boundaries.end()) + { + boundaries.push_back(e.high + 1); + } + if (std::find(boundaries.begin(), boundaries.end(), e.low) + == boundaries.end()) + { + boundaries.push_back(e.low); + } + } + std::sort(boundaries.rbegin(), boundaries.rend()); + + // make the extract variables + std::vector children; + for (unsigned i = 1; i < boundaries.size(); i++) + { + Assert(boundaries[i - 1] > 0); + Node ex = bv::utils::mkExtract( + es.first, boundaries[i - 1] - 1, boundaries[i]); + Node var = + nm->mkSkolem("ek", + ex.getType(), + "variable to represent disjoint extract region"); + children.push_back(var); + vars.push_back(var); + } + + Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children); + Assert(conc.getType() == es.first.getType()); + Node eq_lem = conc.eqNode(es.first); + Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl; + new_lems.push_back(eq_lem); + Trace("cegqi-bv-pp") << "...finished processing extracts for term " + << es.first << std::endl; + } + Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl; + } + + if (!vars.empty()) + { + // could try applying subs -> vars here + // in practice, this led to worse performance + + Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..." + << std::endl; + lems.insert(lems.end(), new_lems.begin(), new_lems.end()); + Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..." + << std::endl; + ce_vars.insert(ce_vars.end(), vars.begin(), vars.end()); + } +} + +void BvInstantiatorPreprocess::collectExtracts( + Node lem, + std::map >& extract_map, + std::unordered_set& visited) +{ + std::vector visit; + TNode cur; + visit.push_back(lem); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() != FORALL) + { + if (cur.getKind() == BITVECTOR_EXTRACT) + { + if (cur[0].getKind() == INST_CONSTANT) + { + extract_map[cur[0]].push_back(cur); + } + } + + for (const Node& nc : cur) + { + visit.push_back(nc); + } + } + } + } while (!visit.empty()); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h new file mode 100644 index 000000000..439309e91 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -0,0 +1,216 @@ +/********************* */ +/*! \file ceg_bv_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ceg_bv_instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H + +#include +#include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Bitvector instantiator + * + * This implements an approach for counterexample-guided instantiation + * for bit-vector variables based on word-level inversions. For details, + * see Niemetz et al, "Solving Quantified Bit-Vectors Using Invertibility + * Conditions", CAV 2018. It is enabled by --cbqi-bv. + * + * This class contains all necessary information for instantiating a single + * bit-vector variable of a single quantified formula. + */ +class BvInstantiator : public Instantiator +{ + public: + BvInstantiator(QuantifiersEngine* qe, TypeNode tn); + ~BvInstantiator() override; + /** reset */ + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** this instantiator processes assertions */ + bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** this instantiator processes bit-vector equalities and inequalities + * + * Based on the configuration --cbqi-bv-ineq, it may modify the form of lit + * based on a projection. For lit (not) s <> t, this may be one of: + * - eq-slack: s = t + ( s^M - t^M ) + * - eq-boundary: s = t + ( s^M > t^M ? 1 : -1 ) + * - keep: (not) s <> t, i.e. unchanged. + * Additionally for eq-boundary, inequalities s != t become s < t or t < s. + * This is the method project_* from Figure 3 of Niemetz et al, CAV 2018. + */ + Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) override; + /** process assertion + * + * Computes a solved form for pv in lit based on Figure 1 of Niemetz et al, + * CAV 2018. + */ + bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) override; + /** process assertions + * + * This is called after processAssertion has been called on all currently + * asserted literals that involve pv. This chooses the best solved form for pv + * based on heuristics. Currently, by default, we choose a random solved form. + * We may try multiple or zero bounds based on the options + * --cbqi-multi-inst and --cbqi-bv-interleave-value. + */ + bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** use model value + * + * We allow model values if we have not already tried an assertion, + * and only at levels below full if cbqiFullEffort is false. + */ + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** identify */ + std::string identify() const override { return "Bv"; } + + private: + /** pointer to the bv inverter class */ + BvInverter* d_inverter; + //--------------------------------solved forms + /** identifier counter, used to allocate ids to each solve form */ + unsigned d_inst_id_counter; + /** map from variables to list of solved form ids */ + std::unordered_map, NodeHashFunction> + d_var_to_inst_id; + /** for each solved form id, the term for instantiation */ + std::unordered_map d_inst_id_to_term; + /** for each solved form id, the corresponding asserted literal */ + std::unordered_map d_inst_id_to_alit; + /** map from variable to current id we are processing */ + std::unordered_map d_var_to_curr_inst_id; + /** the amount of slack we added for asserted literals */ + std::unordered_map d_alit_to_model_slack; + //--------------------------------end solved forms + /** whether we have tried an instantiation based on assertion in this round */ + bool d_tried_assertion_inst; + /** rewrite assertion for solve pv + * + * Returns a literal that is equivalent to lit that leads to best solved form + * for pv. + */ + Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit); + /** rewrite term for solve pv + * + * This is a helper function for rewriteAssertionForSolvePv. + * If this returns non-null value ret, then this indicates + * that n should be rewritten to ret. It is called as + * a "post-rewrite", that is, after the children of n + * have been rewritten and stored in the vector children. + * + * contains_pv stores whether certain nodes contain pv. + * where we guarantee that all subterms of terms in children + * appear in the domain of contains_pv. + */ + Node rewriteTermForSolvePv( + Node pv, + Node n, + std::vector& children, + std::unordered_map& contains_pv); + /** process literal, called from processAssertion + * + * lit is the literal to solve for pv that has been rewritten according to + * internal rules here. + * alit is the asserted literal that lit is derived from. + */ + void processLiteral(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort); +}; + +/** Bitvector instantiator preprocess + * + * This class implements preprocess techniques that are helpful for + * counterexample-guided instantiation, such as introducing variables + * that refer to disjoint bit-vector extracts. + */ +class BvInstantiatorPreprocess : public InstantiatorPreprocess +{ + public: + BvInstantiatorPreprocess() {} + ~BvInstantiatorPreprocess() override {} + /** register counterexample lemma + * + * This method modifies the contents of lems based on the extract terms + * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces + * a dummy equality so that segments of terms t under extracts can be solved + * independently. + * + * For example: + * P[ ((extract 7 4) t), ((extract 3 0) t)] + * becomes: + * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * t = concat( x74, x30 ) + * where x74 and x30 are fresh variables of type BV_4. + * + * Another example: + * P[ ((extract 7 3) t), ((extract 4 0) t)] + * becomes: + * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * t = concat( x75, x44, x30 ) + * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4 + * respectively. + * + * Notice we leave the original conjecture alone. This is done for performance + * since the added equalities ensure we are able to construct the proper + * solved forms for variables in t and for the intermediate variables above. + */ + void registerCounterexampleLemma(std::vector& lems, + std::vector& ce_vars) override; + + private: + /** collect extracts + * + * This method collects all extract terms in lem + * and stores them in d_extract_map. + * visited is the terms we've already visited. + */ + void collectExtracts(Node lem, + std::map >& extract_map, + std::unordered_set& visited); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp new file mode 100644 index 000000000..54dc78442 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -0,0 +1,175 @@ +/********************* */ +/*! \file ceg_dt_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of ceg_dt_instantiator + **/ + +#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void DtInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ +} + +bool DtInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + CegInstEffort effort) +{ + Trace("cegqi-dt-debug") << "try based on constructors in equivalence class." + << std::endl; + // look in equivalence class for a constructor + NodeManager* nm = NodeManager::currentNM(); + for (unsigned k = 0, size = eqc.size(); k < size; k++) + { + Node n = eqc[k]; + if (n.getKind() == APPLY_CONSTRUCTOR) + { + Trace("cegqi-dt-debug") + << "...try based on constructor term " << n << std::endl; + std::vector children; + children.push_back(n.getOperator()); + const Datatype& dt = + static_cast(d_type.toType()).getDatatype(); + unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + // now must solve for selectors applied to pv + for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++) + { + Node c = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)), + pv); + ci->pushStackVariable(c); + children.push_back(c); + } + Node val = nm->mkNode(kind::APPLY_CONSTRUCTOR, children); + TermProperties pv_prop_dt; + if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf)) + { + return true; + } + // cleanup + for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++) + { + ci->popStackVariable(); + } + break; + } + } + return false; +} + +bool DtInstantiator::hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return true; +} + +bool DtInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + CegInstEffort effort) +{ + Node val = solve_dt(pv, terms[0], terms[1], terms[0], terms[1]); + if (!val.isNull()) + { + TermProperties pv_prop; + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { + return true; + } + } + return false; +} + +Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) +{ + Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b + << " " << sa << " " << sb << std::endl; + Node ret; + if (!a.isNull() && a == v) + { + ret = sb; + } + else if (!b.isNull() && b == v) + { + ret = sa; + } + else if (!a.isNull() && a.getKind() == APPLY_CONSTRUCTOR) + { + if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR) + { + if (a.getOperator() == b.getOperator()) + { + for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) + { + Node s = solve_dt(v, a[i], b[i], sa[i], sb[i]); + if (!s.isNull()) + { + return s; + } + } + } + } + else + { + NodeManager* nm = NodeManager::currentNM(); + unsigned cindex = Datatype::indexOf(a.getOperator().toExpr()); + TypeNode tn = a.getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) + { + Node nn = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), + sb); + Node s = solve_dt(v, a[i], Node::null(), sa[i], nn); + if (!s.isNull()) + { + return s; + } + } + } + } + else if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR) + { + // flip sides + return solve_dt(v, b, a, sb, sa); + } + if (!ret.isNull()) + { + // ensure does not contain v + if (ret.hasSubterm(v)) + { + ret = Node::null(); + } + } + return ret; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h new file mode 100644 index 000000000..37a81b625 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -0,0 +1,91 @@ +/********************* */ +/*! \file ceg_dt_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ceg_dt_instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H + +#include "expr/node.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Datatypes Instantiator + * + * This class implements a selection function for datatypes based on solving + * for occurrences of variables in subfields of datatypes. + */ +class DtInstantiator : public Instantiator +{ + public: + DtInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {} + virtual ~DtInstantiator() {} + /** reset */ + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** process equal terms + * + * This tries to find an equality eqc[i] = eqc[j] such that pv can be solved + * for (via solve_dt). If a solved form for pv can be found in this way, we + * add the substitution for pv to sf and recurse. + */ + bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + CegInstEffort effort) override; + /** this instantiator processes equalities */ + bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** process equality + * + * This tries to find a solved form for pv based on the equality + * terms[0] = terms[1] via solve_dt. If a solved form for pv can be found in + * this way, we add the substitution for pv to sf and recurse. + */ + bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& term_props, + std::vector& terms, + CegInstEffort effort) override; + /** identify */ + std::string identify() const override { return "Dt"; } + + private: + /** solve datatype + * + * If this method returns a non-null node ret, then v -> ret is a + * solution for v in the equality a = b and ret does not contain v. + * + * For example, if cons( v, nil ) = cons( 5, nil ), this method returns 5. + * For example, if cons( v, nil ) = L, this method returns head( L ). + * For example, if cons( v, nil ) = cons( v+1, nil ), this method returns + * the null node. + */ + Node solve_dt(Node v, Node a, Node b, Node sa, Node sb); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp new file mode 100644 index 000000000..7acdab00f --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -0,0 +1,170 @@ +/********************* */ +/*! \file ceg_epr_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of ceg_epr_instantiator + **/ + +#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void EprInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_equal_terms.clear(); +} + +bool EprInstantiator::processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) +{ + if (options::quantEprMatching()) + { + Assert(pv_prop.isBasic()); + d_equal_terms.push_back(n); + return false; + } + pv_prop.d_type = 0; + return ci->constructInstantiationInc(pv, n, pv_prop, sf); +} + +struct sortEqTermsMatch +{ + std::map d_match_score; + bool operator()(Node i, Node j) + { + int match_score_i = d_match_score[i]; + int match_score_j = d_match_score[j]; + return match_score_i > match_score_j + || (match_score_i == match_score_j && i < j); + } +}; + +bool EprInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + CegInstEffort effort) +{ + if (!options::quantEprMatching()) + { + return false; + } + // heuristic for best matching constant + sortEqTermsMatch setm; + for (unsigned i = 0; i < ci->getNumCEAtoms(); i++) + { + Node catom = ci->getCEAtom(i); + computeMatchScore(ci, pv, catom, catom, setm.d_match_score); + } + // sort by match score + std::sort(d_equal_terms.begin(), d_equal_terms.end(), setm); + TermProperties pv_prop; + pv_prop.d_type = 0; + for (unsigned i = 0, size = d_equal_terms.size(); i < size; i++) + { + if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf)) + { + return true; + } + } + return false; +} + +void EprInstantiator::computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + std::vector& arg_reps, + TermArgTrie* tat, + unsigned index, + std::map& match_score) +{ + if (index == catom.getNumChildren()) + { + Assert(tat->hasNodeData()); + Node gcatom = tat->getNodeData(); + Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom + << std::endl; + for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++) + { + if (catom[i] == pv) + { + Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl; + match_score[gcatom[i]]++; + } + else + { + // recursive matching + computeMatchScore(ci, pv, catom[i], gcatom[i], match_score); + } + } + return; + } + std::map::iterator it = tat->d_data.find(arg_reps[index]); + if (it != tat->d_data.end()) + { + computeMatchScore( + ci, pv, catom, arg_reps, &it->second, index + 1, match_score); + } +} + +void EprInstantiator::computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + Node eqc, + std::map& match_score) +{ + if (!inst::Trigger::isAtomicTrigger(catom) || !catom.hasSubterm(pv)) + { + return; + } + Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; + eq::EqualityEngine* ee = + ci->getQuantifiersEngine()->getMasterEqualityEngine(); + std::vector arg_reps; + for (unsigned j = 0, nchild = catom.getNumChildren(); j < nchild; j++) + { + arg_reps.push_back(ee->getRepresentative(catom[j])); + } + if (!ee->hasTerm(eqc)) + { + return; + } + TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase(); + Node rep = ee->getRepresentative(eqc); + Node op = tdb->getMatchOperator(catom); + TermArgTrie* tat = tdb->getTermArgTrie(rep, op); + Trace("cegqi-epr") << "EPR instantiation match term : " << catom + << ", check ground terms=" << (tat != NULL) << std::endl; + if (tat) + { + computeMatchScore(ci, pv, catom, arg_reps, tat, 0, match_score); + } +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h new file mode 100644 index 000000000..cfc937bbd --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -0,0 +1,105 @@ +/********************* */ +/*! \file ceg_epr_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ceg_epr_instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H + +#include +#include +#include "theory/quantifiers/cegqi/ceg_instantiator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class TermArgTrie; + +/** Effectively Propositional (EPR) Instantiator + * + * This implements a selection function for the EPR fragment. + */ +class EprInstantiator : public Instantiator +{ + public: + EprInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {} + virtual ~EprInstantiator() {} + /** reset */ + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** process equal terms + * + * This adds n to the set of equal terms d_equal_terms if matching heuristics + * are enabled (--quant-epr-match), or simply tries the substitution pv -> n + * otherwise. + */ + bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) override; + /** process equal terms + * + * Called when pv is equal to the set eqc. If matching heuristics are enabled, + * this adds the substitution pv -> n based on the best term n in eqc. + */ + bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector& eqc, + CegInstEffort effort) override; + /** identify */ + std::string identify() const override { return "Epr"; } + + private: + /** + * The current set of terms that are equal to the variable-to-instantate of + * this class. + */ + std::vector d_equal_terms; + /** compute match score + * + * This method computes the map match_score, from ground term t to the + * number of times that occur in simple matches for a quantified formula. + * For example, for quantified formula forall xy. P( x ) V Q( x, y ) and + * ground terms { P( a ), Q( a, a ), Q( b, c ), Q( a, c ) }, we compute for x: + * match_score[a] = 3, + * match_score[b] = 1, + * match_score[c] = 0. + * The higher the match score for a term, the more likely this class is to use + * t in instantiations. + */ + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + std::vector& arg_reps, + TermArgTrie* tat, + unsigned index, + std::map& match_score); + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + Node eqc, + std::map& match_score); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 102a6327b..af003ce39 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -13,7 +13,11 @@ **/ #include "theory/quantifiers/cegqi/ceg_instantiator.h" -#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" + +#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp deleted file mode 100644 index a54382130..000000000 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ /dev/null @@ -1,2006 +0,0 @@ -/********************* */ -/*! \file ceg_t_instantiator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation - **/ - -#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" - -#include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/ematching/trigger.h" - -#include "theory/arith/arith_msum.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" -#include "theory/bv/theory_bv_utils.h" -#include "util/bitvector.h" -#include "util/random.h" - -#include -#include - -using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -struct BvLinearAttributeId {}; -using BvLinearAttribute = expr::Attribute; - -Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { - Node val = t; - Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; - Assert( !e.getType().isInteger() || t.getType().isInteger() ); - Assert( !e.getType().isInteger() || mt.getType().isInteger() ); - //add rho value - //get the value of c*e - Node ceValue = me; - Node new_theta = theta; - if( !c.isNull() ){ - Assert( c.getType().isInteger() ); - ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); - ceValue = Rewriter::rewrite( ceValue ); - if( new_theta.isNull() ){ - new_theta = c; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); - new_theta = Rewriter::rewrite( new_theta ); - } - Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; - } - if( !new_theta.isNull() && e.getType().isInteger() ){ - Node rho; - //if( !mt.getType().isInteger() ){ - //round up/down - //mt = NodeManager::currentNM()->mkNode( - //} - if( isLower ){ - rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); - }else{ - rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); - } - rho = Rewriter::rewrite( rho ); - Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = "; - rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); - rho = Rewriter::rewrite( rho ); - Trace("cegqi-arith-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; - val = NodeManager::currentNM()->mkNode( rk, val, rho ); - val = Rewriter::rewrite( val ); - Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; - } - if( !inf_coeff.isNull() ){ - Assert( !d_vts_sym[0].isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); - val = Rewriter::rewrite( val ); - } - if( !delta_coeff.isNull() ){ - //create delta here if necessary - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) ); - val = Rewriter::rewrite( val ); - } - return val; -} - -//this isolates the atom into solved form -// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf -// ensures val is Int if pv is Int, and val does not contain vts symbols -int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { - int ires = 0; - Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl; - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(atom, msum)) - { - Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; - if( Trace.isOn("cegqi-arith-debug") ){ - ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug"); - } - TypeNode pvtn = pv.getType(); - //remove vts symbols from polynomial - Node vts_coeff[2]; - for( unsigned t=0; t<2; t++ ){ - if( !d_vts_sym[t].isNull() ){ - std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); - if( itminf!=msum.end() ){ - vts_coeff[t] = itminf->second; - if( vts_coeff[t].isNull() ){ - vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - } - //negate if coefficient on variable is positive - std::map< Node, Node >::iterator itv = msum.find( pv ); - if( itv!=msum.end() ){ - //multiply by the coefficient we will isolate for - if( itv->second.isNull() ){ - vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); - }else{ - if( !pvtn.isInteger() ){ - vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst() ), vts_coeff[t] ); - vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); - }else if( itv->second.getConst().sgn()==1 ){ - vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); - } - } - } - Trace("cegqi-arith-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; - msum.erase( d_vts_sym[t] ); - } - } - } - - ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); - if( ires!=0 ){ - Node realPart; - if( Trace.isOn("cegqi-arith-debug") ){ - Trace("cegqi-arith-debug") << "Isolate : "; - if( !veq_c.isNull() ){ - Trace("cegqi-arith-debug") << veq_c << " * "; - } - Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl; - } - // when not pure LIA/LRA, we must check whether the lhs contains pv - if (val.hasSubterm(pv)) - { - Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; - return 0; - } - if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ - //redo, split integer/non-integer parts - bool useCoeff = false; - Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst().getNumerator(); - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( it->first.isNull() || it->first.getType().isInteger() ){ - if( !it->second.isNull() ){ - coeff = coeff.lcm( it->second.getConst().getDenominator() ); - useCoeff = true; - } - } - } - //multiply everything by this coefficient - Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); - std::vector< Node > real_part; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( useCoeff ){ - if( it->second.isNull() ){ - msum[it->first] = rcoeff; - }else{ - msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); - } - } - if( !it->first.isNull() && !it->first.getType().isInteger() ){ - real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); - } - } - //remove delta TODO: check this - vts_coeff[1] = Node::null(); - //multiply inf - if( !vts_coeff[0].isNull() ){ - vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); - } - realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); - Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); - //re-isolate - Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; - veq_c = Node::null(); - ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); - Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; - Trace("cegqi-arith-debug") << " real part : " << realPart << std::endl; - if( ires!=0 ){ - int ires_use = ( msum[pv].isNull() || msum[pv].getConst().sgn()==1 ) ? 1 : -1; - val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, - NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), - NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? - Trace("cegqi-arith-debug") << "result : " << val << std::endl; - Assert( val.getType().isInteger() ); - } - } - } - vts_coeff_inf = vts_coeff[0]; - vts_coeff_delta = vts_coeff[1]; - Trace("cegqi-arith-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; - }else{ - Trace("cegqi-arith-debug") << "fail : could not get monomial sum" << std::endl; - } - return ires; -} - -void ArithInstantiator::reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false ); - d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false ); - for( unsigned i=0; i<2; i++ ){ - d_mbp_bounds[i].clear(); - d_mbp_coeff[i].clear(); - for( unsigned j=0; j<2; j++ ){ - d_mbp_vts_coeff[i][j].clear(); - } - d_mbp_lit[i].clear(); - } -} - -bool ArithInstantiator::processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& term_props, - std::vector& terms, - CegInstEffort effort) -{ - Node eq_lhs = terms[0]; - Node eq_rhs = terms[1]; - Node lhs_coeff = term_props[0].d_coeff; - Node rhs_coeff = term_props[1].d_coeff; - //make the same coefficient - if( rhs_coeff!=lhs_coeff ){ - if( !rhs_coeff.isNull() ){ - Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; - eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff.isNull() ){ - Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Node val; - TermProperties pv_prop; - Node vts_coeff_inf; - Node vts_coeff_delta; - //isolate pv in the equality - int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - pv_prop.d_type = 0; - if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) - { - return true; - } - } - - return false; -} - -Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - 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())) { - return lit; - } else { - return Node::null(); - } -} - -bool ArithInstantiator::processAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) -{ - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - //arithmetic inequalities and disequalities - Assert( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ); - // get model value for pv - Node pv_value = ci->getModelValue( pv ); - //cannot contain infinity? - Node vts_coeff_inf; - Node vts_coeff_delta; - Node val; - TermProperties pv_prop; - //isolate pv in the inequality - int ires = solve_arith( ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( d_type.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper; - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff_inf.isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; - Assert( vts_coeff_inf.isConst() ); - is_upper = ( vts_coeff_inf.getConst().sgn()==1 ); - }else{ - Node rhs_value = ci->getModelValue( val ); - Node lhs_value = pv_prop.getModifiedTerm( pv_value ); - if( !pv_prop.isBasic() ){ - lhs_value = pv_prop.getModifiedTerm( pv_value ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - // it generally should be the case that lhs_value!=rhs_value - // however, this assertion is violated e.g. if non-linear is enabled - // since the quantifier-free arithmetic solver may pass full - // effort with no lemmas even when we are not guaranteed to have a - // model. By convention, we use GEQ to compare the values here. - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true ); - } - }else{ - is_upper = (r==0); - } - Assert( atom.getKind()==EQUAL && !pol ); - if( d_type.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( d_type.isReal() ); - uires = is_upper ? -2 : 2; - } - } - if( Trace.isOn("cegqi-arith-bound-inf") ){ - Node pvmod = pv_prop.getModifiedTerm( pv ); - Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : "; - Trace("cegqi-arith-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl; - } - //take into account delta - if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff_delta.isNull() ){ - vts_coeff_delta = delta_coeff; - }else{ - vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); - vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); - } - }else{ - Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); - } - } - if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - unsigned index = uires>0 ? 0 : 1; - d_mbp_bounds[index].push_back( uval ); - d_mbp_coeff[index].push_back( pv_prop.d_coeff ); - Trace("cegqi-arith-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; - for( unsigned t=0; t<2; t++ ){ - d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); - } - d_mbp_lit[index].push_back( lit ); - }else{ - //try this bound - pv_prop.d_type = uires>0 ? 1 : -1; - if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) - { - return true; - } - } - } - } - - - return false; -} - -bool ArithInstantiator::processAssertions(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - if (options::cbqiModel()) { - bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); - bool upper_first = false; - if( options::cbqiMinBounds() ){ - upper_first = d_mbp_bounds[1].size() t_values[3]; - Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero; - Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one; - Node pv_value = ci->getModelValue( pv ); - //try optimal bounds - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - best_used[rr] = -1; - if( d_mbp_bounds[rr].empty() ){ - if( use_inf ){ - Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; - //no bounds, we do +- infinity - Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type ); - //TODO : rho value for infinity? - if( rr==0 ){ - val = NodeManager::currentNM()->mkNode( UMINUS, val ); - val = Rewriter::rewrite( val ); - } - TermProperties pv_prop_no_bound; - if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) - { - return true; - } - } - }else{ - Trace("cegqi-arith-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; - int best = -1; - Node best_bound_value[3]; - for( unsigned j=0; jgetModelValue( d_mbp_bounds[rr][j] ); - t_values[rr][j] = t_value; - value[1] = t_value; - Trace("cegqi-arith-bound") << value[1]; - }else{ - value[2] = d_mbp_vts_coeff[rr][1][j]; - if( !value[2].isNull() ){ - Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; - }else{ - value[2] = zero; - } - } - //multiply by coefficient - if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){ - Assert( d_mbp_coeff[rr][j].isConst() ); - value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst() ), value[t] ); - value[t] = Rewriter::rewrite( value[t] ); - } - //check if new best - if( best!=-1 ){ - Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); - if( value[t]!=best_bound_value[t] ){ - Kind k = rr==0 ? GEQ : LEQ; - Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); - cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){ - new_best = false; - break; - } - } - } - } - Trace("cegqi-arith-bound") << std::endl; - if( new_best ){ - for( unsigned t=0; t<3; t++ ){ - best_bound_value[t] = value[t]; - } - best = j; - } - } - if( best!=-1 ){ - Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; - if( best_bound_value[0]!=zero ){ - Trace("cegqi-arith-bound") << "( " << best_bound_value[0] << " * INF ) + "; - } - Trace("cegqi-arith-bound") << best_bound_value[1]; - if( best_bound_value[2]!=zero ){ - Trace("cegqi-arith-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; - } - Trace("cegqi-arith-bound") << std::endl; - best_used[rr] = best; - //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict - if (!options::cbqiMidpoint() || d_type.isInteger() - || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull())) - { - Node val = d_mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(), - d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); - if( !val.isNull() ){ - TermProperties pv_prop_bound; - pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; - pv_prop_bound.d_type = rr==0 ? 1 : -1; - if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) - { - return true; - } - } - } - } - } - } - //if not using infinity, use model value of zero - if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ - Node val = zero; - TermProperties pv_prop_zero; - Node theta = sf.getTheta(); - val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() ); - if( !val.isNull() ){ - if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) - { - return true; - } - } - } - if( options::cbqiMidpoint() && !d_type.isInteger() ){ - Node vals[2]; - bool bothBounds = true; - Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; - for( unsigned rr=0; rr<2; rr++ ){ - int best = best_used[rr]; - if( best==-1 ){ - bothBounds = false; - }else{ - vals[rr] = d_mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(), - d_mbp_vts_coeff[rr][0][best], Node::null() ); - } - Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; - } - Node val; - if( bothBounds ){ - Assert( !vals[0].isNull() && !vals[1].isNull() ); - if( vals[0]==vals[1] ){ - val = vals[0]; - }else{ - val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), - NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); - val = Rewriter::rewrite( val ); - } - }else{ - if( !vals[0].isNull() ){ - val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one ); - val = Rewriter::rewrite( val ); - }else if( !vals[1].isNull() ){ - val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one ); - val = Rewriter::rewrite( val ); - } - } - Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; - if( !val.isNull() ){ - TermProperties pv_prop_midpoint; - if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) - { - return true; - } - } - } - //generally should not make it to this point FIXME: write proper assertion - //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); - - if( options::cbqiNopt() ){ - //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - for( unsigned j=0; jconstructInstantiationInc( - pv, val, pv_prop_nopt_bound, sf)) - { - return true; - } - } - } - } - } - } - } - return false; -} - -bool ArithInstantiator::needsPostProcessInstantiationForVariable( - CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) -{ - return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end(); -} - -bool ArithInstantiator::postProcessInstantiationForVariable( - CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort, - std::vector& lemmas) -{ - Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() ); - Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); - unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); - Assert( !sf.d_props[index].isBasic() ); - Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] ); - if( Trace.isOn("cegqi-arith-debug") ){ - Trace("cegqi-arith-debug") << "Normalize substitution for "; - Trace("cegqi-arith-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl; - } - Assert( sf.d_vars[index].getType().isInteger() ); - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_rhs = sf.d_subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(eq, msum)) - { - Node veq; - if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) != 0) - { - Node veq_c; - if( veq[0]!=sf.d_vars[index] ){ - Node veq_v; - if (ArithMSum::getMonomial(veq[0], veq_c, veq_v)) - { - Assert( veq_v==sf.d_vars[index] ); - } - } - sf.d_subs[index] = veq[1]; - if( !veq_c.isNull() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cegqi-arith-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl; - //intger division rounding up if from a lower bound - if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){ - sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), - ci->getQuantifiersEngine()->getTermUtil()->d_zero ), - ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one ) - ); - } - } - Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; - }else{ - Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; - return false; - } - }else{ - Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; - return false; - } - return true; -} - -void DtInstantiator::reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ -} - -Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { - Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; - Node ret; - if( !a.isNull() && a==v ){ - ret = sb; - }else if( !b.isNull() && b==v ){ - ret = sa; - }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ - if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - if( a.getOperator()==b.getOperator() ){ - for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), sb ); - Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); - if( !s.isNull() ){ - return s; - } - } - } - }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ - return solve_dt( v, b, a, sb, sa ); - } - if( !ret.isNull() ){ - //ensure does not contain - if (ret.hasSubterm(v)) - { - ret = Node::null(); - } - } - return ret; -} - -bool DtInstantiator::processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& eqc, - CegInstEffort effort) -{ - Trace("cegqi-dt-debug") << "try based on constructors in equivalence class." - << std::endl; - // look in equivalence class for a constructor - for( unsigned k=0; k children; - children.push_back( n.getOperator() ); - const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); - unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); - //now must solve for selectors applied to pv - for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( d_type.toType(), j ) ), pv ); - ci->pushStackVariable( c ); - children.push_back( c ); - } - Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - TermProperties pv_prop_dt; - if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf)) - { - return true; - }else{ - //cleanup - for( unsigned j=0; jpopStackVariable(); - } - break; - } - } - } - return false; -} - -bool DtInstantiator::processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& term_props, - std::vector& terms, - CegInstEffort effort) -{ - Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); - if( !val.isNull() ){ - TermProperties pv_prop; - if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) - { - return true; - } - } - return false; -} - -void EprInstantiator::reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - d_equal_terms.clear(); -} - -bool EprInstantiator::processEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - TermProperties& pv_prop, - Node n, - CegInstEffort effort) -{ - if( options::quantEprMatching() ){ - Assert( pv_prop.isBasic() ); - d_equal_terms.push_back( n ); - return false; - }else{ - pv_prop.d_type = 0; - return ci->constructInstantiationInc(pv, n, pv_prop, sf); - } -} - -void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { - if( index==catom.getNumChildren() ){ - Assert( tat->hasNodeData() ); - Node gcatom = tat->getNodeData(); - Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl; - for( unsigned i=0; i::iterator it = tat->d_data.find( arg_reps[index] ); - if( it!=tat->d_data.end() ){ - computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); - } - } -} - -void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { - if (inst::Trigger::isAtomicTrigger(catom) && catom.hasSubterm(pv)) - { - Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; - std::vector< Node > arg_reps; - for( unsigned j=0; jgetQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); - } - if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ - Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); - Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); - TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); - Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; - if( tat ){ - computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); - } - } - } -} - -struct sortEqTermsMatch { - std::map< Node, int > d_match_score; - bool operator() (Node i, Node j) { - int match_score_i = d_match_score[i]; - int match_score_j = d_match_score[j]; - return match_score_i>match_score_j || ( match_score_i==match_score_j && i& eqc, - CegInstEffort effort) -{ - if( options::quantEprMatching() ){ - //heuristic for best matching constant - sortEqTermsMatch setm; - for( unsigned i=0; igetNumCEAtoms(); i++ ){ - Node catom = ci->getCEAtom( i ); - computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); - } - //sort by match score - std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); - TermProperties pv_prop; - pv_prop.d_type = 0; - for( unsigned i=0; iconstructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf)) - { - return true; - } - } - } - return false; -} - -// this class can be used to query the model value through the CegInstaniator class -class CegInstantiatorBvInverterQuery : public BvInverterQuery -{ - public: - CegInstantiatorBvInverterQuery(CegInstantiator* ci) - : BvInverterQuery(), d_ci(ci) - { - } - ~CegInstantiatorBvInverterQuery() {} - /** return the model value of n */ - Node getModelValue(Node n) override { return d_ci->getModelValue(n); } - /** get bound variable of type tn */ - Node getBoundVariable(TypeNode tn) override - { - return d_ci->getBoundVariable(tn); - } - - protected: - // pointer to class that is able to query model values - CegInstantiator * d_ci; -}; - -BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn), d_tried_assertion_inst(false) -{ - // get the global inverter utility - // this must be global since we need to: - // * process Skolem functions properly across multiple variables within the same quantifier - // * cache Skolem variables uniformly across multiple quantified formulas - d_inverter = qe->getBvInverter(); -} - -BvInstantiator::~BvInstantiator(){ - -} -void BvInstantiator::reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - d_inst_id_counter = 0; - d_var_to_inst_id.clear(); - d_inst_id_to_term.clear(); - d_inst_id_to_alit.clear(); - d_var_to_curr_inst_id.clear(); - d_alit_to_model_slack.clear(); - d_tried_assertion_inst = false; -} - -void BvInstantiator::processLiteral(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) -{ - Assert(d_inverter != NULL); - // find path to pv - std::vector path; - Node sv = d_inverter->getSolveVariable(pv.getType()); - Node pvs = ci->getModelValue(pv); - Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl; - Node slit = - d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl()); - if (!slit.isNull()) - { - CegInstantiatorBvInverterQuery m(ci); - unsigned iid = d_inst_id_counter; - Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl; - Node inst = d_inverter->solveBvLit(sv, slit, path, &m); - if (!inst.isNull()) - { - inst = Rewriter::rewrite(inst); - if (inst.isConst() || !ci->hasNestedQuantification()) - { - Trace("cegqi-bv") << "...solved form is " << inst << std::endl; - // store information for id and increment - d_var_to_inst_id[pv].push_back(iid); - d_inst_id_to_term[iid] = inst; - d_inst_id_to_alit[iid] = alit; - d_inst_id_counter++; - } - } - else - { - Trace("cegqi-bv") << "...failed to solve." << std::endl; - } - } - else - { - Trace("cegqi-bv") << "...no path." << std::endl; - } -} - -Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - CegInstEffort effort) -{ - if (effort == CEG_INST_EFFORT_FULL) - { - // always use model values at full effort - return Node::null(); - } - Node atom = lit.getKind() == NOT ? lit[0] : lit; - bool pol = lit.getKind() != NOT; - Kind k = atom.getKind(); - if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT) - { - // others are unhandled - return Node::null(); - } - else if (!atom[0].getType().isBitVector()) - { - return Node::null(); - } - else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP - || (pol && k == EQUAL)) - { - return lit; - } - NodeManager* nm = NodeManager::currentNM(); - Node s = atom[0]; - Node t = atom[1]; - - Node sm = ci->getModelValue(s); - Node tm = ci->getModelValue(t); - Assert(!sm.isNull() && sm.isConst()); - Assert(!tm.isNull() && tm.isConst()); - Trace("cegqi-bv") << "Model value: " << std::endl; - Trace("cegqi-bv") << " " << s << " " << k << " " << t << " is " - << std::endl; - Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; - - Node ret; - if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) - { - // if using slack, we convert constraints to a positive equality based on - // the current model M, e.g.: - // (not) s ~ t ---> s = t + ( s^M - t^M ) - if (sm != tm) - { - Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); - Assert(slack.isConst()); - // remember the slack value for the asserted literal - d_alit_to_model_slack[lit] = slack; - ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack)); - Trace("cegqi-bv") << "Slack is " << slack << std::endl; - } - else - { - ret = s.eqNode(t); - } - } else { - // turn disequality into an inequality - // e.g. s != t becomes s < t or t < s - if (k == EQUAL) - { - if (Random::getRandom().pickWithProb(0.5)) - { - std::swap(s, t); - } - pol = true; - } - // otherwise, we optimistically solve for the boundary point of an - // inequality, for example: - // for s < t, we solve s+1 = t - // for ~( s < t ), we solve s = t - // notice that this equality does not necessarily hold in the model, and - // hence the corresponding instantiation strategy is not guaranteed to be - // monotonic. - if (!pol) - { - ret = s.eqNode(t); - } else { - Node bv_one = bv::utils::mkOne(bv::utils::getSize(s)); - ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t); - } - } - Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; - return ret; -} - -bool BvInstantiator::processAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) -{ - // if option enabled, use approach for word-level inversion for BV instantiation - if( options::cbqiBv() ){ - // get the best rewritten form of lit for solving for pv - // this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible - Node rlit = rewriteAssertionForSolvePv(ci, pv, lit); - if( Trace.isOn("cegqi-bv") ){ - Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl; - if( lit!=rlit ){ - Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl; - } - } - if (!rlit.isNull()) - { - processLiteral(ci, sf, pv, rlit, alit, effort); - } - } - return false; -} - -bool BvInstantiator::useModelValue(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - return !d_tried_assertion_inst - && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort()); -} - -bool BvInstantiator::processAssertions(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv ); - if( iti!=d_var_to_inst_id.end() ){ - Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; - // if interleaving, do not do inversion half the time - if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5)) - { - bool firstVar = sf.empty(); - // get inst id list - if (Trace.isOn("cegqi-bv")) - { - Trace("cegqi-bv") << " " << iti->second.size() - << " candidate instantiations for " << pv << " : " - << std::endl; - if (firstVar) - { - Trace("cegqi-bv") << " ...this is the first variable" << std::endl; - } - } - // until we have a model-preserving selection function for BV, this must - // be heuristic (we only pick one literal) - // hence we randomize the list - // this helps robustness, since picking the same literal every time may - // lead to a stream of value instantiations, whereas with randomization - // we may find an invertible literal that leads to a useful instantiation. - std::random_shuffle(iti->second.begin(), iti->second.end()); - - if (Trace.isOn("cegqi-bv")) - { - for (unsigned j = 0, size = iti->second.size(); j < size; j++) - { - unsigned inst_id = iti->second[j]; - Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); - Node inst_term = d_inst_id_to_term[inst_id]; - Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); - Node alit = d_inst_id_to_alit[inst_id]; - - // get the slack value introduced for the asserted literal - Node curr_slack_val; - std::unordered_map::iterator itms = - d_alit_to_model_slack.find(alit); - if (itms != d_alit_to_model_slack.end()) - { - curr_slack_val = itms->second; - } - - // debug printing - Trace("cegqi-bv") << " [" << j << "] : "; - Trace("cegqi-bv") << inst_term << std::endl; - if (!curr_slack_val.isNull()) { - Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val - << std::endl; - } - Trace("cegqi-bv-debug") << " ...from : " << alit << std::endl; - Trace("cegqi-bv") << std::endl; - } - } - - // Now, try all instantiation ids we want to try - // Typically we try only one, otherwise worst-case performance - // for constructing instantiations is exponential on the number of - // variables in this quantifier prefix. - bool ret = false; - bool tryMultipleInst = firstVar && options::cbqiMultiInst(); - bool revertOnSuccess = tryMultipleInst; - for (unsigned j = 0, size = iti->second.size(); j < size; j++) - { - unsigned inst_id = iti->second[j]; - Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); - Node inst_term = d_inst_id_to_term[inst_id]; - Node alit = d_inst_id_to_alit[inst_id]; - // try instantiation pv -> inst_term - TermProperties pv_prop_bv; - Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term - << std::endl; - d_var_to_curr_inst_id[pv] = inst_id; - d_tried_assertion_inst = true; - ci->markSolved(alit); - if (ci->constructInstantiationInc( - pv, inst_term, pv_prop_bv, sf, revertOnSuccess)) - { - ret = true; - } - ci->markSolved(alit, false); - // we are done unless we try multiple instances - if (!tryMultipleInst) - { - break; - } - } - if (ret) - { - return true; - } - Trace("cegqi-bv") << "...failed to add instantiation for " << pv - << std::endl; - d_var_to_curr_inst_id.erase(pv); - } else { - Trace("cegqi-bv") << "...do not do instantiation for " << pv - << " (skip, based on heuristic)" << std::endl; - } - } - - return false; -} - -Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, - Node pv, - Node lit) -{ - // result of rewriting the visited term - std::stack > visited; - visited.push(std::unordered_map()); - // whether the visited term contains pv - std::unordered_map visited_contains_pv; - std::unordered_map::iterator it; - std::unordered_map curr_subs; - std::stack > visit; - TNode cur; - visit.push(std::stack()); - visit.top().push(lit); - do { - cur = visit.top().top(); - visit.top().pop(); - it = visited.top().find(cur); - - if (it == visited.top().end()) - { - std::unordered_map::iterator itc = - curr_subs.find(cur); - if (itc != curr_subs.end()) - { - visited.top()[cur] = itc->second; - } - else - { - if (cur.getKind() == CHOICE) - { - // must replace variables of choice functions - // with new variables to avoid variable - // capture when considering substitutions - // with multiple literals. - Node bv = ci->getBoundVariable(cur[0][0].getType()); - // should not have captured variables - Assert(curr_subs.find(cur[0][0]) == curr_subs.end()); - curr_subs[cur[0][0]] = bv; - // we cannot cache the results of subterms - // of this choice expression since we are - // now in the context { cur[0][0] -> bv }, - // hence we push a context here - visited.push(std::unordered_map()); - visit.push(std::stack()); - } - visited.top()[cur] = Node::null(); - visit.top().push(cur); - for (unsigned i = 0; i < cur.getNumChildren(); i++) - { - visit.top().push(cur[i]); - } - } - } else if (it->second.isNull()) { - Node ret; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back(cur.getOperator()); - } - bool contains_pv = ( cur==pv ); - for (unsigned i = 0; i < cur.getNumChildren(); i++) { - it = visited.top().find(cur[i]); - Assert(it != visited.top().end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cur[i] != it->second; - children.push_back(it->second); - contains_pv = contains_pv || visited_contains_pv[cur[i]]; - } - // careful that rewrites above do not affect whether this term contains pv - visited_contains_pv[cur] = contains_pv; - - // rewrite the term - ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv); - - // return original if the above function does not produce a result - if (ret.isNull()) { - if (childChanged) { - ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); - }else{ - ret = cur; - } - } - - /* We need to update contains_pv also for rewritten nodes, since - * the normalizePv* functions rely on the information if pv occurs in a - * rewritten node or not. */ - if (ret != cur) - { - contains_pv = (ret == pv); - for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i) - { - contains_pv = contains_pv || visited_contains_pv[ret[i]]; - } - visited_contains_pv[ret] = contains_pv; - } - - // if was choice, pop context - if (cur.getKind() == CHOICE) - { - Assert(curr_subs.find(cur[0][0]) != curr_subs.end()); - curr_subs.erase(cur[0][0]); - visited.pop(); - visit.pop(); - Assert(visited.size() == visit.size()); - Assert(!visit.empty()); - } - - visited.top()[cur] = ret; - } - } while (!visit.top().empty()); - Assert(visited.size() == 1); - Assert(visited.top().find(lit) != visited.top().end()); - Assert(!visited.top().find(lit)->second.isNull()); - - Node result = visited.top()[lit]; - - if (Trace.isOn("cegqi-bv-nl")) - { - std::vector trace_visit; - std::unordered_set trace_visited; - - trace_visit.push_back(result); - do - { - cur = trace_visit.back(); - trace_visit.pop_back(); - - if (trace_visited.find(cur) == trace_visited.end()) - { - trace_visited.insert(cur); - trace_visit.insert(trace_visit.end(), cur.begin(), cur.end()); - } - else if (cur == pv) - { - Trace("cegqi-bv-nl") - << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl; - } - } while (!trace_visit.empty()); - } - - return result; -} - -/** - * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, - * or -pv * t. Extracting the coefficient of multiplications only succeeds if - * the multiplication are normalized with normalizePvMult. - * - * If sucessful it returns - * 1 if n == pv, - * -1 if n == -pv, - * t if n == pv * t, - * -t if n == -pv * t. - * If n is not a linear term, a null node is returned. - */ -static Node getPvCoeff(TNode pv, TNode n) -{ - bool neg = false; - Node coeff; - - if (n.getKind() == BITVECTOR_NEG) - { - neg = true; - n = n[0]; - } - - if (n == pv) - { - coeff = bv::utils::mkOne(bv::utils::getSize(pv)); - } - /* All multiplications are normalized to pv * (t1 * t2). */ - else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) - { - Assert(n.getNumChildren() == 2); - Assert(n[0] == pv); - coeff = n[1]; - } - else /* n is in no form to extract the coefficient for pv */ - { - Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " - << n << std::endl; - return Node::null(); - } - Assert(!coeff.isNull()); - - if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); - return coeff; -} - -/** - * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * -pv * b * c - * - * is rewritten to - * - * pv * -(a * b * c) - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns a - * multiplication over children. - */ -static Node normalizePvMult( - TNode pv, - const std::vector& children, - std::unordered_map& contains_pv) -{ - bool neg, neg_coeff = false; - bool found_pv = false; - NodeManager* nm; - NodeBuilder<> nb(BITVECTOR_MULT); - BvLinearAttribute is_linear; - - nm = NodeManager::currentNM(); - for (TNode nc : children) - { - if (!contains_pv[nc]) - { - nb << nc; - continue; - } - - neg = false; - if (nc.getKind() == BITVECTOR_NEG) - { - neg = true; - nc = nc[0]; - } - - if (!found_pv && nc == pv) - { - found_pv = true; - neg_coeff = neg; - continue; - } - else if (!found_pv && nc.getKind() == BITVECTOR_MULT - && nc.getAttribute(is_linear)) - { - Assert(nc.getNumChildren() == 2); - Assert(nc[0] == pv); - Assert(!contains_pv[nc[1]]); - found_pv = true; - neg_coeff = neg; - nb << nc[1]; - continue; - } - return Node::null(); /* non-linear */ - } - Assert(nb.getNumChildren() > 0); - - Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); - if (neg_coeff) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - } - coeff = Rewriter::rewrite(coeff); - unsigned size_coeff = bv::utils::getSize(coeff); - Node zero = bv::utils::mkZero(size_coeff); - if (coeff == zero) - { - return zero; - } - Node result; - if (found_pv) - { - if (coeff == bv::utils::mkOne(size_coeff)) - { - return pv; - } - result = nm->mkNode(BITVECTOR_MULT, pv, coeff); - contains_pv[result] = true; - result.setAttribute(is_linear, true); - } - else - { - result = coeff; - } - return result; -} - -#ifdef CVC4_ASSERTIONS -static bool isLinearPlus( - TNode n, - TNode pv, - std::unordered_map& contains_pv) -{ - Node coeff; - Assert(n.getAttribute(BvLinearAttribute())); - Assert(n.getNumChildren() == 2); - if (n[0] != pv) - { - Assert(n[0].getKind() == BITVECTOR_MULT); - Assert(n[0].getNumChildren() == 2); - Assert(n[0][0] == pv); - Assert(!contains_pv[n[0][1]]); - } - Assert(!contains_pv[n[1]]); - coeff = getPvCoeff(pv, n[0]); - Assert(!coeff.isNull()); - Assert(!contains_pv[coeff]); - return true; -} -#endif - -/** - * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * pv + b + c * -pv - * - * is rewritten to - * - * pv * (a - c) + b - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns an - * addition over children. - */ -static Node normalizePvPlus( - Node pv, - const std::vector& children, - std::unordered_map& contains_pv) -{ - NodeManager* nm; - NodeBuilder<> nb_c(BITVECTOR_PLUS); - NodeBuilder<> nb_l(BITVECTOR_PLUS); - BvLinearAttribute is_linear; - bool neg; - - nm = NodeManager::currentNM(); - for (TNode nc : children) - { - if (!contains_pv[nc]) - { - nb_l << nc; - continue; - } - - neg = false; - if (nc.getKind() == BITVECTOR_NEG) - { - neg = true; - nc = nc[0]; - } - - if (nc == pv - || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) - { - Node coeff = getPvCoeff(pv, nc); - Assert(!coeff.isNull()); - if (neg) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - } - nb_c << coeff; - continue; - } - else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) - { - Assert(isLinearPlus(nc, pv, contains_pv)); - Node coeff = getPvCoeff(pv, nc[0]); - Assert(!coeff.isNull()); - Node leaf = nc[1]; - if (neg) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - leaf = nm->mkNode(BITVECTOR_NEG, leaf); - } - nb_c << coeff; - nb_l << leaf; - continue; - } - /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ - return Node::null(); - } - Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); - - Node pv_mult_coeffs, result; - if (nb_c.getNumChildren() > 0) - { - Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); - coeffs = Rewriter::rewrite(coeffs); - result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv); - } - - if (nb_l.getNumChildren() > 0) - { - Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); - leafs = Rewriter::rewrite(leafs); - Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); - /* pv * 0 + t --> t */ - if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) - { - result = leafs; - } - else - { - result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); - contains_pv[result] = true; - result.setAttribute(is_linear, true); - } - } - Assert(!result.isNull()); - return result; -} - -/** - * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv - * marks terms in which pv occurs. - * For example, equality - * - * -pv * a + b = c + pv - * - * rewrites to - * - * pv * (-a - 1) = c - b. - */ -static Node normalizePvEqual( - Node pv, - const std::vector& children, - std::unordered_map& contains_pv) -{ - Assert(children.size() == 2); - - NodeManager* nm = NodeManager::currentNM(); - BvLinearAttribute is_linear; - Node coeffs[2], leafs[2]; - bool neg; - TNode child; - - for (unsigned i = 0; i < 2; ++i) - { - child = children[i]; - neg = false; - if (child.getKind() == BITVECTOR_NEG) - { - neg = true; - child = child[0]; - } - if (child.getAttribute(is_linear) || child == pv) - { - if (child.getKind() == BITVECTOR_PLUS) - { - Assert(isLinearPlus(child, pv, contains_pv)); - coeffs[i] = getPvCoeff(pv, child[0]); - leafs[i] = child[1]; - } - else - { - Assert(child.getKind() == BITVECTOR_MULT || child == pv); - coeffs[i] = getPvCoeff(pv, child); - } - } - if (neg) - { - if (!coeffs[i].isNull()) - { - coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); - } - if (!leafs[i].isNull()) - { - leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); - } - } - } - - if (coeffs[0].isNull() || coeffs[1].isNull()) - { - return Node::null(); - } - - Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); - coeff = Rewriter::rewrite(coeff); - std::vector mult_children = {pv, coeff}; - Node lhs = normalizePvMult(pv, mult_children, contains_pv); - - Node rhs; - if (!leafs[0].isNull() && !leafs[1].isNull()) - { - rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); - } - else if (!leafs[0].isNull()) - { - rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); - } - else if (!leafs[1].isNull()) - { - rhs = leafs[1]; - } - else - { - rhs = bv::utils::mkZero(bv::utils::getSize(pv)); - } - rhs = Rewriter::rewrite(rhs); - - if (lhs == rhs) - { - return bv::utils::mkTrue(); - } - - Node result = lhs.eqNode(rhs); - contains_pv[result] = true; - return result; -} - -Node BvInstantiator::rewriteTermForSolvePv( - Node pv, - Node n, - std::vector& children, - std::unordered_map& contains_pv) -{ - NodeManager* nm = NodeManager::currentNM(); - - // [1] rewrite cases of non-invertible operators - - if (n.getKind() == EQUAL) - { - TNode lhs = children[0]; - TNode rhs = children[1]; - - /* rewrite: x * x = x -> x < 2 */ - if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv - && rhs[1] == pv) - || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv - && lhs[1] == pv)) - { - return nm->mkNode( - BITVECTOR_ULT, - pv, - bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); - } - - if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) - { - Node result = normalizePvEqual(pv, children, contains_pv); - if (!result.isNull()) - { - Trace("cegqi-bv-nl") - << "Normalize " << n << " to " << result << std::endl; - } - else - { - Trace("cegqi-bv-nl") - << "Nonlinear " << n.getKind() << " " << n << std::endl; - } - return result; - } - } - else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) - { - if (options::cbqiBvLinearize() && contains_pv[n]) - { - Node result; - if (n.getKind() == BITVECTOR_MULT) - { - result = normalizePvMult(pv, children, contains_pv); - } - else - { - result = normalizePvPlus(pv, children, contains_pv); - } - if (!result.isNull()) - { - Trace("cegqi-bv-nl") - << "Normalize " << n << " to " << result << std::endl; - return result; - } - else - { - Trace("cegqi-bv-nl") - << "Nonlinear " << n.getKind() << " " << n << std::endl; - } - } - } - - // [2] try to rewrite non-linear literals -> linear literals - - return Node::null(); -} - -/** sort bv extract interval - * - * This sorts lists of bitvector extract terms where - * ((_ extract i1 i2) t) < ((_ extract j1 j2) t) - * if i1>j1 or i1=j1 and i2>j2. - */ -struct SortBvExtractInterval -{ - bool operator()(Node i, Node j) - { - Assert(i.getKind() == BITVECTOR_EXTRACT); - Assert(j.getKind() == BITVECTOR_EXTRACT); - BitVectorExtract ie = i.getOperator().getConst(); - BitVectorExtract je = j.getOperator().getConst(); - if (ie.high > je.high) - { - return true; - } - else if (ie.high == je.high) - { - Assert(ie.low != je.low); - return ie.low > je.low; - } - return false; - } -}; - -void BvInstantiatorPreprocess::registerCounterexampleLemma( - std::vector& lems, std::vector& ce_vars) -{ - // new variables - std::vector vars; - // new lemmas - std::vector new_lems; - - if (options::cbqiBvRmExtract()) - { - NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; - // map from terms to bitvector extracts applied to that term - std::map > extract_map; - std::unordered_set visited; - for (unsigned i = 0, size = lems.size(); i < size; i++) - { - Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : " - << lems[i] << std::endl; - collectExtracts(lems[i], extract_map, visited); - } - for (std::pair >& es : extract_map) - { - // sort based on the extract start position - std::vector& curr_vec = es.second; - - SortBvExtractInterval sbei; - std::sort(curr_vec.begin(), curr_vec.end(), sbei); - - unsigned width = es.first.getType().getBitVectorSize(); - - // list of points b such that: - // b>0 and we must start a segment at (b-1) or b==0 - std::vector boundaries; - boundaries.push_back(width); - boundaries.push_back(0); - - Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl; - for (unsigned i = 0, size = curr_vec.size(); i < size; i++) - { - Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i] << std::endl; - BitVectorExtract e = - curr_vec[i].getOperator().getConst(); - if (std::find(boundaries.begin(), boundaries.end(), e.high + 1) - == boundaries.end()) - { - boundaries.push_back(e.high + 1); - } - if (std::find(boundaries.begin(), boundaries.end(), e.low) - == boundaries.end()) - { - boundaries.push_back(e.low); - } - } - std::sort(boundaries.rbegin(), boundaries.rend()); - - // make the extract variables - std::vector children; - for (unsigned i = 1; i < boundaries.size(); i++) - { - Assert(boundaries[i - 1] > 0); - Node ex = bv::utils::mkExtract( - es.first, boundaries[i - 1] - 1, boundaries[i]); - Node var = - nm->mkSkolem("ek", - ex.getType(), - "variable to represent disjoint extract region"); - children.push_back(var); - vars.push_back(var); - } - - Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children); - Assert(conc.getType() == es.first.getType()); - Node eq_lem = conc.eqNode(es.first); - Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl; - new_lems.push_back(eq_lem); - Trace("cegqi-bv-pp") << "...finished processing extracts for term " - << es.first << std::endl; - } - Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl; - } - - if (!vars.empty()) - { - // could try applying subs -> vars here - // in practice, this led to worse performance - - Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..." - << std::endl; - lems.insert(lems.end(), new_lems.begin(), new_lems.end()); - Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..." - << std::endl; - ce_vars.insert(ce_vars.end(), vars.begin(), vars.end()); - } -} - -void BvInstantiatorPreprocess::collectExtracts( - Node lem, - std::map >& extract_map, - std::unordered_set& visited) -{ - std::vector visit; - TNode cur; - visit.push_back(lem); - do - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur.getKind() != FORALL) - { - if (cur.getKind() == BITVECTOR_EXTRACT) - { - if (cur[0].getKind() == INST_CONSTANT) - { - extract_map[cur[0]].push_back(cur); - } - } - - for (const Node& nc : cur) - { - visit.push_back(nc); - } - } - } - } while (!visit.empty()); -} - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h deleted file mode 100644 index 306b65cc3..000000000 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h +++ /dev/null @@ -1,332 +0,0 @@ -/********************* */ -/*! \file ceg_t_instantiator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief theory-specific counterexample-guided quantifier instantiation - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__CEG_T_INSTANTIATOR_H -#define __CVC4__CEG_T_INSTANTIATOR_H - -#include "theory/quantifiers/bv_inverter.h" -#include "theory/quantifiers/cegqi/ceg_instantiator.h" - -#include - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** TODO (#1367) : document these classes, also move to separate files. */ - -class ArithInstantiator : public Instantiator { - public: - ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~ArithInstantiator(){} - void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool hasProcessEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override - { - return true; - } - bool processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& term_props, - std::vector& terms, - CegInstEffort effort) override; - bool hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override - { - return true; - } - Node hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - CegInstEffort effort) override; - bool processAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) override; - bool processAssertions(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool postProcessInstantiationForVariable(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort, - std::vector& lemmas) override; - std::string identify() const override { return "Arith"; } - - private: - Node d_vts_sym[2]; - std::vector d_mbp_bounds[2]; - std::vector d_mbp_coeff[2]; - std::vector d_mbp_vts_coeff[2][2]; - std::vector d_mbp_lit[2]; - int solve_arith(CegInstantiator* ci, - Node v, - Node atom, - Node& veq_c, - Node& val, - Node& vts_coeff_inf, - Node& vts_coeff_delta); - Node getModelBasedProjectionValue(CegInstantiator* ci, - Node e, - Node t, - bool isLower, - Node c, - Node me, - Node mt, - Node theta, - Node inf_coeff, - Node delta_coeff); -}; - -class DtInstantiator : public Instantiator { -public: - DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~DtInstantiator(){} - void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& eqc, - CegInstEffort effort) override; - bool hasProcessEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override - { - return true; - } - bool processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& term_props, - std::vector& terms, - CegInstEffort effort) override; - std::string identify() const override { return "Dt"; } - - private: - Node solve_dt(Node v, Node a, Node b, Node sa, Node sb); -}; - -class TermArgTrie; - -class EprInstantiator : public Instantiator { - public: - EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~EprInstantiator(){} - void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool processEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - TermProperties& pv_prop, - Node n, - CegInstEffort effort) override; - bool processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& eqc, - CegInstEffort effort) override; - std::string identify() const override { return "Epr"; } - - private: - std::vector d_equal_terms; - void computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - std::vector& arg_reps, - TermArgTrie* tat, - unsigned index, - std::map& match_score); - void computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - Node eqc, - std::map& match_score); -}; - -/** Bitvector instantiator - * - * This implements an approach for counterexample-guided instantiation - * for bit-vector variables based on word-level inversions. - * It is enabled by --cbqi-bv. - */ -class BvInstantiator : public Instantiator { - public: - BvInstantiator(QuantifiersEngine* qe, TypeNode tn); - ~BvInstantiator() override; - void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - bool hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override - { - return true; - } - Node hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - CegInstEffort effort) override; - bool processAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) override; - bool processAssertions(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - /** use model value - * - * We allow model values if we have not already tried an assertion, - * and only at levels below full if cbqiFullEffort is false. - */ - bool useModelValue(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - std::string identify() const override { return "Bv"; } - - private: - // point to the bv inverter class - BvInverter * d_inverter; - unsigned d_inst_id_counter; - /** information about solved forms */ - std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id; - std::unordered_map< unsigned, Node > d_inst_id_to_term; - std::unordered_map d_inst_id_to_alit; - // variable to current id we are processing - std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; - /** the amount of slack we added for asserted literals */ - std::unordered_map d_alit_to_model_slack; - /** whether we have tried an instantiation based on assertion in this round */ - bool d_tried_assertion_inst; - /** rewrite assertion for solve pv - * returns a literal that is equivalent to lit that leads to best solved form for pv - */ - Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit); - /** rewrite term for solve pv - * This is a helper function for rewriteAssertionForSolvePv. - * If this returns non-null value ret, then this indicates - * that n should be rewritten to ret. It is called as - * a "post-rewrite", that is, after the children of n - * have been rewritten and stored in the vector children. - * - * contains_pv stores whether certain nodes contain pv. - * where we guarantee that all subterms of terms in children - * appear in the domain of contains_pv. - */ - Node rewriteTermForSolvePv( - Node pv, - Node n, - std::vector& children, - std::unordered_map& contains_pv); - /** process literal, called from processAssertion - * lit is the literal to solve for pv that has been rewritten according to - * internal rules here. - * alit is the asserted literal that lit is derived from. - */ - void processLiteral(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort); -}; - -/** Bitvector instantiator preprocess - * - * This class implements preprocess techniques that are helpful for - * counterexample-guided instantiation, such as introducing variables - * that refer to disjoint bit-vector extracts. - */ -class BvInstantiatorPreprocess : public InstantiatorPreprocess -{ - public: - BvInstantiatorPreprocess() {} - ~BvInstantiatorPreprocess() override {} - /** register counterexample lemma - * - * This method modifies the contents of lems based on the extract terms - * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces - * a dummy equality so that segments of terms t under extracts can be solved - * independently. - * - * For example: - * P[ ((extract 7 4) t), ((extract 3 0) t)] - * becomes: - * P[((extract 7 4) t), ((extract 3 0) t)] ^ - * t = concat( x74, x30 ) - * where x74 and x30 are fresh variables of type BV_4. - * - * Another example: - * P[ ((extract 7 3) t), ((extract 4 0) t)] - * becomes: - * P[((extract 7 4) t), ((extract 3 0) t)] ^ - * t = concat( x75, x44, x30 ) - * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4 - * respectively. - * - * Notice we leave the original conjecture alone. This is done for performance - * since the added equalities ensure we are able to construct the proper - * solved forms for variables in t and for the intermediate variables above. - */ - void registerCounterexampleLemma(std::vector& lems, - std::vector& ce_vars) override; - - private: - /** collect extracts - * - * This method collects all extract terms in lem - * and stores them in d_extract_map. - * visited is the terms we've already visited. - */ - void collectExtracts(Node lem, - std::map >& extract_map, - std::unordered_set& visited); -}; - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ - -#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 37f11f9cd..3d966726b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -21,7 +21,7 @@ #include "theory/datatypes/theory_datatypes.h" #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/anti_skolem.h" -#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" +#include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 24e3ca98c..4c96f6cb9 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -22,7 +22,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -#include "theory/quantifiers/cegqi/ceg_t_instantiator.cpp" +#include "theory/quantifiers/cegqi/ceg_bv_instantiator.cpp" #include #include