From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 6 Apr 2021 16:23:44 +0000 (-0500)
Subject: Fix tptp parser for negative rational (#6297)
X-Git-Tag: cvc5-1.0.0~1961
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e92b4504d5930234c852bf0fba8f5663ad4809e7;p=cvc5.git

Fix tptp parser for negative rational (#6297)
---

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index f6b845212..0f21cdb20 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1764,6 +1764,7 @@ NUMBER
       }
     | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
       { std::stringstream ss;
+        ss << ( pos ? "" : "-" );
         ss << AntlrInput::tokenText($num) << "/" << AntlrInput::tokenText($den);
         PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 49b7b0543..0c42c09e4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1198,6 +1198,7 @@ set(regress_0_tests
   regress0/tptp/MGT019+2.p
   regress0/tptp/MGT041-2.p
   regress0/tptp/PUZ131_1.p
+  regress0/tptp/parse-neg-rational.p
   regress0/tptp/SYN000_1.p
   regress0/tptp/SYN000_2.p
   regress0/tptp/SYN000-1.p
diff --git a/test/regress/regress0/tptp/parse-neg-rational.p b/test/regress/regress0/tptp/parse-neg-rational.p
new file mode 100644
index 000000000..9e892a3b7
--- /dev/null
+++ b/test/regress/regress0/tptp/parse-neg-rational.p
@@ -0,0 +1,33 @@
+%------------------------------------------------------------------------------
+% File     : ARI196=1 : TPTP v7.4.0. Released v5.0.0.
+% Domain   : Arithmetic
+% Problem  : Rational: -1/4 less than 1/4
+% Version  : Especial.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Theorem
+% Rating   : 0.00 v6.2.0, 0.20 v6.1.0, 0.22 v6.0.0, 0.25 v5.3.0, 0.14 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0
+% Syntax   : Number of formulae    :    1 (   1 unit;   0 type)
+%            Number of atoms       :    1 (   0 equality)
+%            Maximal formula depth :    1 (   1 average)
+%            Number of connectives :    0 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :    1 (   0 propositional; 2-2 arity)
+%            Number of functors    :    2 (   2 constant; 0-0 arity)
+%            Number of variables   :    0 (   0 sgn;   0   !;   0   ?)
+%                                         (   0   :;   0  !>;   0  ?*)
+%            Maximal term depth    :    1 (   1 average)
+%            Arithmetic symbols    :    2 (   1 prd;   0 fun;   1 num;   0 var)
+% SPC      : TF0_THM_NEQ_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(rat_less_problem_7,conjecture,(
+    $less(-1/4,1/4) )).
+%------------------------------------------------------------------------------