From: Andrew Reynolds Date: Sat, 7 May 2022 14:33:17 +0000 (-0500) Subject: Do not rely on subtyping in real-to-int preprocessing pass (#8732) X-Git-Tag: cvc5-1.0.1~155 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41c8937c0de8babd8dd5167880292090ac2d8967;p=cvc5.git Do not rely on subtyping in real-to-int preprocessing pass (#8732) --- diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 44bb709db..89368589e 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -151,9 +151,20 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va { bool childChanged = false; std::vector children; - for (unsigned i = 0; i < n.getNumChildren(); i++) + Kind k = n.getKind(); + // we change Real equalities to Int equalities + bool preserveTypes = k != EQUAL && (kindToTheoryId(k) != THEORY_ARITH); + for (size_t i = 0; i < n.getNumChildren(); i++) { Node nc = realToIntInternal(n[i], cache, var_eq); + // must preserve types if we don't belong to arithmetic, cast back + if (preserveTypes) + { + if (!n[i].getType().isInteger() && nc.getType().isInteger()) + { + nc = nm->mkNode(TO_REAL, nc); + } + } childChanged = childChanged || nc != n[i]; children.push_back(nc); } @@ -163,7 +174,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va { children.insert(children.begin(), n.getOperator()); } - ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + ret = nm->mkNode(k, children); } } } @@ -185,11 +196,15 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va { Node toIntN = nm->mkNode(kind::TO_INTEGER, n); ret = sm->mkPurifySkolem(toIntN, "__realToIntInternal_var"); - var_eq.push_back(n.eqNode(ret)); + Node retToReal = nm->mkNode(kind::TO_REAL, ret); + var_eq.push_back(n.eqNode(retToReal)); // add the substitution to the preprocessing context, which ensures // the model for n is correct, as well as substituting it in the input // assertions when necessary. - d_preprocContext->addSubstitution(n, ret); + // The model value for the Real variable n we are eliminating is + // (to_real k), where k is the Int skolem whose unpurified form is + // (to_int n). + d_preprocContext->addSubstitution(n, retToReal); } } }