From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Mar 2019 19:06:48 +0000 (-0500)
Subject: Implement proper semantics for TPTP predicate is_rat. (#2861)
X-Git-Tag: cvc5-1.0.0~4247
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92d541960c7c1d4b06dbef8bebbb106d52fcaeb4;p=cvc5.git

Implement proper semantics for TPTP predicate is_rat. (#2861)
---

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) ) ).
+
+%------------------------------------------------------------------------------