From 12588439a7b1497d03d1ffb0d4b9ed4646ac9bdf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 13:41:46 -0600 Subject: [PATCH] Remove unecessary CEGQI options (#8281) Code changed indenting, but did not change otherwise. --- src/options/quantifiers_options.toml | 16 --- src/smt/set_defaults.cpp | 3 +- .../cegqi/ceg_arith_instantiator.cpp | 131 +++++++----------- .../quantifiers/cegqi/ceg_instantiator.cpp | 10 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 3 +- 5 files changed, 53 insertions(+), 110 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 660170c4d..dce3bfa69 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1559,22 +1559,6 @@ name = "Quantifiers" default = "false" help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation" -[[option]] - name = "cegqiSat" - category = "regular" - long = "cegqi-sat" - type = "bool" - default = "true" - help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation" - -[[option]] - name = "cegqiModel" - category = "regular" - long = "cegqi-model" - type = "bool" - default = "true" - help = "guide instantiations by model values for counterexample-based quantifier instantiation" - [[option]] name = "cegqiAll" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 140510b3f..4c1df2d05 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1452,8 +1452,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { opts.quantifiers.instNoEntail = false; } - if (!opts.quantifiers.instWhenModeWasSetByUser - && opts.quantifiers.cegqiModel) + if (!opts.quantifiers.instWhenModeWasSetByUser) { // only instantiation should happen at last call when model is avaiable opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 82a285f6f..a8dbbce67 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -166,7 +166,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } // compute how many bounds we will consider unsigned rmax = 1; - if (atom.getKind() == EQUAL && (pol || !options().quantifiers.cegqiModel)) + if (atom.getKind() == EQUAL && pol) { rmax = 2; } @@ -205,48 +205,40 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { // disequalities are either strict upper or lower bounds bool is_upper; - if (options().quantifiers.cegqiModel) + // 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()) { - // 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 = 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. - // It also may be the case that cmp is non-constant, in the case - // where lhs or rhs contains a transcendental function. We consider - // the bound to be an upper bound in this case. - Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); - cmp = rewrite(cmp); - is_upper = !cmp.isConst() || !cmp.getConst(); - } + // 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 { - // since we are not using the model, we try both. - is_upper = (r == 0); + 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 = 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. + // It also may be the case that cmp is non-constant, in the case + // where lhs or rhs contains a transcendental function. We consider + // the bound to be an upper bound in this case. + Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); + cmp = rewrite(cmp); + is_upper = !cmp.isConst() || !cmp.getConst(); } Assert(atom.getKind() == EQUAL && !pol); if (d_type.isInteger()) @@ -274,54 +266,31 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, // take into account delta if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT) { - if (options().quantifiers.cegqiModel) + Node delta_coeff = nm->mkConstRealOrInt( + d_type, Rational(isUpperBoundCTT(uires) ? 1 : -1)); + if (vts_coeff_delta.isNull()) { - Node delta_coeff = nm->mkConstRealOrInt( - d_type, Rational(isUpperBoundCTT(uires) ? 1 : -1)); - if (vts_coeff_delta.isNull()) - { - vts_coeff_delta = delta_coeff; - } - else - { - vts_coeff_delta = nm->mkNode(ADD, vts_coeff_delta, delta_coeff); - vts_coeff_delta = rewrite(vts_coeff_delta); - } + vts_coeff_delta = delta_coeff; } else { - Node delta = d_vtc->getVtsDelta(); - uval = - nm->mkNode(uires == CEG_TT_UPPER_STRICT ? ADD : SUB, uval, delta); - uval = rewrite(uval); + vts_coeff_delta = nm->mkNode(ADD, vts_coeff_delta, delta_coeff); + vts_coeff_delta = rewrite(vts_coeff_delta); } } - if (options().quantifiers.cegqiModel) + // just store bounds, will choose based on tighest bound + unsigned index = isUpperBoundCTT(uires) ? 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++) { - // just store bounds, will choose based on tighest bound - unsigned index = isUpperBoundCTT(uires) ? 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 = isUpperBoundCTT(uires) ? CEG_TT_UPPER : CEG_TT_LOWER; - if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) - { - return true; - } + d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf + : vts_coeff_delta); } + d_mbp_lit[index].push_back(lit); } return false; } @@ -331,10 +300,6 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Node pv, CegInstEffort effort) { - if (!options().quantifiers.cegqiModel) - { - return false; - } NodeManager* nm = NodeManager::currentNM(); bool use_inf = d_type.isInteger() ? options().quantifiers.cegqiUseInfInt : options().quantifiers.cegqiUseInfReal; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 8d1f9f007..9cc3269e5 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -680,12 +680,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, Trace("cegqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl; - Node pv_value; - if (options().quantifiers.cegqiModel) - { - pv_value = getModelValue(pv); - Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; - } + Node pv_value = getModelValue(pv); + Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; //[1] easy case : pv is in the equivalence class as another term not // containing pv @@ -873,7 +869,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { lits.insert(lit); Node plit; - if (options().quantifiers.cegqiRepeatLit || !isSolvedAssertion(lit)) + if (!isSolvedAssertion(lit)) { plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index bbc853ee4..dd68d2de0 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -298,8 +298,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) bool InstStrategyCegqi::checkComplete(IncompleteId& incId) { - if ((!options().quantifiers.cegqiSat && d_cbqi_set_quant_inactive) - || d_incomplete_check) + if (d_incomplete_check) { incId = IncompleteId::QUANTIFIERS_CEGQI; return false; -- 2.30.2