}
// 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;
}
{
// 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<Rational>().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<bool>();
- }
+ // 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<Rational>().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<bool>();
}
Assert(atom.getKind() == EQUAL && !pol);
if (d_type.isInteger())
// 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;
}
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;
projects / cvc5.git / commitdiff