more compliance fixes for SMT-LIBv2

3 files changed, 23 insertions, 5 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index f48e07887..f4b40cbb3 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -990,11 +990,11 @@ std::string GetInfoCommand::getFlag() const throw() {
 
 void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.push_back(smtEngine->getInfo(d_flag));
+    SExpr response = smtEngine->getInfo(d_flag);
     stringstream ss;
-    ss << SExpr(v);
+    ss << SExpr(SExpr::Keyword(d_flag))
+       << ' '
+       << response;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bddb64c3c..be5a797bf 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -198,7 +198,9 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
   | /* sort declaration */
     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
+    symbol[name,CHECK_UNDECLARED,SYM_SORT]
+    { PARSER_STATE->checkUserSymbol(name); }
+    n=INTEGER_LITERAL
     { Debug("parser") << "declare sort: '" << name
                       << "' arity=" << n << std::endl;
       unsigned arity = AntlrInput::tokenToUnsigned(n);
@@ -213,6 +215,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* sort definition */
     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
+    { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
     {
       PARSER_STATE->pushScope();
@@ -233,6 +236,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* function declaration */
     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK sortList[sorts] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
@@ -244,6 +248,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* function definition */
     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
     { /* add variables to parser state before parsing term */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 9d33e3e62..c55a5e430 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -24,6 +24,8 @@
 #include "parser/parser.h"
 #include "parser/smt/smt.h"
 
+#include <sstream>
+
 namespace CVC4 {
 
 class SExpr;
@@ -75,9 +77,20 @@ public:
 
   void checkThatLogicIsSet();
 
+  void checkUserSymbol(const std::string& name) {
+    if( strictModeEnabled() &&
+        name.length() > 0 &&
+        ( name[0] == '.' || name[0] == '@' ) ) {
+      std::stringstream ss;
+      ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIBv2";
+      parseError(ss.str());
+    }
+  }
+
 private:
 
   void addArithmeticOperators();
+
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */