diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c72a4f99b..00f2e944d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -407,6 +407,8 @@ command [std::unique_ptr<CVC4::Command>* cmd] ExprManager::VAR_FLAG_DEFINED, true); cmd->reset(new DefineFunctionCommand(name, func, terms, expr)); } + | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] + | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -1211,9 +1213,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] * --smtlib2 compliance mode. */ : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd] | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] - | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] - | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | rewriterulesCommand[cmd] @@ -1886,7 +1886,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Kind lassocKind = CVC4::kind::UNDEFINED_KIND; if (args.size() >= 2) { - if (kind == CVC4::kind::INTS_DIVISION) + if (kind == CVC4::kind::INTS_DIVISION + || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) { // Builtin operators that are not tokenized, are left associative, // but not internally variadic must set this. @@ -2306,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm] sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { - api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type)); - api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2)); + api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1"); + api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } |