From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 19 Aug 2013 22:15:21 +0000 (-0400)
Subject: Add support for check-sat with argument.
X-Git-Tag: cvc5-1.0.0~7287^2~19
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=28ec8ce392a815c47689ecd86b5b91f9a58104e5;p=cvc5.git

Add support for check-sat with argument.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 23f0fb9fa..a6a2aa58c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -344,7 +344,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
+    ( term[expr, expr2]
+      { if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("Extended commands (such as check-sat with an argument) are not permitted while operating in strict compliance mode.");
+        }
+      }
+    | { expr = MK_CONST(bool(true)); } )
+    { cmd = new CheckSatCommand(expr); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetAssertionsCommand(); }
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1dbaf7cdf..8ff62c25a 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -395,7 +395,7 @@ public:
 #ifndef CVC4_COMPETITION_MODE
     tryBadInput("(assert)"); // no args
     tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
-    tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg
+    tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg
     tryBadInput("(declare-sort a)"); // no arg
     tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
     tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"