From: Morgan Deters 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)