From: Andrew Reynolds Date: Thu, 12 May 2022 17:48:27 +0000 (-0500) Subject: Preserve types in rewriter and make core type rules strict (#8740) X-Git-Tag: cvc5-1.0.1~143 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2f5753469c7404a2893ce72425ada6b842915a5;p=cvc5.git Preserve types in rewriter and make core type rules strict (#8740) 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. --- diff --git a/NEWS.md b/NEWS.md index 98fc47dcb..b9b13ae83 100644 --- a/NEWS.md +++ b/NEWS.md @@ -7,6 +7,12 @@ cvc5 1.0.1 - 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 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index e0999dbff..29208c2cd 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -168,6 +168,7 @@ const static std::unordered_map> 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), @@ -465,6 +466,7 @@ const static std::unordered_map ${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. diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 419cf5055..6259971cc 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1337,9 +1337,8 @@ Node NodeManager::mkConstReal(const Rational& r) 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) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index dad36788e..cf28d0ac8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1342,10 +1342,7 @@ cvc5::Term Smt2::mkAnd(const std::vector& es) const 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 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 3cda30e18..8f879916f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -66,11 +66,11 @@ namespace smt2 { 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()) @@ -83,7 +83,7 @@ static void toStreamRational(std::ostream& out, { out << r; } - if (decimal) + if (isReal) { out << ".0"; } @@ -94,6 +94,7 @@ static void toStreamRational(std::ostream& out, } else { + Assert (isReal); out << "(/ "; if (neg) { @@ -243,6 +244,12 @@ void Smt2Printer::toStream(std::ostream& out, out << smtKindString(n.getConst(), d_variant); break; case kind::CONST_RATIONAL: { + const Rational& r = n.getConst(); + toStreamRational(out, r, true, d_variant); + break; + } + case kind::CONST_INTEGER: + { const Rational& r = n.getConst(); toStreamRational(out, r, false, d_variant); break; @@ -509,7 +516,8 @@ void Smt2Printer::toStream(std::ostream& out, // 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(); toStreamRational(out, r, !is_int, d_variant); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fdbcf9667..4ee596f6f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -175,6 +175,7 @@ void PropEngine::notifyTopLevelSubstitution(const Node& lhs, Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs)); output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl; } + Assert(lhs.getType() == rhs.getType()); } void PropEngine::assertInputFormulas( diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index c3b18ac6b..354982350 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -242,6 +242,7 @@ int ArithMSum::isolate( } // 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); } diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp index 8ab23f79c..bcceb37d0 100644 --- a/src/theory/arith/linear/congruence_manager.cpp +++ b/src/theory/arith/linear/congruence_manager.cpp @@ -444,8 +444,9 @@ void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){ ++(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 p = mkSameType(x, y); + Node eq = p.first.eqNode(p.second); d_watchedEqualities.set(s, eq); } diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp index 628750973..71daeed58 100644 --- a/src/theory/arith/linear/constraint.cpp +++ b/src/theory/arith/linear/constraint.cpp @@ -658,8 +658,11 @@ bool Constraint::sanityChecking(Node n) const { 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(); diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp index 100223596..41d6db897 100644 --- a/src/theory/arith/linear/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -961,13 +961,21 @@ Polynomial Comparison::getLeft() const { 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; } @@ -980,13 +988,21 @@ Polynomial Comparison::getRight() const { 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; } diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 4add4e798..55f327b3a 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -126,6 +126,7 @@ Node NlModel::computeModelValue(TNode n, bool isConcrete) } Trace("nl-ext-mv-debug") << "computed " << (isConcrete ? "M" : "M_A") << "[" << n << "] = " << ret << std::endl; + Assert(n.getType() == ret.getType()); cache[n] = ret; return ret; } diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp index f12124a4e..ebd94c16b 100644 --- a/src/theory/arith/rewriter/rewrite_atom.cpp +++ b/src/theory/arith/rewriter/rewrite_atom.cpp @@ -297,7 +297,10 @@ Node buildIntegerEquality(Sum&& sum) 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) @@ -313,7 +316,15 @@ 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) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4e8e1a409..bd1a04dfd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -293,8 +293,8 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { 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; @@ -395,8 +395,7 @@ bool TheoryArith::sanityCheckIntegerModel() { 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; diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index 31dede3a9..b709e2d6a 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -25,12 +25,23 @@ TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::CONST_RATIONAL); - if (n.getConst().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().isIntegral()) + { + throw TypeCheckingExceptionPrivate( + n, "making an integer constant from a non-integral rational"); + } + } + return nodeManager->integerType(); } TypeNode ArithRealAlgebraicNumberOpTypeRule::computeType( diff --git a/src/theory/booleans/theory_bool_type_rules.cpp b/src/theory/booleans/theory_bool_type_rules.cpp index 65b69a91f..43a3b9c06 100644 --- a/src/theory/booleans/theory_bool_type_rules.cpp +++ b/src/theory/booleans/theory_bool_type_rules.cpp @@ -47,28 +47,25 @@ TypeNode BooleanTypeRule::computeType(NodeManager* nodeManager, 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 diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index b7698b23e..cd3c1250d 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -34,17 +34,16 @@ TypeNode EqualityTypeRule::computeType(NodeManager* nodeManager, 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; } @@ -61,8 +60,7 @@ TypeNode DistinctTypeRule::computeType(NodeManager* nodeManager, 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"); diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 6b833cb81..ca5c4419c 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -170,7 +170,9 @@ Node mkSygusTerm(const DType& dt, 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, diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 5320638be..8ef7f3d6f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -146,7 +146,7 @@ void TermProperties::composeProperty(TermProperties& p) // 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); @@ -945,7 +945,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, 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; @@ -957,7 +957,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv, << ") "; 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 ); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 0304043e9..6a419f08e 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -954,11 +954,6 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node 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()); } @@ -1306,7 +1301,8 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co return true; } -Node FullModelChecker::mkCond( std::vector< Node > & cond ) { +Node FullModelChecker::mkCond(const std::vector& cond) +{ return NodeManager::currentNM()->mkNode(APPLY_UF, cond); } diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 973dd0724..c4d08505f 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -147,7 +147,7 @@ protected: std::vector< Node > & cond, std::vector & 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& 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 ); diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 4f5ec9cbd..9d2f276f3 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -122,7 +122,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) 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; } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index bf74c0281..2b2ef939d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -219,9 +219,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, 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 @@ -310,8 +309,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, // 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) @@ -403,8 +402,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, 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; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 55a15e2ab..fed582cc5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1077,8 +1077,9 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { 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); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6465743c1..52c78151c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -155,7 +155,7 @@ Node TheoryModel::getValue(TNode n) const } 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; } diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 31ecde0a1..84a54025f 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -50,7 +50,7 @@ TypeNode UfTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { 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 " diff --git a/test/regress/cli/regress0/nl/issue8744-int.smt2 b/test/regress/cli/regress0/nl/issue8744-int.smt2 index 80e9009e9..ddee6a569 100644 --- a/test/regress/cli/regress0/nl/issue8744-int.smt2 +++ b/test/regress/cli/regress0/nl/issue8744-int.smt2 @@ -4,5 +4,5 @@ (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) diff --git a/test/regress/cli/regress0/nl/issue8744-real-cov.smt2 b/test/regress/cli/regress0/nl/issue8744-real-cov.smt2 index 16d3f8b70..5da4054ce 100644 --- a/test/regress/cli/regress0/nl/issue8744-real-cov.smt2 +++ b/test/regress/cli/regress0/nl/issue8744-real-cov.smt2 @@ -5,5 +5,5 @@ (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) diff --git a/test/regress/cli/regress0/nl/issue8744-real.smt2 b/test/regress/cli/regress0/nl/issue8744-real.smt2 index 3c3fee924..32ec9c7d2 100644 --- a/test/regress/cli/regress0/nl/issue8744-real.smt2 +++ b/test/regress/cli/regress0/nl/issue8744-real.smt2 @@ -4,5 +4,5 @@ (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) diff --git a/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2 b/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2 index 20f0a6190..fff6365b0 100644 --- a/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue8147-unc-model.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-const x Bool) diff --git a/test/regress/cli/regress1/fmf/issue3626.smt2 b/test/regress/cli/regress1/fmf/issue3626.smt2 index 5e2c3a468..99dc2022d 100644 --- a/test/regress/cli/regress1/fmf/issue3626.smt2 +++ b/test/regress/cli/regress1/fmf/issue3626.smt2 @@ -1,4 +1,3 @@ -; 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)))) diff --git a/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2 b/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2 index 5f908db6e..e6e8fc974 100644 --- a/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2 +++ b/test/regress/cli/regress1/fmf/sort-inf-int-real.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --finite-model-find --sort-inference -; EXPECT: sat +; EXPECT: unknown (set-logic UFLIRA) (set-info :status sat) (declare-fun f (Int) Int) @@ -11,5 +11,5 @@ (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) diff --git a/test/regress/cli/regress1/nl/bad-050217.smt2 b/test/regress/cli/regress1/nl/bad-050217.smt2 index 4f3cf8951..3bc0df2cf 100644 --- a/test/regress/cli/regress1/nl/bad-050217.smt2 +++ b/test/regress/cli/regress1/nl/bad-050217.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext=full +; COMMAND-LINE: --nl-ext=full -q ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index b8d05446d..da4bef952 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2128,7 +2128,7 @@ void checkSimpleSeparationConstraints(Solver* solver) 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 diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 7b2de58f4..e70e43d0c 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2133,7 +2133,7 @@ class SolverTest 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(); } diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index cb7340495..a8021ff47 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1587,7 +1587,7 @@ def checkSimpleSeparationConstraints(slv): 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() diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index d9c8abbb7..9c5775790 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -83,9 +83,9 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) { 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);