This is the key step for eliminating the use of subtyping.
This makes several changes:
(1) CONST_INTEGER is now used for integer constants, which is now exported in the API. The type rule for CONST_RATIONAL is changed to always return Real, even if its value is integral. This means we can distinguish real and integer versions of the integers. Note this also implies that the rewriter now fully preserves types, as rewriting TO_REAL applied to a constant integer will return a constant integral rational.
(2) The type rules for EQUAL, DISTINCT, ITE and APPLY_UF are made strict, in other words, we given a type exception for equalities between an Int and a Real. This restriction impacts the API.
(3) The arithmetic rewrite for (Real) equality casts integers to reals as needed to ensure Reals are only made equal to Reals. The net effect is that TO_REAL may appear on either side of equalities.
(4) The core arithmetic theory solver is modified in several places to be made robust to TO_REAL occurring as the top symbol of sides of equality.
Several assertions are strengthened or added to ensure that equalities and substitutions are between terms of the same type, when it is necessary to do so.
Two quantifiers regressions are modified since the solving techniques are not robust to TO_REAL. A few unit tests are fixed to use proper types.
- Removed support for non-standard `declare-funs`, `declare-consts`, and
`declare-sorts` commands.
+- The kind for integer constants is now `CONST_INTEGER`, while real constants
+ continue to have kind `CONST_RATIONAL`.
+- Type rules for (dis)equality and if-then-else no longer allow mixing
+ integers and reals. Type rules for other operators like `APPLY_UF` now
+ require their arguments to match the type of the function being applied, and
+ do not assume integer/real subtyping.
cvc5 1.0
KIND_ENUM(ARCCOTANGENT, internal::Kind::ARCCOTANGENT),
KIND_ENUM(SQRT, internal::Kind::SQRT),
KIND_ENUM(CONST_RATIONAL, internal::Kind::CONST_RATIONAL),
+ KIND_ENUM(CONST_INTEGER, internal::Kind::CONST_INTEGER),
KIND_ENUM(LT, internal::Kind::LT),
KIND_ENUM(LEQ, internal::Kind::LEQ),
KIND_ENUM(GT, internal::Kind::GT),
{internal::Kind::SQRT, SQRT},
{internal::Kind::DIVISIBLE_OP, DIVISIBLE},
{internal::Kind::CONST_RATIONAL, CONST_RATIONAL},
+ {internal::Kind::CONST_INTEGER, CONST_INTEGER},
{internal::Kind::LT, LT},
{internal::Kind::LEQ, LEQ},
{internal::Kind::GT, GT},
int32_t getRealOrIntegerValueSign() const;
/**
* @return True if the term is an integer value that fits within int32_t.
+ * Note that this method will return true for integer constants and real
+ * constants that have integer value.
*/
bool isInt32Value() const;
/**
- * Get the `int32_t` representation of this integer value.
+ * Get the `int32_t` representation of this integral value.
* @note Asserts isInt32Value().
* @return This integer value as a `int32_t`.
*/
int32_t getInt32Value() const;
/**
* @return True if the term is an integer value that fits within uint32_t.
+ * Note that this method will return true for integer constants and real
+ * constants that have integral value.
*/
bool isUInt32Value() const;
/**
- * Get the `uint32_t` representation of this integer value.
+ * Get the `uint32_t` representation of this integral value.
* @note Asserts isUInt32Value().
* @return This integer value as a `uint32_t`.
*/
uint32_t getUInt32Value() const;
/**
* @return True if the term is an integer value that fits within int64_t.
+ * Note that this method will return true for integer constants and real
+ * constants that have integral value.
*/
bool isInt64Value() const;
/**
- * Get the `int64_t` representation of this integer value.
+ * Get the `int64_t` representation of this integral value.
* @note Asserts isInt64Value().
* @return This integer value as a `int64_t`.
*/
int64_t getInt64Value() const;
/**
* @return True if the term is an integer value that fits within uint64_t.
+ * Note that this method will return true for integer constants and real
+ * constants that have integral value.
*/
bool isUInt64Value() const;
/**
- * Get the `uint64_t` representation of this integer value.
+ * Get the `uint64_t` representation of this integral value.
* @note Asserts isUInt64Value().
* @return This integer value as a `uint64_t`.
*/
uint64_t getUInt64Value() const;
/**
- * @return True if the term is an integer value.
+ * @return True if the term is an integer constant or a real constant that
+ * has an integral value.
*/
bool isIntegerValue() const;
/**
* @note Asserts isIntegerValue().
- * @return The integer term in (decimal) string representation.
+ * @return The integral term in (decimal) string representation.
*/
std::string getIntegerValue() const;
*/
DIVISIBLE,
/**
- * Multiple-precision rational constant.
+ * Arbitrary-precision rational constant.
*
* - Create Term of this Kind with:
*
- * - Solver::mkInteger(const std::string&) const
- * - Solver::mkInteger(int64_t) const
* - Solver::mkReal(const std::string&) const
* - Solver::mkReal(int64_t) const
* - Solver::mkReal(int64_t, int64_t) const
*/
CONST_RATIONAL,
+ /**
+ * Arbitrary-precision integer constant.
+ *
+ * - Create Term of this Kind with:
+ *
+ * - Solver::mkInteger(const std::string&) const
+ * - Solver::mkInteger(int64_t) const
+ */
+ CONST_INTEGER,
/**
* Less than, chainable.
*
template <>
${class} const& NodeValue::getConst< ${class} >() const {
- AssertArgument(getKind() == ::cvc5::internal::kind::$1, *this,
- \"Improper kind for getConst<${class}>()\");
+ //AssertArgument(getKind() == ::cvc5::internal::kind::$1, *this,
+ // \"Improper kind for getConst<${class}>()\");
// To support non-inlined CONSTANT-kinded NodeValues (those that are
// \"constructed\" when initially checking them against the NodeManager
// pool), we must check d_nchildren here.
Node NodeManager::mkConstInt(const Rational& r)
{
- // !!!! Note will update to CONST_INTEGER.
Assert(r.isIntegral());
- return mkConst(kind::CONST_RATIONAL, r);
+ return mkConst(kind::CONST_INTEGER, r);
}
Node NodeManager::mkConstRealOrInt(const Rational& r)
bool Smt2::isConstInt(const cvc5::Term& t)
{
- cvc5::Kind k = t.getKind();
- // !!! Note when arithmetic subtyping is eliminated, this will update to
- // CONST_INTEGER.
- return k == cvc5::CONST_RATIONAL && t.getSort().isInteger();
+ return t.getKind() == cvc5::CONST_INTEGER;
}
} // namespace parser
static void toStreamRational(std::ostream& out,
const Rational& r,
- bool decimal,
+ bool isReal,
Variant v)
{
bool neg = r.sgn() < 0;
- // Print the rational, possibly as decimal.
+ // Print the rational, possibly as a real.
// Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
// the former is compliant with real values in the smt lib standard.
if (r.isIntegral())
{
out << r;
}
- if (decimal)
+ if (isReal)
{
out << ".0";
}
}
else
{
+ Assert (isReal);
out << "(/ ";
if (neg)
{
out << smtKindString(n.getConst<Kind>(), d_variant);
break;
case kind::CONST_RATIONAL: {
+ const Rational& r = n.getConst<Rational>();
+ toStreamRational(out, r, true, d_variant);
+ break;
+ }
+ case kind::CONST_INTEGER:
+ {
const Rational& r = n.getConst<Rational>();
toStreamRational(out, r, false, d_variant);
break;
// the logic is mixed int/real. The former occurs more frequently.
bool is_int = force_nt.isInteger();
// If constant rational, print as special case
- if (type_asc_arg.getKind() == kind::CONST_RATIONAL)
+ Kind ka = type_asc_arg.getKind();
+ if (ka == kind::CONST_RATIONAL || ka == kind::CONST_INTEGER)
{
const Rational& r = type_asc_arg.getConst<Rational>();
toStreamRational(out, r, !is_int, d_variant);
Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
}
+ Assert(lhs.getType() == rhs.getType());
}
void PropEngine::assertInputFormulas(
}
// note that conversely this utility will never use a real value as
// the solution for an integer, thus the types should match now
+ Assert(val.getType() == vc.getType());
}
veq = nm->mkNode(k, inOrder ? vc : val, inOrder ? val : vc);
}
++(d_statistics.d_watchedVariables);
d_watchedVariables.add(s);
-
- Node eq = x.eqNode(y);
+ // must ensure types are correct, thus, add TO_REAL if necessary here
+ std::pair<Node, Node> p = mkSameType(x, y);
+ Node eq = p.first.eqNode(p.second);
d_watchedEqualities.set(s, eq);
}
Kind k = cmp.comparisonKind();
Polynomial pleft = cmp.normalizedVariablePart();
Assert(k == EQUAL || k == DISTINCT || pleft.leadingCoefficientIsPositive());
- Assert(k != EQUAL || Monomial::isMember(n[0]));
- Assert(k != DISTINCT || Monomial::isMember(n[0][0]));
+ Assert(k != EQUAL
+ || Monomial::isMember(n[0].getKind() == TO_REAL ? n[0][0] : n[0]));
+ Assert(k != DISTINCT
+ || Monomial::isMember(n[0][0].getKind() == TO_REAL ? n[0][0][0]
+ : n[0][0]));
TNode left = pleft.getNode();
DeltaRational right = cmp.normalizedDeltaRational();
switch(k){
case kind::LT:
case kind::LEQ:
+ left = getNode()[0][0];
+ Assert(left.getKind() != kind::TO_REAL);
+ break;
case kind::DISTINCT:
left = getNode()[0][0];
+ left = left.getKind() == kind::TO_REAL ? left[0] : left;
break;
case kind::EQUAL:
+ left = getNode()[0];
+ left = left.getKind() == kind::TO_REAL ? left[0] : left;
+ break;
case kind::GT:
case kind::GEQ:
left = getNode()[0];
+ Assert(left.getKind() != kind::TO_REAL);
break;
default: Unhandled() << k;
}
switch(k){
case kind::LT:
case kind::LEQ:
+ right = getNode()[0][1];
+ Assert(right.getKind() != kind::TO_REAL);
+ break;
case kind::DISTINCT:
right = getNode()[0][1];
+ right = right.getKind() == kind::TO_REAL ? right[0] : right;
break;
case kind::EQUAL:
+ right = getNode()[1];
+ right = right.getKind() == kind::TO_REAL ? right[0] : right;
+ break;
case kind::GT:
case kind::GEQ:
right = getNode()[1];
+ Assert(right.getKind() != kind::TO_REAL);
break;
default: Unhandled() << k;
}
}
Trace("nl-ext-mv-debug") << "computed " << (isConcrete ? "M" : "M_A") << "["
<< n << "] = " << ret << std::endl;
+ Assert(n.getType() == ret.getType());
cache[n] = ret;
return ret;
}
Trace("arith-rewriter::debug")
<< "\tbuilding " << left << " = " << sum << std::endl;
- return buildRelation(Kind::EQUAL, left, collectSum(sum));
+ Node rhs = collectSum(sum);
+ Assert(left.getType().isInteger());
+ Assert(rhs.getType().isInteger());
+ return buildRelation(Kind::EQUAL, left, rhs);
}
Node buildRealEquality(Sum&& sum)
{
s.second = s.second / lcoeff;
}
- return buildRelation(Kind::EQUAL, lterm.first, collectSum(sum));
+ // Must ensure real for both sides. This may change one but not both
+ // terms.
+ Node lhs = lterm.first;
+ lhs = ensureReal(lhs);
+ Node rhs = collectSum(sum);
+ rhs = ensureReal(rhs);
+ Assert(lhs.getType().isReal() && !lhs.getType().isInteger());
+ Assert(rhs.getType().isReal() && !rhs.getType().isInteger());
+ return buildRelation(Kind::EQUAL, lhs, rhs);
}
Node buildIntegerInequality(Sum&& sum, Kind k)
{
continue;
}
- // maps to constant of comparable type
- Assert(p.first.getType().isComparableTo(p.second.getType()));
+ // maps to constant of same type
+ Assert(p.first.getType() == p.second.getType());
if (m->assertEquality(p.first, p.second, true))
{
continue;
{
for (CVC5_UNUSED const auto& p : d_arithModelCache)
{
- // will change to strict type equal
- Assert(p.second.getType().isSubtypeOf(p.second.getType()));
+ Assert(p.first.getType() == p.second.getType());
}
}
bool addedLemma = false;
TNode n,
bool check)
{
- Assert(n.getKind() == kind::CONST_RATIONAL);
- if (n.getConst<Rational>().isIntegral())
+ // we use different kinds for constant integers and reals
+ if (n.getKind() == kind::CONST_RATIONAL)
{
- return nodeManager->integerType();
+ // constant rationals are always real type, even if their value is integral
+ return nodeManager->realType();
}
- return nodeManager->realType();
+ Assert(n.getKind() == kind::CONST_INTEGER);
+ // constant integers should always have integral value
+ if (check)
+ {
+ if (!n.getConst<Rational>().isIntegral())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "making an integer constant from a non-integral rational");
+ }
+ }
+ return nodeManager->integerType();
}
TypeNode ArithRealAlgebraicNumberOpTypeRule::computeType(
TypeNode IteTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
{
TypeNode thenType = n[1].getType(check);
- TypeNode elseType = n[2].getType(check);
- TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
if (check)
{
- TypeNode booleanType = nodeManager->booleanType();
- if (n[0].getType(check) != booleanType)
- {
- throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
- }
- if (iteType.isNull())
+ TypeNode elseType = n[2].getType(check);
+ if (thenType != elseType)
{
std::stringstream ss;
- ss << "Both branches of the ITE must be a subtype of a common type."
- << std::endl
+ ss << "Branches of the ITE must have the same type." << std::endl
<< "then branch: " << n[1] << std::endl
<< "its type : " << thenType << std::endl
<< "else branch: " << n[2] << std::endl
<< "its type : " << elseType << std::endl;
throw TypeCheckingExceptionPrivate(n, ss.str());
}
+ if (!n[0].getType(check).isBoolean())
+ {
+ throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
+ }
}
- return iteType;
+ return thenType;
}
} // namespace boolean
TypeNode lhsType = n[0].getType(check);
TypeNode rhsType = n[1].getType(check);
- if (TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull())
+ if (lhsType != rhsType)
{
std::stringstream ss;
- ss << "Subexpressions must have a common base type:" << std::endl;
+ ss << "Subexpressions must have the same type:" << std::endl;
ss << "Equation: " << n << std::endl;
ss << "Type 1: " << lhsType << std::endl;
ss << "Type 2: " << rhsType << std::endl;
throw TypeCheckingExceptionPrivate(n, ss.str());
}
- // TODO : check isFirstClass for these types? (github issue #1202)
}
return booleanType;
}
for (++child_it; child_it != child_it_end; ++child_it)
{
TypeNode currentType = (*child_it).getType();
- joinType = TypeNode::leastCommonTypeNode(joinType, currentType);
- if (joinType.isNull())
+ if (joinType != currentType)
{
throw TypeCheckingExceptionPrivate(
n, "Not all arguments are of the same type");
opn = getExpandedDefinitionForm(op);
}
}
- return mkSygusTerm(opn, children, doBetaReduction);
+ Node ret = mkSygusTerm(opn, children, doBetaReduction);
+ Assert(ret.getType() == dt.getSygusType());
+ return ret;
}
Node mkSygusTerm(Node op,
// push the substitution pv_prop.getModifiedTerm(pv) -> n
void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
{
- Assert(n.getType().isSubtypeOf(pv.getType()));
+ Assert(n.getType() == pv.getType());
d_vars.push_back(pv);
d_subs.push_back(n);
d_props.push_back(pv_prop);
SolvedForm& sf,
bool revertOnSuccess)
{
- Assert(n.getType().isSubtypeOf(pv.getType()));
+ Assert(n.getType() == pv.getType());
Node cnode = pv_prop.getCacheNode();
if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
d_curr_subs_proc[pv][n][cnode] = true;
<< ") ";
Node mod_pv = pv_prop.getModifiedTerm( pv );
Trace("cegqi-inst-debug") << mod_pv << " -> " << n << std::endl;
- Assert(n.getType().isSubtypeOf(pv.getType()));
+ Assert(n.getType() == pv.getType());
}
//must ensure variables have been computed for n
computeProgVars( n );
doCheck( fm, f, d, n[0] );
doNegate( d );
}
- else if (n.getKind() == kind::TO_REAL)
- {
- // no-op
- doCheck(fm, f, d, n[0]);
- }
else if( n.getKind() == kind::FORALL ){
d.addEntry(fm, mkCondDefault(fm, f), Node::null());
}
return true;
}
-Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
+Node FullModelChecker::mkCond(const std::vector<Node>& cond)
+{
return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
}
std::vector< Node > & cond, std::vector<Node> & val );
int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
- Node mkCond( std::vector< Node > & cond );
+ Node mkCond(const std::vector<Node>& cond);
Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
void mkCondVec( Node n, std::vector< Node > & cond );
TypeNode ct = dt[i].getArgType(j);
TypeNode cbt = tds->sygusToBuiltinType(ct);
TypeNode lat = sop[0][j].getType();
- AlwaysAssert(cbt.isSubtypeOf(lat))
+ AlwaysAssert(cbt == lat)
<< "In sygus datatype " << dt.getName()
<< ", argument to a lambda constructor is not " << lat << std::endl;
}
TheoryId newTheory = theoryOf(newNode);
rewriteStackTop.d_node = newNode;
rewriteStackTop.d_theoryId = newTheory;
- Assert(
- newNode.getType().isSubtypeOf(rewriteStackTop.d_node.getType()))
- << "Pre-rewriting " << rewriteStackTop.d_node
+ Assert(newNode.getType() == rewriteStackTop.d_node.getType())
+ << "Pre-rewriting " << rewriteStackTop.d_node << " to " << newNode
<< " does not preserve type";
// In the pre-rewrite, if changing theories, we just call the other
// theories pre-rewrite. If the kind of the node was changed, then we
// We continue with the response we got
TNode newNode = response.d_node;
TheoryId newTheoryId = theoryOf(newNode);
- Assert(newNode.getType().isSubtypeOf(rewriteStackTop.d_node.getType()))
- << "Post-rewriting " << rewriteStackTop.d_node
+ Assert(newNode.getType() == rewriteStackTop.d_node.getType())
+ << "Post-rewriting " << rewriteStackTop.d_node << " to " << newNode
<< " does not preserve type";
if (newTheoryId != rewriteStackTop.getTheoryId()
|| response.d_status == REWRITE_AGAIN_FULL)
if (rewriteStack.size() == 1) {
Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL
|| rewriteStackTop.d_node.isConst());
- Assert(rewriteStackTop.d_node.getType().isSubtypeOf(node.getType()))
- << "Rewriting " << node << " does not preserve type";
+ Assert(rewriteStackTop.d_node.getType() == node.getType())
+ << "Rewriting " << node << " to " << rewriteStackTop.d_node
+ << " does not preserve type";
return rewriteStackTop.d_node;
}
const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
-theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
- Assert(a.getType().isComparableTo(b.getType()));
+theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b)
+{
+ Assert(a.getType() == b.getType());
return d_sharedSolver->getEqualityStatus(a, b);
}
}
Trace("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
<< "[model-getvalue] returning " << nn << std::endl;
- Assert(nn.getType().isSubtypeOf(n.getType()));
+ Assert(nn.getType() == n.getType());
return nn;
}
{
TypeNode currentArgument = (*argument_it).getType();
TypeNode currentArgumentType = *argument_type_it;
- if (!currentArgument.isSubtypeOf(currentArgumentType))
+ if (currentArgument != currentArgumentType)
{
std::stringstream ss;
ss << "argument type is not a subtype of the function's argument "
(declare-const x Bool)
(declare-fun v () Int)
(declare-fun r () Int)
-(assert (forall ((a Int)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
-(check-sat)
\ No newline at end of file
+(assert (forall ((a Int)) (= (< v r) (= (= 0.0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
(declare-const x Bool)
(declare-fun v () Real)
(declare-fun r () Real)
-(assert (forall ((a Real)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
-(check-sat)
\ No newline at end of file
+(assert (forall ((a Real)) (= (< v r) (= (= 0.0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
(declare-const x Bool)
(declare-fun v () Real)
(declare-fun r () Real)
-(assert (forall ((a Real)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
-(check-sat)
\ No newline at end of file
+(assert (forall ((a Real)) (= (< v r) (= (= 0.0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
+; COMMAND-LINE: -q
+; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-const x Bool)
-; COMMAND-LINE: --fmf-bound --no-cegqi
; EXPECT: sat
(set-logic ALL)
(assert (forall ((a Int)) (or (distinct (/ 0 0) (to_real a)) (= (/ 0 a) 0.0))))
; COMMAND-LINE: --finite-model-find --sort-inference
-; EXPECT: sat
+; EXPECT: unknown
(set-logic UFLIRA)
(set-info :status sat)
(declare-fun f (Int) Int)
(assert (= (to_real (f 4)) (g 8)))
(assert (= (to_real (h 5.0)) 0.0))
; Sort inference fails to infer that x can be uninterpreted in this example,
-; however, fmf is able to reason that all instances are sat.
+; fmf is unable to show sat due to use of to_real.
(check-sat)
-; COMMAND-LINE: --nl-ext=full
+; COMMAND-LINE: --nl-ext=full -q
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
Term heap = solver->mkTerm(cvc5::Kind::SEP_PTO, {p, x});
solver->assertFormula(heap);
Term nil = solver->mkSepNil(integer);
- solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
+ solver->assertFormula(nil.eqTerm(solver->mkInteger(5)));
solver->checkSat();
}
} // namespace
Term heap = solver.mkTerm(SEP_PTO, p, x);
solver.assertFormula(heap);
Term nil = solver.mkSepNil(integer);
- solver.assertFormula(nil.eqTerm(solver.mkReal(5)));
+ solver.assertFormula(nil.eqTerm(solver.mkInteger(5)));
solver.checkSat();
}
heap = slv.mkTerm(Kind.SEP_PTO, p, x)
slv.assertFormula(heap)
nil = slv.mkSepNil(integer)
- slv.assertFormula(nil.eqTerm(slv.mkReal(5)))
+ slv.assertFormula(nil.eqTerm(slv.mkInteger(5)))
slv.checkSat()
{
Node x = d_nodeManager->mkVar(*d_intType);
Node xr = d_nodeManager->mkVar(*d_realType);
- Node c0 = d_nodeManager->mkConstReal(d_zero);
- Node c1 = d_nodeManager->mkConstReal(d_one);
- Node c2 = d_nodeManager->mkConstReal(Rational(2));
+ Node c0 = d_nodeManager->mkConstInt(d_zero);
+ Node c1 = d_nodeManager->mkConstInt(d_one);
+ Node c2 = d_nodeManager->mkConstInt(Rational(2));
Node geq0 = d_nodeManager->mkNode(GEQ, x, c0);
Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
projects / cvc5.git / commitdiff