From 847b494afa496afcbb3c776f6dba65b7f744fee9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Nov 2021 15:25:20 -0600 Subject: [PATCH] Add rewrite for is_int pi (#7711) Fixes cvc5/cvc5-projects#365. Fixes cvc5/cvc5-projects#356. --- src/theory/arith/arith_rewriter.cpp | 65 ++++++++++--------- src/theory/arith/arith_rewriter.h | 2 + src/theory/arith/rewrites.cpp | 3 + src/theory/arith/rewrites.h | 8 ++- test/regress/CMakeLists.txt | 1 + .../regress1/nl/proj-365-is-int-pi.smt2 | 5 ++ 6 files changed, 52 insertions(+), 32 deletions(-) create mode 100644 test/regress/regress1/nl/proj-365-is-int-pi.smt2 diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 19b5c1204..8408f15bb 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -166,6 +166,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ }else if(t.isVar()){ return rewriteVariable(t); }else{ + Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl; switch(t.getKind()){ case kind::MINUS: return rewriteMinus(t, false); @@ -213,29 +214,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); - case kind::TO_INTEGER: - if(t[0].isConst()) { - return RewriteResponse( - REWRITE_DONE, - NodeManager::currentNM()->mkConst( - CONST_RATIONAL, Rational(t[0].getConst().floor()))); - } - if(t[0].getType().isInteger()) { - return RewriteResponse(REWRITE_DONE, t[0]); - } - //Unimplemented() << "TO_INTEGER, nonconstant"; - //return rewriteToInteger(t); - return RewriteResponse(REWRITE_DONE, t); - case kind::IS_INTEGER: - if(t[0].isConst()) { - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst().getDenominator() == 1)); - } - if(t[0].getType().isInteger()) { - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); - } - //Unimplemented() << "IS_INTEGER, nonconstant"; - //return rewriteIsInteger(t); - return RewriteResponse(REWRITE_DONE, t); + case kind::TO_INTEGER:return rewriteExtIntegerOp(t); case kind::POW: { if(t[1].getKind() == kind::CONST_RATIONAL){ @@ -668,14 +647,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ if(atom.getKind() == kind::IS_INTEGER) { - if(atom[0].isConst()) { - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst().isIntegral())); - } - if(atom[0].getType().isInteger()) { - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); - } - // not supported, but this isn't the right place to complain - return RewriteResponse(REWRITE_DONE, atom); + return rewriteExtIntegerOp(atom); } else if(atom.getKind() == kind::DIVISIBLE) { if(atom[0].isConst()) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst() / atom.getOperator().getConst().k).isIntegral()))); @@ -847,6 +819,37 @@ RewriteResponse ArithRewriter::rewriteIntsDivMod(TNode t, bool pre) return RewriteResponse(REWRITE_DONE, t); } +RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t) +{ + Assert(t.getKind() == kind::TO_INTEGER || t.getKind() == kind::IS_INTEGER); + bool isPred = t.getKind() == kind::IS_INTEGER; + NodeManager* nm = NodeManager::currentNM(); + if (t[0].isConst()) + { + Node ret; + if (isPred) + { + ret = nm->mkConst(t[0].getConst().isIntegral()); + } + else + { + ret = nm->mkConstInt(Rational(t[0].getConst().floor())); + } + return returnRewrite(t, ret, Rewrite::INT_EXT_CONST); + } + if (t[0].getType().isInteger()) + { + Node ret = isPred ? nm->mkConst(true) : Node(t[0]); + return returnRewrite(t, ret, Rewrite::INT_EXT_INT); + } + if (t[0].getKind() == kind::PI) + { + Node ret = isPred ? nm->mkConst(false) : nm->mkConstReal(Rational(3)); + return returnRewrite(t, ret, Rewrite::INT_EXT_PI); + } + return RewriteResponse(REWRITE_DONE, t); +} + RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre) { if (pre) diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 813f2b1bb..1f861b08a 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -56,6 +56,8 @@ class ArithRewriter : public TheoryRewriter static RewriteResponse rewriteDiv(TNode t, bool pre); static RewriteResponse rewriteIntsDivMod(TNode t, bool pre); static RewriteResponse rewriteIntsDivModTotal(TNode t, bool pre); + /** Entry for applications of to_int and is_int */ + static RewriteResponse rewriteExtIntegerOp(TNode t); static RewriteResponse preRewritePlus(TNode t); static RewriteResponse postRewritePlus(TNode t); diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp index a70132422..2283cd73a 100644 --- a/src/theory/arith/rewrites.cpp +++ b/src/theory/arith/rewrites.cpp @@ -36,6 +36,9 @@ const char* toString(Rewrite r) case Rewrite::MOD_OVER_MOD: return "MOD_OVER_MOD"; case Rewrite::MOD_CHILD_MOD: return "MOD_CHILD_MOD"; case Rewrite::DIV_OVER_MOD: return "DIV_OVER_MOD"; + 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"; default: return "?"; } } diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 24b6abdd5..6053be916 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -53,7 +53,13 @@ enum class Rewrite : uint32_t // op is one of { NONLINEAR_MULT, MULT, PLUS }. MOD_CHILD_MOD, // (div (mod x c) c) --> 0 - DIV_OVER_MOD + DIV_OVER_MOD, + // (to_int c) --> floor(c), (is_int c) --> true iff c is int + INT_EXT_CONST, + // (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 }; /** diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 686c0ff6e..e52f2ac63 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1814,6 +1814,7 @@ set(regress_1_tests regress1/nl/ones.smt2 regress1/nl/pinto-model-core-ni.smt2 regress1/nl/poly-1025.smt2 + regress1/nl/proj-365-is-int-pi.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 regress1/nl/rewriting-sums.smt2 diff --git a/test/regress/regress1/nl/proj-365-is-int-pi.smt2 b/test/regress/regress1/nl/proj-365-is-int-pi.smt2 new file mode 100644 index 000000000..dab3dcfa3 --- /dev/null +++ b/test/regress/regress1/nl/proj-365-is-int-pi.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :nl-ext light) +(assert (is_int real.pi)) +(check-sat) -- 2.30.2