This is work towards making equalities and substitutions between terms of equal types.
else
{
// TODO(#2377): could build ITE here
- Node test = other.eqNode(nm->mkConstReal(Rational(0)));
+ Node test = other.eqNode(
+ nm->mkConstRealOrInt(other.getType(), Rational(0)));
if (rewrite(test) != nm->mkConst<bool>(false))
{
break;
int ires = isolate(v, msum, veq_c, val, k);
if (ires != 0)
{
+ NodeManager* nm = NodeManager::currentNM();
Node vc = v;
if (!veq_c.isNull())
{
if (doCoeff)
{
- vc = NodeManager::currentNM()->mkNode(MULT, veq_c, vc);
+ vc = nm->mkNode(MULT, veq_c, vc);
}
else
{
}
}
bool inOrder = ires == 1;
- veq = NodeManager::currentNM()->mkNode(
- k, inOrder ? vc : val, inOrder ? val : vc);
+ // ensure type is correct for equality
+ if (k == EQUAL)
+ {
+ if (!vc.getType().isInteger() && val.getType().isInteger())
+ {
+ val = nm->mkNode(TO_REAL, val);
+ }
+ // note that conversely this utility will never use a real value as
+ // the solution for an integer, thus the types should match now
+ }
+ veq = nm->mkNode(k, inOrder ? vc : val, inOrder ? val : vc);
}
return ires;
}
tn, Rational(c1.getConst<Rational>() * c2.getConst<Rational>()));
}
-Node mkEquality(Node a, Node b)
+Node mkEquality(const Node& a, const Node& b)
{
NodeManager* nm = NodeManager::currentNM();
Assert(a.getType().isRealOrInt());
return nm->mkNode(EQUAL, diff, mkZero(diff.getType()));
}
+std::pair<Node,Node> mkSameType(const Node& a, const Node& b)
+{
+ TypeNode at = a.getType();
+ TypeNode bt = b.getType();
+ if (at == bt)
+ {
+ return {a, b};
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ if (at.isInteger() && bt.isReal())
+ {
+ return {nm->mkNode(kind::TO_REAL, a), b};
+ }
+ Assert(at.isReal() && bt.isInteger());
+ return {a, nm->mkNode(kind::TO_REAL, b)};
+}
+
} // namespace arith
} // namespace theory
} // namespace cvc5::internal
* types, where zero has the same type as (- a b).
* Use this utility to ensure an equality is properly typed.
*/
-Node mkEquality(Node a, Node b);
+Node mkEquality(const Node& a, const Node& b);
+
+/**
+ * Ensures that the returned pair has equal type, where a and b have
+ * real or integer type. We add TO_REAL if not.
+ */
+std::pair<Node,Node> mkSameType(const Node& a, const Node& b);
+
} // namespace arith
} // namespace theory
// substitution is integral
Trace("simplify") << "TheoryArithPrivate::solve(): substitution "
<< minVar << " |-> " << elim << endl;
+ if (elim.getType().isInteger() && !minVar.getType().isInteger())
+ {
+ elim = NodeManager::currentNM()->mkNode(kind::TO_REAL, elim);
+ }
+ Assert(elim.getType() == minVar.getType());
outSubstitutions.addSubstitutionSolved(minVar, elim, tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
}
<< " ...coefficient " << mult << " is zero." << std::endl;
continue;
}
+ Node lhsTgt = t;
+ Node rhsTgt = rhs;
+ // if we are making an equality below, we require making it
+ // well-typed so that lhs/rhs have the same type. We use the
+ // mkSameType utility to do this
+ if (type == kind::EQUAL)
+ {
+ std::tie(lhsTgt, rhsTgt) = mkSameType(lhsTgt, rhsTgt);
+ }
Trace("nl-ext-bound-debug")
<< " from " << x << " * " << mult << " = " << y << " and " << t
<< " " << type << " " << rhs << ", infer : " << std::endl;
Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type;
- Node infer_lhs = nm->mkNode(Kind::MULT, mult, t);
- Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
+ Node infer_lhs = nm->mkNode(Kind::MULT, mult, lhsTgt);
+ Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhsTgt);
Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
Trace("nl-ext-bound-debug") << " " << infer << std::endl;
Node infer_mv =
d_data->d_model.computeAbstractModelValue(rewrite(infer));
Trace("nl-ext-bound-debug")
<< " ...infer model value is " << infer_mv << std::endl;
- if (infer_mv == d_data->d_false)
+ if (infer_mv.isConst() && !infer_mv.getConst<bool>())
{
Node exp = nm->mkNode(
Kind::AND,
if (d_data->isProofEnabled())
{
proof = d_data->getProof();
- Node simpleeq = nm->mkNode(type, t, rhs);
+ Node simpleeq = nm->mkNode(type, lhsTgt, rhsTgt);
// this is iblem, but uses (type t rhs) instead of the original
// variant (which is identical under rewriting)
// we first infer the "clean" version of the lemma and then
if (mvaoa.getConst<Rational>().sgn() != 0)
{
Node prem = av.eqNode(zero);
- Node conc = oa.eqNode(zero);
+ Node conc = oa.eqNode(mkZero(oa.getType()));
Node lemma = prem.impNode(conc);
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
if (status == 2)
{
// must state that all variables are non-zero
- Node zero = mkZero(oa.getType());
for (const Node& v : vla)
{
- exp.push_back(v.eqNode(zero).negate());
+ exp.push_back(v.eqNode(mkZero(v.getType())).negate());
}
}
Node clem = nm->mkNode(
void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel)
{
+ NodeManager* nm = NodeManager::currentNM();
Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
// If we extended the model with entries x -> 0 for unconstrained values,
// we first update the map to the extended one.
}
else
{
- // overwrite
- arithModel[v] = l;
- Trace("nl-model") << v << " exact approximation is " << l << std::endl;
+ // overwrite, ensure the type is correct
+ Assert(l.isConst());
+ Node ll = nm->mkConstRealOrInt(v.getType(), l.getConst<Rational>());
+ arithModel[v] = ll;
+ Trace("nl-model") << v << " exact approximation is " << ll << std::endl;
}
}
// Also record the exact values we used. An exact value can be seen as a
// is eliminated.
for (size_t i = 0; i < d_substitutions.size(); ++i)
{
- // overwrite
- arithModel[d_substitutions.d_vars[i]] = d_substitutions.d_subs[i];
- Trace("nl-model") << d_substitutions.d_vars[i] << " solved is "
- << d_substitutions.d_subs[i] << std::endl;
+ // overwrite, ensure the type is correct
+ Node v = d_substitutions.d_vars[i];
+ Node s = d_substitutions.d_subs[i];
+ Node ss = s;
+ // If its a rational constant, ensure it has the proper type now. It
+ // also may be a RAN, in which case v should be a real.
+ if (s.isConst())
+ {
+ ss = nm->mkConstRealOrInt(v.getType(), s.getConst<Rational>());
+ }
+ arithModel[v] = ss;
+ Trace("nl-model") << v << " solved is " << ss << std::endl;
}
// multiplication terms should not be given values; their values are
}
{
// must use real one/zero in equalities
- Node rzero = nm->mkConstReal(Rational(0));
+ Node rzero = mkZero(t[0].getType());
Node rone = nm->mkConstReal(Rational(1));
// exp at zero: (t = 0.0) <=> (exp(t) = 1.0)
Node lem =
Assert(children.empty());
Assert(args.size() == 1);
Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
- Node rzero = nm->mkConstReal(Rational(0));
+ Node rzero = nm->mkConstRealOrInt(args[0].getType(), Rational(0));
Node rone = nm->mkConstReal(Rational(1));
return nm->mkNode(EQUAL, args[0].eqNode(rzero), e.eqNode(rone));
}
rw, "nonlinearDiv", "the result of a non-linear div term");
Node lem = nm->mkNode(IMPLIES,
den.eqNode(mkZero(den.getType())).negate(),
- nm->mkNode(MULT, den, v).eqNode(num));
+ mkEquality(nm->mkNode(MULT, den, v), num));
lems.push_back(mkSkolemLemma(lem, v));
return v;
break;
Node skolem = getArithSkolem(id);
if (usePartialFunction(id))
{
- skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(skolem.getType().isFunction()
+ && skolem.getType().getNumChildren() == 2);
+ TypeNode argType = skolem.getType()[0];
+ if (!argType.isInteger() && n.getType().isInteger())
+ {
+ n = nm->mkNode(TO_REAL, n);
+ }
+ skolem = nm->mkNode(APPLY_UF, skolem, n);
}
return skolem;
}
Node pv,
CegInstEffort effort)
{
+ Assert(pv.getType() == d_type);
d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false);
d_vts_sym[1] = d_vtc->getVtsDelta(false, false);
for (unsigned i = 0; i < 2; i++)
int ires_use =
(msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
: -1;
- val = nm->mkNode(ires_use == -1 ? ADD : SUB,
+ val = nm->mkNode(TO_INTEGER, nm->mkNode(ires_use == -1 ? ADD : SUB,
nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart),
- nm->mkNode(TO_INTEGER, realPart));
+ nm->mkNode(TO_INTEGER, realPart)));
Trace("cegqi-arith-debug")
<< "result (pre-rewrite) : " << val << std::endl;
val = rewrite(val);
- val = val.getKind() == TO_REAL ? val[0] : val;
// 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];
+ if (!pv.getType().isInteger() && val.getType().isInteger())
+ {
+ val = nm->mkNode(TO_REAL, val);
+ }
+ Assert(pv.getType() == val.getType());
Trace("cegqi-arith-debug")
<< "Return " << veq_c << " * " << pv << " " << atom.getKind() << " "
<< val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")"
}
ret = d_env.getRewriter()->rewrite(ret);
Assert(ret.isConst());
+ Assert(ret.getType()==tn);
return ret;
}
}
Rational rr = r.getConst<Rational>();
if (rr.sgn() == 0)
{
- return s;
- }
- else
- {
- return nm->mkConstReal(sr / rr);
+ return nm->mkConstReal(s.getConst<Rational>());
}
+ return nm->mkConstReal(sr / rr);
}
}
// default: use type enumerator
void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
{
+ // don't check type equal here, since this utility may be used in conversions
+ // that change the types of terms
Trace("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
Assert(d_substitutions.find(x) == d_substitutions.end());
Sort real = slv.getRealSort();
Term x = slv.mkConst(real, "x");
- Term four = slv.mkInteger(4);
+ Term four = slv.mkReal(4);
Term xEqFour = slv.mkTerm(Kind::EQUAL, {x, four});
slv.assertFormula(xEqFour);
std::cout << slv.checkSat() << std::endl;
Sort indexType = slv.getIntegerSort();
Sort arrayType = slv.mkArraySort(indexType, elementType);
Term array = slv.mkConst(arrayType, "array");
- Term arrayAtFour = slv.mkTerm(Kind::SELECT, {array, four});
+ Term fourInt = slv.mkInteger(4);
+ Term arrayAtFour = slv.mkTerm(Kind::SELECT, {array, fourInt});
Term ten = slv.mkInteger(10);
Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, {arrayAtFour, ten});
slv.assertFormula(arrayAtFour_eq_ten);
real = slv.getRealSort()
x = slv.mkConst(real, "x")
-four = slv.mkInteger(4)
+four = slv.mkReal(4)
xEqFour = slv.mkTerm(Kind.EQUAL, x, four)
slv.assertFormula(xEqFour)
print(slv.checkSat())
indexType = slv.getIntegerSort()
arrayType = slv.mkArraySort(indexType, elementType)
array = slv.mkConst(arrayType, "array")
-arrayAtFour = slv.mkTerm(Kind.SELECT, array, four)
+fourInt = slv.mkInteger(4)
+arrayAtFour = slv.mkTerm(Kind.SELECT, array, fourInt)
ten = slv.mkInteger(10)
arrayAtFour_eq_ten = slv.mkTerm(Kind.EQUAL, arrayAtFour, ten)
slv.assertFormula(arrayAtFour_eq_ten)
regress0/datatypes/datatype2.cvc.smt2
regress0/datatypes/datatype3.cvc.smt2
regress0/datatypes/datatype4.cvc.smt2
+ regress0/datatypes/dd.pair-real-bool-const-conf.smt2
regress0/datatypes/dt-2.6.smt2
regress0/datatypes/dt-different-params.smt2
regress0/datatypes/dt-match-pat-param-2.6.smt2
--- /dev/null
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((P 0)) (((k (f Real)))))
+(declare-const r P)
+(assert (= 0.0 (f r)))
+(check-sat)
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
-(assert (and (>= x 0) (< y 7)))
-(get-abduct A (>= y 5))
+(assert (and (>= x 0.0) (< y 7.0)))
+(get-abduct A (>= y 5.0))
(set-info :status sat)
(declare-fun a () Real)
(declare-fun b (Real Real) Real)
-(assert (> (b a 0) (b (- a) 1)))
+(assert (> (b a 0.0) (b (- a) 1.0)))
(check-sat)
projects / cvc5.git / commitdiff