diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-06 11:23:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-06 13:23:44 -0300 |
| commit | e92b4504d5930234c852bf0fba8f5663ad4809e7 (patch) | |
| tree | 128c1859cedbcac407b2f7da7daeb0ef20001c1d | |
| parent | da03399e50e33acd4d4a6534205a67d03f44f4c1 (diff) | |
Fix tptp parser for negative rational (#6297)
| -rw-r--r-- | src/parser/tptp/Tptp.g | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/tptp/parse-neg-rational.p | 33 |
3 files changed, 35 insertions, 0 deletions
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) )). +%------------------------------------------------------------------------------ |