Only allow bv2nat/int2bv with BV and integer logic (#4118)

CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e54f8eaa91c65e62f57bfb6f71532e3a4876506a..d01fd7a052b901ef9cdbc0445e9b2fb5fda16f9f 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -250,13 +250,10 @@ command [std::unique_ptr<CVC4::Command>* cmd]
           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->parseErrorLogic("Free sort symbols not allowed in ");
-      }
+    DECLARE_SORT_TOK
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      PARSER_STATE->checkLogicAllowsFreeSorts();
     }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
@@ -303,12 +300,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       if( !sorts.empty() ) {
         t = PARSER_STATE->mkFlatFunctionType(sorts, t);
       }
-      if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-        PARSER_STATE->parseError(
-            "Functions (of non-zero arity) cannot "
-            "be declared in logic "
-            + PARSER_STATE->getLogic().getLogicString()
-            + " unless option --uf-ho is used.");
+      if(t.isFunction())
+      {
+        PARSER_STATE->checkLogicAllowsFunctions();
       }
       // we allow overloading for function declarations
       if (PARSER_STATE->sygus_v1())
@@ -1259,15 +1253,12 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 
     /* Support some of Z3's extended SMT-LIB commands */
 
-  | 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->parseErrorLogic("Free sort symbols not allowed in ");
-      }
+  | DECLARE_SORTS_TOK
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      PARSER_STATE->checkLogicAllowsFreeSorts();
+      seq.reset(new CVC4::CommandSequence());
     }
-    { seq.reset(new CVC4::CommandSequence()); }
     LPAREN_TOK
     ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
       { PARSER_STATE->checkUserSymbol(name);
@@ -1286,13 +1277,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       nonemptySortList[sorts] RPAREN_TOK
       { api::Sort tt;
         if(sorts.size() > 1) {
-          if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseError(
-                "Functions (of non-zero arity) cannot "
-                "be declared in logic "
-                + PARSER_STATE->getLogic().getLogicString()
-                + " unless option --uf-ho is used");
-          }
+          PARSER_STATE->checkLogicAllowsFunctions();
           // must flatten
           api::Sort range = sorts.back();
           sorts.pop_back();
@@ -1318,13 +1303,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       sortList[sorts] RPAREN_TOK
       { t = SOLVER->getBooleanSort();
         if(sorts.size() > 0) {
-          if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseError(
-                "Functions (of non-zero arity) cannot "
-                "be declared in logic "
-                + PARSER_STATE->getLogic().getLogicString()
-                + " unless option --uf-ho is used");
-          }
+          PARSER_STATE->checkLogicAllowsFunctions();
           t = SOLVER->mkFunctionSort(sorts, t);
         }
         // allow overloading
@@ -2414,13 +2393,13 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Extra parentheses around sort name not "
                                    "permitted in SMT-LIB");
         } else if(name == "Array" &&
-           PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
+           PARSER_STATE->isTheoryEnabled(theory::THEORY_ARRAYS) ) {
           if(args.size() != 2) {
             PARSER_STATE->parseError("Illegal array type.");
           }
           t = SOLVER->mkArraySort( args[0], args[1] );
         } else if(name == "Set" &&
-                  PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
+                  PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) ) {
           if(args.size() != 1) {
             PARSER_STATE->parseError("Illegal set type.");
           }
@@ -2611,9 +2590,9 @@ DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'decla
 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
-COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }?'comprehension';
-TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
-MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
+COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
+TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
+MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';
 GET_MODEL_TOK : 'get-model';
 BLOCK_MODEL_TOK : 'block-model';
 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
@@ -2657,9 +2636,9 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
 
-EMP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'emp';
-TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple';
-TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel';
+EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
+TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
+TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
 
 HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
 HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c30c44362ddd5921edf223340e1b42ba52babd15..c7c30005c73e41520d3d8be212ad2ab9f7b3efe4 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -40,7 +40,7 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
 {
   if (!strictModeEnabled())
   {
-    addTheory(Smt2::THEORY_CORE);
+    addCoreSymbols();
   }
 }
 
@@ -120,7 +120,6 @@ void Smt2::addBitvectorOperators() {
   addOperator(api::BITVECTOR_SGE, "bvsge");
   addOperator(api::BITVECTOR_REDOR, "bvredor");
   addOperator(api::BITVECTOR_REDAND, "bvredand");
-  addOperator(api::BITVECTOR_TO_NAT, "bv2nat");
 
   addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
   addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
@@ -132,7 +131,6 @@ void Smt2::addBitvectorOperators() {
       api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
   addIndexedOperator(
       api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right");
-  addIndexedOperator(api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
 }
 
 void Smt2::addDatatypesOperators()
@@ -270,161 +268,19 @@ void Smt2::addSepOperators() {
   Parser::addOperator(api::SEP_EMP);
 }
 
-void Smt2::addTheory(Theory theory) {
-  switch(theory) {
-  case THEORY_ARRAYS:
-    addOperator(api::SELECT, "select");
-    addOperator(api::STORE, "store");
-    break;
-
-  case THEORY_BITVECTORS:
-    addBitvectorOperators();
-    break;
-
-  case THEORY_CORE:
-    defineType("Bool", d_solver->getBooleanSort());
-    defineVar("true", d_solver->mkTrue());
-    defineVar("false", d_solver->mkFalse());
-    addOperator(api::AND, "and");
-    addOperator(api::DISTINCT, "distinct");
-    addOperator(api::EQUAL, "=");
-    addOperator(api::IMPLIES, "=>");
-    addOperator(api::ITE, "ite");
-    addOperator(api::NOT, "not");
-    addOperator(api::OR, "or");
-    addOperator(api::XOR, "xor");
-    break;
-
-  case THEORY_REALS_INTS:
-    defineType("Real", d_solver->getRealSort());
-    addOperator(api::DIVISION, "/");
-    addOperator(api::TO_INTEGER, "to_int");
-    addOperator(api::IS_INTEGER, "is_int");
-    addOperator(api::TO_REAL, "to_real");
-    // falling through on purpose, to add Ints part of Reals_Ints
-    CVC4_FALLTHROUGH;
-  case THEORY_INTS:
-    defineType("Int", d_solver->getIntegerSort());
-    addArithmeticOperators();
-    addOperator(api::INTS_DIVISION, "div");
-    addOperator(api::INTS_MODULUS, "mod");
-    addOperator(api::ABS, "abs");
-    addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
-    break;
-
-  case THEORY_REALS:
-    defineType("Real", d_solver->getRealSort());
-    addArithmeticOperators();
-    addOperator(api::DIVISION, "/");
-    if (!strictModeEnabled())
-    {
-      addOperator(api::ABS, "abs");
-    }
-    break;
-
-  case THEORY_TRANSCENDENTALS:
-    defineVar("real.pi", d_solver->mkTerm(api::PI));
-    addTranscendentalOperators();
-    break;
-
-  case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
-
-  case THEORY_SETS:
-    defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort()));
-    // the Boolean sort is a placeholder here since we don't have type info
-    // without type annotation
-    defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort()));
-
-    addOperator(api::UNION, "union");
-    addOperator(api::INTERSECTION, "intersection");
-    addOperator(api::SETMINUS, "setminus");
-    addOperator(api::SUBSET, "subset");
-    addOperator(api::MEMBER, "member");
-    addOperator(api::SINGLETON, "singleton");
-    addOperator(api::INSERT, "insert");
-    addOperator(api::CARD, "card");
-    addOperator(api::COMPLEMENT, "complement");
-    addOperator(api::JOIN, "join");
-    addOperator(api::PRODUCT, "product");
-    addOperator(api::TRANSPOSE, "transpose");
-    addOperator(api::TCLOSURE, "tclosure");
-    break;
-
-  case THEORY_DATATYPES:
-  {
-    const std::vector<api::Sort> types;
-    defineType("Tuple", d_solver->mkTupleSort(types));
-    addDatatypesOperators();
-    break;
-  }
-
-  case THEORY_STRINGS:
-    defineType("String", d_solver->getStringSort());
-    defineType("RegLan", d_solver->getRegExpSort());
-    defineType("Int", d_solver->getIntegerSort());
-
-    if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
-    {
-      defineVar("re.none", d_solver->mkRegexpEmpty());
-    }
-    else
-    {
-      defineVar("re.nostr", d_solver->mkRegexpEmpty());
-    }
-    defineVar("re.allchar", d_solver->mkRegexpSigma());
-
-    addStringOperators();
-    break;
-
-  case THEORY_UF:
-    Parser::addOperator(api::APPLY_UF);
-
-    if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
-    {
-      addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
-      addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
-    }
-    break;
-
-  case THEORY_FP:
-    defineType("RoundingMode", d_solver->getRoundingmodeSort());
-    defineType("Float16", d_solver->mkFloatingPointSort(5, 11));
-    defineType("Float32", d_solver->mkFloatingPointSort(8, 24));
-    defineType("Float64", d_solver->mkFloatingPointSort(11, 53));
-    defineType("Float128", d_solver->mkFloatingPointSort(15, 113));
-
-    defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
-    defineVar("roundNearestTiesToEven",
-              d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
-    defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
-    defineVar("roundNearestTiesToAway",
-              d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
-    defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
-    defineVar("roundTowardPositive",
-              d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
-    defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
-    defineVar("roundTowardNegative",
-              d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
-    defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
-    defineVar("roundTowardZero",
-              d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
-
-    addFloatingPointOperators();
-    break;
-    
-  case THEORY_SEP:
-    // the Boolean sort is a placeholder here since we don't have type info
-    // without type annotation
-    defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
-
-    addSepOperators();
-    break;
-    
-  default:
-    std::stringstream ss;
-    ss << "internal error: unsupported theory " << theory;
-    throw ParserException(ss.str());
-  }
+void Smt2::addCoreSymbols()
+{
+  defineType("Bool", d_solver->getBooleanSort());
+  defineVar("true", d_solver->mkTrue());
+  defineVar("false", d_solver->mkFalse());
+  addOperator(api::AND, "and");
+  addOperator(api::DISTINCT, "distinct");
+  addOperator(api::EQUAL, "=");
+  addOperator(api::IMPLIES, "=>");
+  addOperator(api::ITE, "ite");
+  addOperator(api::NOT, "not");
+  addOperator(api::OR, "or");
+  addOperator(api::XOR, "xor");
 }
 
 void Smt2::addOperator(api::Kind kind, const std::string& name)
@@ -453,42 +309,9 @@ bool Smt2::isOperatorEnabled(const std::string& name) const {
   return operatorKindMap.find(name) != operatorKindMap.end();
 }
 
-bool Smt2::isTheoryEnabled(Theory theory) const {
-  switch(theory) {
-  case THEORY_ARRAYS:
-    return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
-  case THEORY_BITVECTORS:
-    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() );
-  case THEORY_REALS:
-    return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
-      ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
-  case THEORY_REALS_INTS:
-    return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
-      d_logic.areIntegersUsed() && d_logic.areRealsUsed();
-  case THEORY_QUANTIFIERS:
-    return d_logic.isQuantified();
-  case THEORY_SETS:
-    return d_logic.isTheoryEnabled(theory::THEORY_SETS);
-  case THEORY_STRINGS:
-    return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
-  case THEORY_UF:
-    return d_logic.isTheoryEnabled(theory::THEORY_UF);
-  case THEORY_FP:
-    return d_logic.isTheoryEnabled(theory::THEORY_FP);
-  case THEORY_SEP:
-    return d_logic.isTheoryEnabled(theory::THEORY_SEP);
-  default:
-    std::stringstream ss;
-    ss << "internal error: unsupported theory " << theory;
-    throw ParserException(ss.str());
-  }
+bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
+{
+  return d_logic.isTheoryEnabled(theory);
 }
 
 bool Smt2::logicIsSet() {
@@ -522,7 +345,7 @@ bool Smt2::getTesterName(api::Term cons, std::string& name)
 api::Term Smt2::mkIndexedConstant(const std::string& name,
                                   const std::vector<uint64_t>& numerals)
 {
-  if (isTheoryEnabled(THEORY_FP))
+  if (d_logic.isTheoryEnabled(theory::THEORY_FP))
   {
     if (name == "+oo")
     {
@@ -546,7 +369,7 @@ api::Term Smt2::mkIndexedConstant(const std::string& name,
     }
   }
 
-  if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
+  if (d_logic.isTheoryEnabled(theory::THEORY_BV) && name.find("bv") == 0)
   {
     std::string bvStr = name.substr(2);
     return d_solver->mkBitVector(numerals[0], bvStr, 10);
@@ -628,7 +451,7 @@ void Smt2::reset() {
   this->Parser::reset();
 
   if( !strictModeEnabled() ) {
-    addTheory(Smt2::THEORY_CORE);
+    addCoreSymbols();
   }
 }
 
@@ -760,59 +583,152 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
   }
 
   // Core theory belongs to every logic
-  addTheory(THEORY_CORE);
+  addCoreSymbols();
 
   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
-    addTheory(THEORY_UF);
+    Parser::addOperator(api::APPLY_UF);
+
+    if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
+    {
+      addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
+      addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
+    }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
     if(d_logic.areIntegersUsed()) {
-      if(d_logic.areRealsUsed()) {
-        addTheory(THEORY_REALS_INTS);
-      } else {
-        addTheory(THEORY_INTS);
+      defineType("Int", d_solver->getIntegerSort());
+      addArithmeticOperators();
+      addOperator(api::INTS_DIVISION, "div");
+      addOperator(api::INTS_MODULUS, "mod");
+      addOperator(api::ABS, "abs");
+      addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
+    }
+
+    if (d_logic.areRealsUsed())
+    {
+      defineType("Real", d_solver->getRealSort());
+      addArithmeticOperators();
+      addOperator(api::DIVISION, "/");
+      if (!strictModeEnabled())
+      {
+        addOperator(api::ABS, "abs");
       }
-    } else if(d_logic.areRealsUsed()) {
-      addTheory(THEORY_REALS);
+    }
+
+    if (d_logic.areIntegersUsed() && d_logic.areRealsUsed())
+    {
+      addOperator(api::TO_INTEGER, "to_int");
+      addOperator(api::IS_INTEGER, "is_int");
+      addOperator(api::TO_REAL, "to_real");
     }
 
     if (d_logic.areTranscendentalsUsed())
     {
-      addTheory(THEORY_TRANSCENDENTALS);
+      defineVar("real.pi", d_solver->mkTerm(api::PI));
+      addTranscendentalOperators();
     }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
-    addTheory(THEORY_ARRAYS);
+    addOperator(api::SELECT, "select");
+    addOperator(api::STORE, "store");
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
-    addTheory(THEORY_BITVECTORS);
+    addBitvectorOperators();
+
+    if (!strictModeEnabled() && d_logic.isTheoryEnabled(theory::THEORY_ARITH)
+        && d_logic.areIntegersUsed())
+    {
+      // Conversions between bit-vectors and integers
+      addOperator(api::BITVECTOR_TO_NAT, "bv2nat");
+      addIndexedOperator(
+          api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
+    }
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
-    addTheory(THEORY_DATATYPES);
+    const std::vector<api::Sort> types;
+    defineType("Tuple", d_solver->mkTupleSort(types));
+    addDatatypesOperators();
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
-    addTheory(THEORY_SETS);
+    defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort()));
+    // the Boolean sort is a placeholder here since we don't have type info
+    // without type annotation
+    defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+
+    addOperator(api::UNION, "union");
+    addOperator(api::INTERSECTION, "intersection");
+    addOperator(api::SETMINUS, "setminus");
+    addOperator(api::SUBSET, "subset");
+    addOperator(api::MEMBER, "member");
+    addOperator(api::SINGLETON, "singleton");
+    addOperator(api::INSERT, "insert");
+    addOperator(api::CARD, "card");
+    addOperator(api::COMPLEMENT, "complement");
+    addOperator(api::JOIN, "join");
+    addOperator(api::PRODUCT, "product");
+    addOperator(api::TRANSPOSE, "transpose");
+    addOperator(api::TCLOSURE, "tclosure");
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
-    addTheory(THEORY_STRINGS);
+    defineType("String", d_solver->getStringSort());
+    defineType("RegLan", d_solver->getRegExpSort());
+    defineType("Int", d_solver->getIntegerSort());
+
+    if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+    {
+      defineVar("re.none", d_solver->mkRegexpEmpty());
+    }
+    else
+    {
+      defineVar("re.nostr", d_solver->mkRegexpEmpty());
+    }
+    defineVar("re.allchar", d_solver->mkRegexpSigma());
+
+    addStringOperators();
   }
 
   if(d_logic.isQuantified()) {
-    addTheory(THEORY_QUANTIFIERS);
+    addQuantifiersOperators();
   }
 
   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
-    addTheory(THEORY_FP);
+    defineType("RoundingMode", d_solver->getRoundingmodeSort());
+    defineType("Float16", d_solver->mkFloatingPointSort(5, 11));
+    defineType("Float32", d_solver->mkFloatingPointSort(8, 24));
+    defineType("Float64", d_solver->mkFloatingPointSort(11, 53));
+    defineType("Float128", d_solver->mkFloatingPointSort(15, 113));
+
+    defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+    defineVar("roundNearestTiesToEven",
+              d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
+    defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+    defineVar("roundNearestTiesToAway",
+              d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
+    defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
+    defineVar("roundTowardPositive",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
+    defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
+    defineVar("roundTowardNegative",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
+    defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
+    defineVar("roundTowardZero",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
+
+    addFloatingPointOperators();
   }
 
   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
-    addTheory(THEORY_SEP);
+    // the Boolean sort is a placeholder here since we don't have type info
+    // without type annotation
+    defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
+
+    addSepOperators();
   }
 
   Command* cmd =
@@ -871,6 +787,28 @@ void Smt2::checkThatLogicIsSet()
   }
 }
 
+void Smt2::checkLogicAllowsFreeSorts()
+{
+  if (!d_logic.isTheoryEnabled(theory::THEORY_UF)
+      && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)
+      && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)
+      && !d_logic.isTheoryEnabled(theory::THEORY_SETS))
+  {
+    parseErrorLogic("Free sort symbols not allowed in ");
+  }
+}
+
+void Smt2::checkLogicAllowsFunctions()
+{
+  if (!d_logic.isTheoryEnabled(theory::THEORY_UF))
+  {
+    parseError(
+        "Functions (of non-zero arity) cannot "
+        "be declared in logic "
+        + d_logic.getLogicString() + " unless option --uf-ho is used");
+  }
+}
+
 /* The include are managed in the lexer but called in the parser */
 // Inspired by http://www.antlr3.org/api/C/interop.html
 

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 6d3c2e6f60fc01c85a8623ef136c8e8ed9f1efcc..0400c680f52c10c4d812fe3fcd81626048c845a4 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -46,25 +46,6 @@ class Smt2 : public Parser
 {
   friend class ParserBuilder;
 
- public:
-  enum Theory
-  {
-    THEORY_ARRAYS,
-    THEORY_BITVECTORS,
-    THEORY_CORE,
-    THEORY_DATATYPES,
-    THEORY_INTS,
-    THEORY_REALS,
-    THEORY_TRANSCENDENTALS,
-    THEORY_REALS_INTS,
-    THEORY_QUANTIFIERS,
-    THEORY_SETS,
-    THEORY_STRINGS,
-    THEORY_UF,
-    THEORY_FP,
-    THEORY_SEP
-  };
-
  private:
   /** Has the logic been set (either by forcing it or a set-logic command)? */
   bool d_logicSet;
@@ -91,11 +72,9 @@ class Smt2 : public Parser
 
  public:
   /**
-   * Add theory symbols to the parser state.
-   *
-   * @param theory the theory to open (e.g., Core, Ints)
+   * Add core theory symbols to the parser state.
    */
-  void addTheory(Theory theory);
+  void addCoreSymbols();
 
   void addOperator(api::Kind k, const std::string& name);
 
@@ -117,7 +96,7 @@ class Smt2 : public Parser
 
   bool isOperatorEnabled(const std::string& name) const;
 
-  bool isTheoryEnabled(Theory theory) const;
+  bool isTheoryEnabled(theory::TheoryId theory) const;
 
   bool logicIsSet() override;
 
@@ -312,6 +291,19 @@ class Smt2 : public Parser
 
   void checkThatLogicIsSet();
 
+  /**
+   * Checks whether the current logic allows free sorts. If the logic does not
+   * support free sorts, the function triggers a parse error.
+   */
+  void checkLogicAllowsFreeSorts();
+
+  /**
+   * Checks whether the current logic allows functions of non-zero arity. If
+   * the logic does not support such functions, the function triggers a parse
+   * error.
+   */
+  void checkLogicAllowsFunctions();
+
   void checkUserSymbol(const std::string& name) {
     if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) {
       std::stringstream ss;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bffb2c4db6d8308413338c0421d92c776ff91c98..0ea6114352a293b26ab9b9c9d8142cae84efe747 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -608,6 +608,7 @@ set(regress_0_tests
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
+  regress0/parser/bv_nat.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
   regress0/parser/force_logic_set_logic.smt2

diff --git a/test/regress/regress0/parser/bv_nat.smt2 b/test/regress/regress0/parser/bv_nat.smt2
new file mode 100644 (file)
index 0000000..fc21408
--- /dev/null
+++ b/test/regress/regress0/parser/bv_nat.smt2
@@ -0,0 +1,13 @@
+; EXPECT: sat
+; EXPECT: not declared
+; SCRUBBER: grep -o "sat\|not declared"
+; EXIT: 1
+(set-logic QF_BVLIA)
+(declare-const x (_ BitVec 4))
+(assert (= (bv2nat x) 0))
+(check-sat)
+(reset)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 4))
+(assert (= (bv2nat x) 0))
+(check-sat)

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 85b379ac05b069b9728a98460a3383a43e7933e8..a829d9a8d61b7611957951de99e7c6981a1e491b 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -316,9 +316,6 @@ public:
 
   void setupContext(Parser& parser) override
   {
-    if(dynamic_cast<Smt2*>(&parser) != NULL){
-      dynamic_cast<Smt2*>(&parser)->addTheory(Smt2::THEORY_CORE);
-    }
     super::setupContext(parser);
   }