From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 15 Mar 2014 21:29:09 +0000 (-0400)
Subject: Minor usability fixes related to SMT-LIB compliance.
X-Git-Tag: cvc5-1.0.0~7010
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=035aaf3a248960e6bbe6a7350fa8e4ca86b35f94;p=cvc5.git

Minor usability fixes related to SMT-LIB compliance.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3c68e4e4c..f987de2f1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -253,6 +253,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
   | /* sort declaration */
     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
+        PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString());
+      }
+    }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
     n=INTEGER_LITERAL
@@ -295,6 +302,9 @@ command returns [CVC4::Command* cmd = NULL]
     sortSymbol[t,CHECK_DECLARED]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
       if( sorts.size() > 0 ) {
+        if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
+          PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
+        }
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
       Expr func = PARSER_STATE->mkVar(name, t);
@@ -488,6 +498,13 @@ extendedCommand[CVC4::Command*& cmd]
       $cmd = new DeclareFunctionCommand(name, c, t); }
 
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
+         !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
+        PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString());
+      }
+    }
     { $cmd = new CommandSequence(); }
     LPAREN_TOK
     ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
@@ -506,6 +523,9 @@ extendedCommand[CVC4::Command*& cmd]
       nonemptySortList[sorts] RPAREN_TOK
       { Type t;
         if(sorts.size() > 1) {
+          if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
+            PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
+          }
           t = EXPR_MANAGER->mkFunctionType(sorts);
         } else {
           t = sorts[0];
@@ -524,6 +544,9 @@ extendedCommand[CVC4::Command*& cmd]
       sortList[sorts] RPAREN_TOK
       { Type t = EXPR_MANAGER->booleanType();
         if(sorts.size() > 0) {
+          if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
+            PARSER_STATE->parseError(std::string("Predicates (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
+          }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
         Expr func = PARSER_STATE->mkVar(name, t);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b59880a5e..64b321613 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -154,6 +154,12 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::SET_SINGLETON, "setenum");
     break;
 
+  case THEORY_DATATYPES:
+    Parser::addOperator(kind::APPLY_CONSTRUCTOR);
+    Parser::addOperator(kind::APPLY_TESTER);
+    Parser::addOperator(kind::APPLY_SELECTOR);
+    break;
+
   case THEORY_STRINGS:
     defineType("String", getExprManager()->stringType());
     addStringOperators();
@@ -194,6 +200,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
     return d_logic.isTheoryEnabled(theory::THEORY_BV);
   case THEORY_CORE:
     return true;
+  case THEORY_DATATYPES:
+    return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
   case THEORY_INTS:
     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
@@ -253,6 +261,10 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
   }
 
+  if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+    addTheory(THEORY_DATATYPES);
+  }
+
   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
     addTheory(THEORY_SETS);
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 969892c5f..55a06a8e3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -40,6 +40,7 @@ public:
     THEORY_ARRAYS,
     THEORY_BITVECTORS,
     THEORY_CORE,
+    THEORY_DATATYPES,
     THEORY_INTS,
     THEORY_REALS,
     THEORY_REALS_INTS,
@@ -83,6 +84,11 @@ public:
    */
   void setLogic(const std::string& name);
 
+  /**
+   * Get the logic.
+   */
+  const LogicInfo& getLogic() const { return d_logic; }
+
   void setInfo(const std::string& flag, const SExpr& sexpr);
 
   void setOption(const std::string& flag, const SExpr& sexpr);
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
index 12658e507..75d82d98f 100644
--- a/test/regress/regress0/bug548a.smt2
+++ b/test/regress/regress0/bug548a.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --rewrite-divk --tlimit 1000
 ; EXPECT: unknown
-(set-logic LIA)
+(set-logic AUFLIA)
 (declare-fun f (Int) Int)