From: Andrew Reynolds Date: Fri, 29 Apr 2022 19:35:04 +0000 (-0500) Subject: Towards proper usage of TO_REAL (#8680) X-Git-Tag: cvc5-1.0.1~197 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=06105f6ccf1cb73fd8e3335c855177c1fcdcd800;p=cvc5.git Towards proper usage of TO_REAL (#8680) This is work towards making the rewriter preserve types, which is work towards eliminating subtyping. This makes it so that the arithmetic rewriter does not simply drop TO_REAL from all terms, as this may change the type of the Node. Instead, TO_REAL is pulled upwards, and can be removed beneath arithmetic relations. TO_REAL is not eliminated if it occurs as a child of an operator not belonging to arithmetic. For example if x,y : Int: (= (+ (to_real x) y) 0.0) ---> (= (to_real (+ x y)) 0.0) ---> (= (+ x y) 0.0) ; note this is the same rewritten form as before (P (+ (to_real x) y)) ---> (P (to_real (+ x y))). The one exception is that to_real applied to constants is simply dropped (for now), for example: (to_real 5) ---> 5 where above, a Real term is rewritten to an Int term. (Fixing this will require further PRs that make integer constants of kind CONST_INTEGER and integral CONST_RATIONAL have Real type, thus we can have the above rewrite return 5 that is constant and has type Real). Several quantifiers utilities are patched to preserve their behavior wrt handling TO_REAL. Finally, a few fixes for subtypes are made to the regressions that we were not catching as errors before, and adds one regression. The net effect of this PR is that the rewritten form of terms may have to_real applications that occur as direct children of symbols from other theories. Special care is required for preregistration, shared terms, and getting model values in the linear solver to strip off TO_REAL if necessary before using the (unmodified) interface to the linear solver. FYI @barrettcw --- diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index b32d488a2..128b2e84c 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -81,12 +81,18 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom) { Assert(rewriter::isAtom(atom)); - if (auto response = rewriter::tryEvaluateRelationReflexive(atom); response) + Kind kind = atom.getKind(); + if (atom.getNumChildren() == 2) { - return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response)); + if (auto response = + rewriter::tryEvaluateRelationReflexive(kind, atom[0], atom[1]); + response) + { + return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response)); + } } - switch (atom.getKind()) + switch (kind) { case Kind::GT: return RewriteResponse( @@ -144,16 +150,17 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom) nm->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], rewriter::mkConst(k)), rewriter::mkConst(Integer(0)))); } + // left |><| right + Kind kind = atom.getKind(); + Node left = removeToReal(atom[0]); + Node right = removeToReal(atom[1]); - if (auto response = rewriter::tryEvaluateRelationReflexive(atom); response) + if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right); + response) { return RewriteResponse(REWRITE_DONE, rewriter::mkConst(*response)); } - // left |><| right - Kind kind = atom.getKind(); - TNode left = atom[0]; - TNode right = atom[1]; Assert(isRelationOperator(kind)); if (auto response = rewriter::tryEvaluateRelation(kind, left, right); @@ -241,10 +248,10 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true); case kind::ABS: return rewriteAbs(t); case kind::IS_INTEGER: - case kind::TO_INTEGER: return RewriteResponse(REWRITE_DONE, t); + case kind::TO_INTEGER: case kind::TO_REAL: - case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); - case kind::POW: return RewriteResponse(REWRITE_DONE, t); + case kind::CAST_TO_REAL: + case kind::POW: case kind::PI: return RewriteResponse(REWRITE_DONE, t); default: Unhandled() << k; } @@ -291,7 +298,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false); case kind::ABS: return rewriteAbs(t); case kind::TO_REAL: - case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); + case kind::CAST_TO_REAL: return rewriteToReal(t); case kind::TO_INTEGER: return rewriteExtIntegerOp(t); case kind::POW: { @@ -350,6 +357,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ RewriteResponse ArithRewriter::rewriteRAN(TNode t) { Assert(rewriter::isRAN(t)); + Assert(t.getType().isReal()); const RealAlgebraicNumber& r = rewriter::getRAN(t); if (r.isRational()) { @@ -369,10 +377,12 @@ RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre) { Assert(t.getKind() == kind::NEG); + NodeManager* nm = NodeManager::currentNM(); if (t[0].isConst()) { Rational neg = -(t[0].getConst()); - return RewriteResponse(REWRITE_DONE, rewriter::mkConst(neg)); + return RewriteResponse(REWRITE_DONE, + nm->mkConstRealOrInt(t.getType(), neg)); } if (rewriter::isRAN(t[0])) { @@ -380,8 +390,7 @@ RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre) rewriter::mkConst(-rewriter::getRAN(t[0]))); } - auto* nm = NodeManager::currentNM(); - Node noUminus = nm->mkNode(kind::MULT, rewriter::mkConst(Integer(-1)), t[0]); + Node noUminus = nm->mkNode(kind::MULT, rewriter::mkConst(Rational(-1)), t[0]); if (pre) { return RewriteResponse(REWRITE_DONE, noUminus); @@ -397,16 +406,19 @@ RewriteResponse ArithRewriter::rewriteSub(TNode t) Assert(t.getKind() == kind::SUB); Assert(t.getNumChildren() == 2); + NodeManager* nm = NodeManager::currentNM(); if (t[0] == t[1]) { - return RewriteResponse(REWRITE_DONE, rewriter::mkConst(Integer(0))); + return RewriteResponse(REWRITE_DONE, + nm->mkConstRealOrInt(t.getType(), Rational(0))); } - auto* nm = NodeManager::currentNM(); return RewriteResponse( REWRITE_AGAIN_FULL, nm->mkNode(Kind::ADD, t[0], - nm->mkNode(kind::MULT, rewriter::mkConst(Integer(-1)), t[1]))); + nm->mkNode(kind::MULT, + nm->mkConstRealOrInt(t[1].getType(), Rational(-1)), + t[1]))); } RewriteResponse ArithRewriter::preRewritePlus(TNode t) @@ -426,9 +438,11 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t) rewriter::Sum sum; for (const auto& child : children) { - rewriter::addToSum(sum, child); + rewriter::addToSum(sum, removeToReal(child)); } - return RewriteResponse(REWRITE_DONE, rewriter::collectSum(sum)); + Node retSum = rewriter::collectSum(sum); + retSum = maybeEnsureReal(t.getType(), retSum); + return RewriteResponse(REWRITE_DONE, retSum); } RewriteResponse ArithRewriter::preRewriteMult(TNode node) @@ -438,7 +452,7 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode node) if (auto res = rewriter::getZeroChild(node); res) { - return RewriteResponse(REWRITE_DONE, *res); + return RewriteResponse(REWRITE_DONE, maybeEnsureReal(node.getType(), *res)); } return RewriteResponse(REWRITE_DONE, node); } @@ -452,43 +466,52 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ if (auto res = rewriter::getZeroChild(children); res) { - return RewriteResponse(REWRITE_DONE, *res); + return RewriteResponse(REWRITE_DONE, maybeEnsureReal(t.getType(), *res)); } + // remove TO_REAL + for (TNode& tc : children) + { + tc = removeToReal(tc); + } + + Node ret; // Distribute over addition if (std::any_of(children.begin(), children.end(), [](TNode child) { return child.getKind() == Kind::ADD; })) { - return RewriteResponse(REWRITE_DONE, - rewriter::distributeMultiplication(children)); + ret = rewriter::distributeMultiplication(children); } - - RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1)); - std::vector leafs; - - for (const auto& child : children) + else { - if (child.isConst()) + RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1)); + std::vector leafs; + + for (const auto& child : children) { - if (child.getConst().isZero()) + if (child.isConst()) { - return RewriteResponse(REWRITE_DONE, child); + if (child.getConst().isZero()) + { + return RewriteResponse(REWRITE_DONE, + maybeEnsureReal(t.getType(), child)); + } + ran *= child.getConst(); + } + else if (rewriter::isRAN(child)) + { + ran *= rewriter::getRAN(child); + } + else + { + leafs.emplace_back(child); } - ran *= child.getConst(); - } - else if (rewriter::isRAN(child)) - { - ran *= rewriter::getRAN(child); - } - else - { - leafs.emplace_back(child); } + ret = rewriter::mkMultTerm(ran, std::move(leafs)); } - - return RewriteResponse(REWRITE_DONE, - rewriter::mkMultTerm(ran, std::move(leafs))); + ret = maybeEnsureReal(t.getType(), ret); + return RewriteResponse(REWRITE_DONE, ret); } RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) @@ -496,22 +519,22 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION); Assert(t.getNumChildren() == 2); - Node left = t[0]; - Node right = t[1]; + Node left = removeToReal(t[0]); + Node right = removeToReal(t[1]); + NodeManager* nm = NodeManager::currentNM(); if (right.isConst()) { - NodeManager* nm = NodeManager::currentNM(); const Rational& den = right.getConst(); if (den.isZero()) { if (t.getKind() == kind::DIVISION_TOTAL) { - return RewriteResponse(REWRITE_DONE, nm->mkConstReal(0)); + Node ret = nm->mkConstReal(0); + return RewriteResponse(REWRITE_DONE, ret); } else { - // This is unsupported, but this is not a good place to complain return RewriteResponse(REWRITE_DONE, t); } } @@ -530,42 +553,68 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) } Node result = nm->mkConstReal(den.inverse()); - Node mult = NodeManager::currentNM()->mkNode(kind::MULT, left, result); + Node mult = + ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result)); if (pre) { return RewriteResponse(REWRITE_DONE, mult); } - else - { - return RewriteResponse(REWRITE_AGAIN, mult); - } + // requires again full since ensureReal may have added a to_real + return RewriteResponse(REWRITE_AGAIN_FULL, mult); } if (rewriter::isRAN(right)) { const RealAlgebraicNumber& den = rewriter::getRAN(right); - + // mkConst is applied to RAN in this block, which are always Real if (left.isConst()) { return RewriteResponse( - REWRITE_DONE, rewriter::mkConst(left.getConst() / den)); + REWRITE_DONE, + ensureReal(rewriter::mkConst(left.getConst() / den))); } if (rewriter::isRAN(left)) { - return RewriteResponse(REWRITE_DONE, - rewriter::mkConst(rewriter::getRAN(left) / den)); + return RewriteResponse( + REWRITE_DONE, + ensureReal(rewriter::mkConst(rewriter::getRAN(left) / den))); } Node result = rewriter::mkConst(inverse(den)); - Node mult = NodeManager::currentNM()->mkNode(kind::MULT, left, result); + Node mult = + ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result)); if (pre) { return RewriteResponse(REWRITE_DONE, mult); } - else - { - return RewriteResponse(REWRITE_AGAIN, mult); - } + // requires again full since ensureReal may have added a to_real + return RewriteResponse(REWRITE_AGAIN_FULL, mult); + } + Node ret = nm->mkNode(t.getKind(), left, right); + return RewriteResponse(REWRITE_DONE, ret); +} + +RewriteResponse ArithRewriter::rewriteToReal(TNode t) +{ + Assert(t.getKind() == kind::CAST_TO_REAL || t.getKind() == kind::TO_REAL); + if (!t[0].getType().isInteger()) + { + // if it is already real type, then just return the argument + return RewriteResponse(REWRITE_DONE, t[0]); + } + NodeManager* nm = NodeManager::currentNM(); + if (t[0].isConst()) + { + // If the argument is constant, return a real constant. + // !!!! Note that this does not preserve the type of t, since rat is + // an integral rational. This will be corrected when the type rule for + // CONST_RATIONAL is changed to always return Real. + const Rational& rat = t[0].getConst(); + return RewriteResponse(REWRITE_DONE, nm->mkConstReal(rat)); } + // CAST_TO_REAL is our way of marking integral constants coming from the + // user as Real. It should only be applied to constants, which is handled + // above. + Assert(t.getKind() != kind::CAST_TO_REAL); return RewriteResponse(REWRITE_DONE, t); } @@ -759,6 +808,11 @@ RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t) Node ret = isPred ? nm->mkConst(false) : nm->mkConstReal(Rational(3)); return returnRewrite(t, ret, Rewrite::INT_EXT_PI); } + else if (t[0].getKind() == kind::TO_REAL) + { + Node ret = nm->mkNode(t.getKind(), t[0][0]); + return returnRewrite(t, ret, Rewrite::INT_EXT_TO_REAL); + } return RewriteResponse(REWRITE_DONE, t); } @@ -884,12 +938,12 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) const Rational& rat = t[0].getConst(); if (rat.sgn() == 0) { - return RewriteResponse(REWRITE_DONE, rewriter::mkConst(Integer(0))); + return RewriteResponse(REWRITE_DONE, nm->mkConstReal(Rational(0))); } else if (rat.sgn() == -1) { - Node ret = nm->mkNode( - kind::NEG, nm->mkNode(kind::SINE, rewriter::mkConst(-rat))); + Node ret = nm->mkNode(kind::NEG, + nm->mkNode(kind::SINE, nm->mkConstReal(-rat))); return RewriteResponse(REWRITE_AGAIN_FULL, ret); } } @@ -965,6 +1019,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { new_arg = nm->mkNode(kind::ADD, new_arg, rem); } + new_arg = ensureReal(new_arg); // sin( 2*n*PI + x ) = sin( x ) return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode(kind::SINE, new_arg)); @@ -994,8 +1049,8 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) if (r_abs.getDenominator() == two) { Assert(r_abs.getNumerator() == one); - return RewriteResponse(REWRITE_DONE, - nm->mkConstReal(Rational(r.sgn()))); + return RewriteResponse( + REWRITE_DONE, ensureReal(nm->mkConstReal(Rational(r.sgn())))); } else if (r_abs.getDenominator() == six) { @@ -1070,6 +1125,40 @@ TrustNode ArithRewriter::expandDefinition(Node node) return ret; } +TNode ArithRewriter::removeToReal(TNode t) +{ + return t.getKind() == kind::TO_REAL ? t[0] : t; +} + +Node ArithRewriter::maybeEnsureReal(TypeNode tn, TNode t) +{ + // if we require being a real + if (!tn.isInteger()) + { + // ensure that t has type real + Assert(tn.isReal()); + return ensureReal(t); + } + return t; +} + +Node ArithRewriter::ensureReal(TNode t) +{ + if (t.getType().isInteger()) + { + if (t.isConst()) + { + // short-circuit + Node ret = NodeManager::currentNM()->mkConstReal(t.getConst()); + Assert(ret.getType().isReal()); + return ret; + } + Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl; + return NodeManager::currentNM()->mkNode(kind::TO_REAL, t); + } + return t; +} + RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r) { Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by " diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 0f2a55f84..3da45fead 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -40,7 +40,6 @@ class ArithRewriter : public TheoryRewriter * the given node. */ TrustNode expandDefinition(Node node) override; - private: /** preRewrite for atoms */ static RewriteResponse preRewriteAtom(TNode t); @@ -72,6 +71,8 @@ class ArithRewriter : public TheoryRewriter /** rewrite division */ static RewriteResponse rewriteDiv(TNode t, bool pre); + /** rewrite to_real */ + static RewriteResponse rewriteToReal(TNode t); /** rewrite absolute */ static RewriteResponse rewriteAbs(TNode t); /** rewrite integer division and modulus */ @@ -93,6 +94,17 @@ class ArithRewriter : public TheoryRewriter /** return rewrite */ static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r); + /** + * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL. + */ + static TNode removeToReal(TNode t); + /** + * Ensure that t has real type if tn is the real type. Do so by applying + * TO_REAL to t. + */ + static Node maybeEnsureReal(TypeNode tn, TNode t); + /** Same as above, without a check for the type of tn. */ + static Node ensureReal(TNode t); /** The operator elimination utility */ OperatorElim& d_opElim; }; /* class ArithRewriter */ diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 0d31d734f..8a6d535c9 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -3823,6 +3823,8 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{ Theory::shared_terms_iterator shared_end = d_containing.shared_terms_end(); for(; shared_iter != shared_end; ++shared_iter){ Node sharedCurr = *shared_iter; + sharedCurr = + sharedCurr.getKind() == kind::TO_REAL ? sharedCurr[0] : sharedCurr; // ModelException is fatal as this point. Don't catch! // DeltaRationalException is fatal as this point. Don't catch! diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp index cd6510a6b..f12124a4e 100644 --- a/src/theory/arith/rewriter/rewrite_atom.cpp +++ b/src/theory/arith/rewriter/rewrite_atom.cpp @@ -226,11 +226,13 @@ std::optional tryEvaluateRelation(Kind rel, TNode left, TNode right) return {}; } -std::optional tryEvaluateRelationReflexive(TNode atom) +std::optional tryEvaluateRelationReflexive(Kind rel, + TNode left, + TNode right) { - if (atom.getNumChildren() == 2 && atom[0] == atom[1]) + if (left == right) { - switch (atom.getKind()) + switch (rel) { case Kind::LT: return false; case Kind::LEQ: return true; @@ -352,4 +354,4 @@ Node buildRealInequality(Sum&& sum, Kind k) } // namespace rewriter } // namespace arith } // namespace theory -} // namespace cvc5::internal \ No newline at end of file +} // namespace cvc5::internal diff --git a/src/theory/arith/rewriter/rewrite_atom.h b/src/theory/arith/rewriter/rewrite_atom.h index 68c8cd564..e5ffdba93 100644 --- a/src/theory/arith/rewriter/rewrite_atom.h +++ b/src/theory/arith/rewriter/rewrite_atom.h @@ -41,7 +41,9 @@ std::optional tryEvaluateRelation(Kind rel, TNode left, TNode right); * not identical). * Assumes atom to be a relational operator, i.e. one of <,<=,=,!=,>=,>. */ -std::optional tryEvaluateRelationReflexive(TNode atom); +std::optional tryEvaluateRelationReflexive(Kind rel, + TNode left, + TNode right); /** * Build a node `(kind left right)`. If negate is true, it returns the negation diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp index 51a50fbdc..4e2d6fb33 100644 --- a/src/theory/arith/rewrites.cpp +++ b/src/theory/arith/rewrites.cpp @@ -39,6 +39,7 @@ const char* toString(Rewrite r) case Rewrite::INT_EXT_CONST: return "INT_EXT_CONST"; case Rewrite::INT_EXT_INT: return "INT_EXT_INT"; case Rewrite::INT_EXT_PI: return "INT_EXT_PI"; + case Rewrite::INT_EXT_TO_REAL: return "INT_EXT_TO_REAL"; default: return "?"; } } diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 8e198c53d..be90f2417 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -59,7 +59,9 @@ enum class Rewrite : uint32_t // (to_int t) --> t, (is_int t) ---> true if t is int INT_EXT_INT, // (to_int real.pi) --> 3, (is_int real.pi) ---> false - INT_EXT_PI + INT_EXT_PI, + // (to_int (to_real x)) --> (to_int x), (is_int (to_real x)) --> (is_int x) + INT_EXT_TO_REAL }; /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index fe04a9c26..c1cdef9f1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -121,7 +121,11 @@ void TheoryArith::preRegisterTerm(TNode n) d_internal->preRegisterTerm(n); } -void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); } +void TheoryArith::notifySharedTerm(TNode n) +{ + n = n.getKind() == kind::TO_REAL ? n[0] : n; + d_internal->notifySharedTerm(n); +} TrustNode TheoryArith::ppRewrite(TNode atom, std::vector& lems) { @@ -352,6 +356,7 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { } Node TheoryArith::getModelValue(TNode var) { + var = var.getKind() == kind::TO_REAL ? var[0] : var; std::map::iterator it = d_arithModelCache.find(var); if (it != d_arithModelCache.end()) { diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 3acc0b76a..ab03ba395 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -520,6 +520,7 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(x.abs()); break; } + case kind::TO_REAL: case kind::CAST_TO_REAL: { // casting to real is a no-op @@ -527,6 +528,19 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(x); break; } + case kind::TO_INTEGER: + { + // casting to int takes the floor + const Rational& x = results[currNode[0]].d_rat.floor(); + results[currNode] = EvalResult(x); + break; + } + case kind::IS_INTEGER: + { + const Rational& x = results[currNode[0]].d_rat; + results[currNode] = EvalResult(x.isIntegral()); + break; + } case kind::CONST_STRING: results[currNode] = EvalResult(currNodeVal.getConst()); break; diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index d8119e45f..40e07fb55 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -904,10 +904,13 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, int ires_use = (msum[pv].isNull() || msum[pv].getConst().sgn() == 1) ? 1 : -1; - val = rewrite( - nm->mkNode(ires_use == -1 ? ADD : SUB, - nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart), - nm->mkNode(TO_INTEGER, realPart))); + val = nm->mkNode(ires_use == -1 ? ADD : SUB, + nm->mkNode(ires_use == -1 ? SUB : ADD, val, 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()); diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index dbb6c6acc..5320638be 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -266,7 +266,7 @@ CegHandledStatus CegInstantiator::isCbqiKind(Kind k) || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER - || k == IS_INTEGER) + || k == IS_INTEGER || k == TO_REAL) { return CEG_HANDLED; } diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 4c6eac6eb..503ee4c2c 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -954,6 +954,11 @@ 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()); } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 417763123..174d448ee 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -778,6 +778,7 @@ set(regress_0_tests regress0/nl/all-logic.smt2 regress0/nl/coeff-sat.smt2 regress0/nl/combined-uf.smt2 + regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2 regress0/nl/iand-no-init.smt2 regress0/nl/issue3003.smt2 regress0/nl/issue3407.smt2 diff --git a/test/regress/cli/regress0/arith/bug549.cvc.smt2 b/test/regress/cli/regress0/arith/bug549.cvc.smt2 index 8a62b7064..74bdc8878 100644 --- a/test/regress/cli/regress0/arith/bug549.cvc.smt2 +++ b/test/regress/cli/regress0/arith/bug549.cvc.smt2 @@ -3,4 +3,4 @@ (set-option :incremental false) (declare-fun a () Real) (declare-fun b () Real) -(check-sat-assuming ( (not (= (^ (* a b) 5.0) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) )) +(check-sat-assuming ( (not (= (^ (* a b) 5) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) )) diff --git a/test/regress/cli/regress0/bug339.smt2 b/test/regress/cli/regress0/bug339.smt2 index bb03cf9b1..6252aa322 100644 --- a/test/regress/cli/regress0/bug339.smt2 +++ b/test/regress/cli/regress0/bug339.smt2 @@ -5,7 +5,7 @@ (declare-fun P () Bool) (assert - (let ((y (ite P 1 x))) + (let ((y (ite P 1.0 x))) (and (not (= y 1)) (> y 0) (<= y 1)))) diff --git a/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2 b/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2 new file mode 100644 index 000000000..abc694109 --- /dev/null +++ b/test/regress/cli/regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_UFNRA) +(set-info :status sat) +(declare-fun f (Real) Real) +(declare-fun p (Real Real Real) Bool) +(check-sat-assuming ((= 0.0 (/ 1 (ite (p 0.0 0.0 (/ (ite (p 0.0 0.0 (f 0.0)) 1 0) 1)) 1 0))))) diff --git a/test/regress/cli/regress0/quantifiers/mix-match.smt2 b/test/regress/cli/regress0/quantifiers/mix-match.smt2 index d123bf9c4..a7fc077de 100644 --- a/test/regress/cli/regress0/quantifiers/mix-match.smt2 +++ b/test/regress/cli/regress0/quantifiers/mix-match.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: +; COMMAND-LINE: --enum-inst ; EXPECT: unsat (set-logic ALL) (set-info :status unsat)