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

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 54e9b0b4a17af3314001ed4552acc504f4a047bc..f4bc48df44cc227f01531ab6668cd2d889375cec 100644 (file)
--- 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 abec884c2a7d5b9a8c974133aca66a64c525f57b..64d8e35985f8b21413c309987e70bfd572ccd5f0 100644 (file)
--- 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 (file)
index 0000000..c983033
--- /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) ) ).
+
+%------------------------------------------------------------------------------