From 92d541960c7c1d4b06dbef8bebbb106d52fcaeb4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Mar 2019 14:06:48 -0500
Subject: [PATCH] Implement proper semantics for TPTP predicate is_rat. (#2861)

---
 src/parser/tptp/Tptp.g                     | 20 +++++++++++++++++---
 test/regress/CMakeLists.txt                |  1 +
 test/regress/regress0/tptp/is_rat_simple.p |  8 ++++++++
 3 files changed, 26 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/tptp/is_rat_simple.p

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 54e9b0b4a..f4bc48df4 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -352,10 +352,24 @@ definedPred[CVC4::Expr& expr]
   | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); }
   | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); }
   | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); }
-  | '$is_rat' // all "real" are actually "rat" in CVC4
+  | '$is_rat'
+    // a real n is a rational if there exists q,r integers such that
+    //   to_real(q) = n*to_real(r),
+    // where r is non-zero.
     { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
-      expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true)));
+      Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
+      Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q);
+      Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
+      Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r);
+      Expr body =
+          MK_EXPR(CVC4::kind::AND,
+                  MK_EXPR(CVC4::kind::NOT,
+                          MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))),
+                  MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr)));
+      Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r);
+      body = MK_EXPR(CVC4::kind::EXISTS, bvl, body);
+      Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body);
     }
   | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
   | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index abec884c2..64d8e3598 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -877,6 +877,7 @@ set(regress_0_tests
   regress0/test9.cvc
   regress0/tptp/ARI086=1.p
   regress0/tptp/DAT001=1.p
+  regress0/tptp/is_rat_simple.p
   regress0/tptp/KRS018+1.p
   regress0/tptp/KRS063+1.p
   regress0/tptp/MGT019+2.p
diff --git a/test/regress/regress0/tptp/is_rat_simple.p b/test/regress/regress0/tptp/is_rat_simple.p
new file mode 100644
index 000000000..c983033b9
--- /dev/null
+++ b/test/regress/regress0/tptp/is_rat_simple.p
@@ -0,0 +1,8 @@
+% states that all reals are not rational (countersatisfiable)
+% Status   : CounterSatisfiable
+%------------------------------------------------------------------------------
+tff(the,conjecture,(
+    ! [X: $real] :
+      ~ $is_rat(X) ) ).
+
+%------------------------------------------------------------------------------
-- 
2.30.2