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 b03188b3ce8909393da3ebe2018396ca613646b3..2a3a791259392f65ffac3daf7fe5e557a37e6c21 100644 (file)
--- 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 a8dfbfeab7abebf2533355b4d0940a748804ca3f..091e6c93ca857aa6ff8e8f399723e200b9186f7d 100644 (file)
--- 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';