From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 30 Jun 2011 21:03:52 +0000 (+0000)
Subject: Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
X-Git-Tag: cvc5-1.0.0~8525
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af25c3f8498198dd6dd114c3b4ef39af54611e1e;p=cvc5.git

Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default).  The danoint benchmarks
have such monsters.
---

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index b03188b3c..2a3a79125 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -218,6 +218,10 @@ annotatedFormula[CVC4::Expr& expr]
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
+      } else if(!PARSER_STATE->strictModeEnabled() &&
+                kind == CVC4::kind::MINUS && args.size() == 1) {
+        /* Special fix-up for unary minus improperly used in some benchmarks */
+        expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
       } else {
         PARSER_STATE->checkArity(kind, args.size());
         expr = MK_EXPR(kind, args);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a8dfbfeab..091e6c93c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -765,7 +765,7 @@ POUND_TOK         : '#';
 SELECT_TOK        : 'select';
 STAR_TOK          : '*';
 STORE_TOK         : 'store';
-TILDE_TOK         : '~';
+// TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
 CONCAT_TOK : 'concat';