diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 2 | ||||
-rw-r--r-- | src/expr/dtype_cons.cpp | 2 | ||||
-rw-r--r-- | src/expr/dtype_selector.cpp | 2 | ||||
-rw-r--r-- | src/main/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 5 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 12 | ||||
-rw-r--r-- | src/options/language.cpp | 13 | ||||
-rw-r--r-- | src/options/language.h | 2 | ||||
-rw-r--r-- | src/parser/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 7 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 2459 | ||||
-rw-r--r-- | src/parser/cvc/README | 98 | ||||
-rw-r--r-- | src/parser/cvc/cvc.cpp | 37 | ||||
-rw-r--r-- | src/parser/cvc/cvc.h | 51 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 77 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 79 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 1558 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 208 | ||||
-rw-r--r-- | src/printer/printer.cpp | 4 |
22 files changed, 12 insertions, 4625 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9b2e2e8e2..3113f03ab 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -149,8 +149,6 @@ libcvc5_add_sources( preprocessing/util/ite_utilities.h printer/ast/ast_printer.cpp printer/ast/ast_printer.h - printer/cvc/cvc_printer.cpp - printer/cvc/cvc_printer.h printer/let_binding.cpp printer/let_binding.h printer/printer.cpp diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index fdb397d39..d8ec0cb61 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -910,8 +910,6 @@ std::unordered_set<TypeNode> DType::getSubfieldTypes() const std::ostream& operator<<(std::ostream& os, const DType& dt) { - // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, Language::LANG_CVC); dt.toStream(os); return os; } diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 3603c776a..ddb88499b 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -684,8 +684,6 @@ void DTypeConstructor::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor) { - // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, Language::LANG_CVC); ctor.toStream(os); return os; } diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index 1898a4186..30c9057f1 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -83,8 +83,6 @@ void DTypeSelector::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg) { - // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, Language::LANG_CVC); arg.toStream(os); return os; } diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 27086d3fb..8ce0ba754 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -127,7 +127,6 @@ endforeach() # Create target used as a dependency for libmain. add_custom_target(gen-tokens DEPENDS - cvc_tokens.h smt2_tokens.h tptp_tokens.h ) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index ec3e10b5e..de7566b1f 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -143,7 +143,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - solver->setOption("input-language", "cvc"); + solver->setOption("input-language", "smt2"); } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { @@ -151,9 +151,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { solver->setOption("input-language", "tptp"); - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - solver->setOption("input-language", "cvc"); } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 86f344979..d5759db1b 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -66,10 +66,6 @@ using __gnu_cxx::stdio_filebuf; char** commandCompletion(const char* text, int start, int end); char* commandGenerator(const char* text, int state); -static const std::string cvc_commands[] = { -#include "main/cvc_tokens.h" -};/* cvc_commands */ - static const std::string smt2_commands[] = { #include "main/smt2_tokens.h" };/* smt2_commands */ @@ -112,13 +108,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, ::using_history(); std::string lang = solver->getOption("input-language"); - if (lang == "LANG_CVC") - { - d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; - commandsBegin = cvc_commands; - commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); - } - else if (lang == "LANG_TPTP") + if (lang == "LANG_TPTP") { d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; commandsBegin = tptp_commands; diff --git a/src/options/language.cpp b/src/options/language.cpp index 041debd67..6170bcf28 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -26,7 +26,6 @@ std::ostream& operator<<(std::ostream& out, Language lang) case Language::LANG_AUTO: out << "LANG_AUTO"; break; case Language::LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; case Language::LANG_TPTP: out << "LANG_TPTP"; break; - case Language::LANG_CVC: out << "LANG_CVC"; break; case Language::LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; default: out << "undefined_language"; } @@ -37,15 +36,9 @@ namespace language { Language toLanguage(const std::string& language) { - if (language == "cvc" || language == "pl" || language == "presentation" - || language == "native" || language == "LANG_CVC") - { - return Language::LANG_CVC; - } - else if (language == "smtlib" || language == "smt" || language == "smtlib2" - || language == "smt2" || language == "smtlib2.6" - || language == "smt2.6" || language == "LANG_SMTLIB_V2_6" - || language == "LANG_SMTLIB_V2") + if (language == "smtlib" || language == "smt" || language == "smtlib2" + || language == "smt2" || language == "smtlib2.6" || language == "smt2.6" + || language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") { return Language::LANG_SMTLIB_V2_6; } diff --git a/src/options/language.h b/src/options/language.h index 6031a6487..05756f98f 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -36,8 +36,6 @@ enum class CVC5_EXPORT Language LANG_SMTLIB_V2_6 = 0, /** The TPTP language */ LANG_TPTP, - /** The cvc5 language */ - LANG_CVC, /** The SyGuS language version 2.0 */ LANG_SYGUS_V2, diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index f2596ceeb..589bfad1f 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -32,10 +32,6 @@ set(libcvc5parser_src_files bounded_token_buffer.h bounded_token_factory.cpp bounded_token_factory.h - cvc/cvc.cpp - cvc/cvc.h - cvc/cvc_input.cpp - cvc/cvc_input.h input.cpp input.h line_buffer.cpp @@ -66,7 +62,7 @@ set(libcvc5parser_src_files #-----------------------------------------------------------------------------# # Generate parsers for all supported languages -foreach(lang Cvc Smt2 Tptp) +foreach(lang Smt2 Tptp) string(TOLOWER ${lang} lang_dir) file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}) add_custom_command( diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index c190fe7f0..89d56a108 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -23,7 +23,6 @@ #include "parser/antlr_line_buffered_input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" -#include "parser/cvc/cvc_input.h" #include "parser/input.h" #include "parser/memory_mapped_input_buffer.h" #include "parser/parser.h" @@ -188,11 +187,7 @@ AntlrInputStream::newStringInputStream(const std::string& input, AntlrInput* AntlrInput::newInput(const std::string& lang, AntlrInputStream& inputStream) { - if (lang == "LANG_CVC") - { - return new CvcInput(inputStream); - } - else if (lang == "LANG_SYGUS_V2") + if (lang == "LANG_SYGUS_V2") { return new SygusInput(inputStream); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g deleted file mode 100644 index a01753b56..000000000 --- a/src/parser/cvc/Cvc.g +++ /dev/null @@ -1,2459 +0,0 @@ -/* **************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Parser for CVC presentation input language. - */ - -grammar Cvc; - -options { - // C output for antlr - language = 'C'; - - // Skip the default error handling, just break with exceptions - // defaultErrorHandler = false; - - // Only lookahead of <= k requested (disable for LL* parsing) - // Note that cvc5's BoundedTokenBuffer requires a fixed k ! - // If you change this k, change it also in cvc_input.cpp ! - k = 3; -}/* options */ - -tokens { - /* commands */ - - ASSERT_TOK = 'ASSERT'; - QUERY_TOK = 'QUERY'; - CHECKSAT_TOK = 'CHECKSAT'; - OPTION_TOK = 'OPTION'; - PUSH_TOK = 'PUSH'; - POP_TOK = 'POP'; - POPTO_TOK = 'POPTO'; - PUSH_SCOPE_TOK = 'PUSH_SCOPE'; - POP_SCOPE_TOK = 'POP_SCOPE'; - POPTO_SCOPE_TOK = 'POPTO_SCOPE'; - RESET_TOK = 'RESET'; - DATATYPE_TOK = 'DATATYPE'; - END_TOK = 'END'; - CONTEXT_TOK = 'CONTEXT'; - FORGET_TOK = 'FORGET'; - GET_TYPE_TOK = 'GET_TYPE'; - CHECK_TYPE_TOK = 'CHECK_TYPE'; - GET_CHILD_TOK = 'GET_CHILD'; - GET_OP_TOK = 'GET_OP'; - GET_VALUE_TOK = 'GET_VALUE'; - SUBSTITUTE_TOK = 'SUBSTITUTE'; - DBG_TOK = 'DBG'; - TRACE_TOK = 'TRACE'; - UNTRACE_TOK = 'UNTRACE'; - HELP_TOK = 'HELP'; - TRANSFORM_TOK = 'TRANSFORM'; - PRINT_TOK = 'PRINT'; - PRINT_TYPE_TOK = 'PRINT_TYPE'; - CALL_TOK = 'CALL'; - ECHO_TOK = 'ECHO'; - EXIT_TOK = 'EXIT'; - INCLUDE_TOK = 'INCLUDE'; - DUMP_PROOF_TOK = 'DUMP_PROOF'; - DUMP_UNSAT_CORE_TOK = 'DUMP_UNSAT_CORE'; - DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS'; - DUMP_SIG_TOK = 'DUMP_SIG'; - DUMP_TCC_TOK = 'DUMP_TCC'; - DUMP_TCC_ASSUMPTIONS_TOK = 'DUMP_TCC_ASSUMPTIONS'; - DUMP_TCC_PROOF_TOK = 'DUMP_TCC_PROOF'; - DUMP_CLOSURE_TOK = 'DUMP_CLOSURE'; - DUMP_CLOSURE_PROOF_TOK = 'DUMP_CLOSURE_PROOF'; - WHERE_TOK = 'WHERE'; - ASSERTIONS_TOK = 'ASSERTIONS'; - ASSUMPTIONS_TOK = 'ASSUMPTIONS'; - COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE'; - COUNTERMODEL_TOK = 'COUNTERMODEL'; - ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER'; - CONTINUE_TOK = 'CONTINUE'; - RESTART_TOK = 'RESTART'; - RECURSIVE_FUNCTION_TOK = 'REC-FUN'; - /* operators */ - - AND_TOK = 'AND'; - BOOLEAN_TOK = 'BOOLEAN'; - ELSEIF_TOK = 'ELSIF'; - ELSE_TOK = 'ELSE'; - ENDIF_TOK = 'ENDIF'; - FALSE_TOK = 'FALSE'; - IF_TOK = 'IF'; - IN_TOK = 'IN'; - INT_TOK = 'INT'; - LET_TOK = 'LET'; - MEMBER_TOK = 'IS_IN'; - NOT_TOK = 'NOT'; - OR_TOK = 'OR'; - REAL_TOK = 'REAL'; - THEN_TOK = 'THEN'; - TRUE_TOK = 'TRUE'; - TYPE_TOK = 'TYPE'; - XOR_TOK = 'XOR'; - - ARRAY_TOK = 'ARRAY'; - OF_TOK = 'OF'; - WITH_TOK = 'WITH'; - - SUBTYPE_TOK = 'SUBTYPE'; - SET_TOK = 'SET'; - - TUPLE_TOK = 'TUPLE'; - - FORALL_TOK = 'FORALL'; - EXISTS_TOK = 'EXISTS'; - PATTERN_TOK = 'PATTERN'; - - LAMBDA_TOK = 'LAMBDA'; - - // Symbols - - COLON = ':'; - COMMA = ','; - LPAREN = '('; - RPAREN = ')'; - LBRACE = '{'; - RBRACE = '}'; - LBRACKET = '['; - RBRACKET = ']'; - SEMICOLON = ';'; - BAR = '|'; - UNDERSCORE = '_'; - - SQHASH = '[#'; - HASHSQ = '#]'; - PARENHASH = '(#'; - HASHPAREN = '#)'; - - // Operators - - ARROW_TOK = '->'; - DIV_TOK = '/'; - EQUAL_TOK = '='; - DISEQUAL_TOK = '/='; - EXP_TOK = '^'; - GT_TOK = '>'; - GEQ_TOK = '>='; - IFF_TOK = '<=>'; - IMPLIES_TOK = '=>'; - LT_TOK = '<'; - LEQ_TOK = '<='; - MINUS_TOK = '-'; - PLUS_TOK = '+'; - STAR_TOK = '*'; - ASSIGN_TOK = ':='; - MOD_TOK = 'MOD'; - INTDIV_TOK = 'DIV'; - FLOOR_TOK = 'FLOOR'; - ABS_TOK = 'ABS'; - DIVISIBLE_TOK = 'DIVISIBLE'; - DISTINCT_TOK = 'DISTINCT'; - - // Bitvectors - - BITVECTOR_TOK = 'BITVECTOR'; - LEFTSHIFT_TOK = '<<'; - RIGHTSHIFT_TOK = '>>'; - BVPLUS_TOK = 'BVPLUS'; - BVSUB_TOK = 'BVSUB'; - BVUDIV_TOK = 'BVUDIV'; - BVSDIV_TOK = 'BVSDIV'; - BVUREM_TOK = 'BVUREM'; - BVSREM_TOK = 'BVSREM'; - BVSMOD_TOK = 'BVSMOD'; - BVSHL_TOK = 'BVSHL'; - BVASHR_TOK = 'BVASHR'; - BVLSHR_TOK = 'BVLSHR'; - BVUMINUS_TOK = 'BVUMINUS'; - BVMULT_TOK = 'BVMULT'; - BVNEG_TOK = '~'; - BVAND_TOK = '&'; - BVXOR_TOK = 'BVXOR'; - BVNAND_TOK = 'BVNAND'; - BVNOR_TOK = 'BVNOR'; - BVCOMP_TOK = 'BVCOMP'; - BVXNOR_TOK = 'BVXNOR'; - CONCAT_TOK = '@'; - //BVTOINT_TOK = 'BVTOINT'; - //INTTOBV_TOK = 'INTTOBV'; - //BOOLEXTRACT_TOK = 'BOOLEXTRACT'; - IS_INTEGER_TOK = 'IS_INTEGER'; - BVLT_TOK = 'BVLT'; - BVGT_TOK = 'BVGT'; - BVLE_TOK = 'BVLE'; - BVGE_TOK = 'BVGE'; - SX_TOK = 'SX'; - BVZEROEXTEND_TOK = 'BVZEROEXTEND'; - BVREPEAT_TOK = 'BVREPEAT'; - BVROTL_TOK = 'BVROTL'; - BVROTR_TOK = 'BVROTR'; - BVSLT_TOK = 'BVSLT'; - BVSGT_TOK = 'BVSGT'; - BVSLE_TOK = 'BVSLE'; - BVSGE_TOK = 'BVSGE'; - - // Sets - SETS_CHOOSE_TOK = 'CHOOSE'; - - // Relations - JOIN_TOK = 'JOIN'; - TRANSPOSE_TOK = 'TRANSPOSE'; - PRODUCT_TOK = 'PRODUCT'; - TRANSCLOSURE_TOK = 'TCLOSURE'; - IDEN_TOK = 'IDEN'; - JOIN_IMAGE_TOK = 'JOIN_IMAGE'; - - // Strings - STRING_TOK = 'STRING'; - STRING_CONCAT_TOK = 'CONCAT'; - STRING_LENGTH_TOK = 'LENGTH'; - STRING_CONTAINS_TOK = 'CONTAINS'; - STRING_SUBSTR_TOK = 'SUBSTR'; - STRING_CHARAT_TOK = 'CHARAT'; - STRING_INDEXOF_TOK = 'INDEXOF'; - STRING_REPLACE_TOK = 'REPLACE'; - STRING_REPLACE_ALL_TOK = 'REPLACE_ALL'; - STRING_PREFIXOF_TOK = 'PREFIXOF'; - STRING_SUFFIXOF_TOK = 'SUFFIXOF'; - STRING_STOI_TOK = 'STRING_TO_INTEGER'; - STRING_ITOS_TOK = 'INTEGER_TO_STRING'; - STRING_TO_REGEXP_TOK = 'STRING_TO_REGEXP'; - STRING_TOLOWER_TOK = 'TOLOWER'; - STRING_TOUPPER_TOK = 'TOUPPER'; - STRING_REV_TOK = 'REVERSE'; - REGEXP_CONCAT_TOK = 'RE_CONCAT'; - REGEXP_UNION_TOK = 'RE_UNION'; - REGEXP_INTER_TOK = 'RE_INTER'; - REGEXP_STAR_TOK = 'RE_STAR'; - REGEXP_PLUS_TOK = 'RE_PLUS'; - REGEXP_OPT_TOK = 'RE_OPT'; - REGEXP_RANGE_TOK = 'RE_RANGE'; - REGEXP_LOOP_TOK = 'RE_LOOP'; - REGEXP_EMPTY_TOK = 'RE_EMPTY'; - REGEXP_SIGMA_TOK = 'RE_SIGMA'; - REGEXP_COMPLEMENT_TOK = 'RE_COMPLEMENT'; - SEQ_UNIT_TOK = 'SEQ_UNIT'; - - SETS_CARD_TOK = 'CARD'; - - FMF_CARD_TOK = 'HAS_CARD'; - UNIVSET_TOK = 'UNIVERSE'; - - // these are parsed by special NUMBER_OR_RANGEOP rule, below - DECIMAL_LITERAL; - INTEGER_LITERAL; - DOT; - DOTDOT; -}/* tokens */ - -@parser::members { - -// Idea and code guidance from Sam Harwell, -// http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser - -bool isRightToLeft(int type) { - // return true here for any operators that are right-to-left associative - switch(type) { - case IMPLIES_TOK: return true; - default: return false; - } -}/* isRightToLeft() */ - -int getOperatorPrecedence(int type) { - switch(type) { - case BITVECTOR_TOK: return 1; - //case DOT: - case LPAREN: - case LBRACE: return 2; - case LBRACKET: return 3; - case ARROW_TOK: return 4; - case IS_INTEGER_TOK: return 5; - case BVSLT_TOK: - case BVSLE_TOK: - case BVSGT_TOK: - case BVSGE_TOK: return 6; - case BVLT_TOK: - case BVLE_TOK: - case BVGT_TOK: - case BVGE_TOK: return 7; - case LEFTSHIFT_TOK: - case RIGHTSHIFT_TOK: return 8; - case SX_TOK: - case BVZEROEXTEND_TOK: - case BVREPEAT_TOK: - case BVROTL_TOK: - case BVROTR_TOK: return 9; - case BVUDIV_TOK: - case BVSDIV_TOK: - case BVUREM_TOK: - case BVSREM_TOK: - case BVSMOD_TOK: - case BVSHL_TOK: - case BVASHR_TOK: - case BVLSHR_TOK: return 10; - case BVUMINUS_TOK: - case BVPLUS_TOK: - case BVSUB_TOK: return 11; - case BVNEG_TOK: return 12; - case BVXNOR_TOK: return 13; - case BVNOR_TOK: - case BVCOMP_TOK: return 14; - case BVNAND_TOK: return 15; - case BVXOR_TOK: return 16; - case BVAND_TOK: return 17; - case BAR: return 18; - case CONCAT_TOK: return 19; -//case UMINUS_TOK: return 20; - case WITH_TOK: return 21; - case EXP_TOK: return 22; - case STAR_TOK: - case INTDIV_TOK: - case DIV_TOK: - case TUPLE_TOK: - case MOD_TOK: return 23; - case PLUS_TOK: - case MINUS_TOK: - case JOIN_TOK: - case TRANSPOSE_TOK: - case PRODUCT_TOK: - case IDEN_TOK: - case JOIN_IMAGE_TOK: - case TRANSCLOSURE_TOK: - case SETS_CHOOSE_TOK: return 24; - case LEQ_TOK: - case LT_TOK: - case GEQ_TOK: - case GT_TOK: - case MEMBER_TOK: - case SETS_CARD_TOK: - case FMF_CARD_TOK: return 25; - case EQUAL_TOK: - case DISEQUAL_TOK: return 26; - case NOT_TOK: return 27; - case AND_TOK: return 28; - case OR_TOK: - case XOR_TOK: return 29; - case IMPLIES_TOK: return 30;// right-to-left - case IFF_TOK: return 31; - case FORALL_TOK: - case EXISTS_TOK:return 32; - case ASSIGN_TOK: - case IN_TOK: return 33; - - default: - std::stringstream ss; - ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type]; - throw ParserException(ss.str()); - } -}/* getOperatorPrecedence() */ - -api::Kind getOperatorKind(int type, bool& negate) { - negate = false; - - switch(type) { - // booleanBinop - case IFF_TOK: return api::EQUAL; - case IMPLIES_TOK: return api::IMPLIES; - case OR_TOK: return api::OR; - case XOR_TOK: return api::XOR; - case AND_TOK: return api::AND; - - case SETS_CHOOSE_TOK: return api::CHOOSE; - case PRODUCT_TOK: return api::PRODUCT; - case JOIN_TOK: return api::JOIN; - case JOIN_IMAGE_TOK: return api::JOIN_IMAGE; - - - // comparisonBinop - case EQUAL_TOK: return api::EQUAL; - case DISEQUAL_TOK: negate = true; return api::EQUAL; - case GT_TOK: return api::GT; - case GEQ_TOK: return api::GEQ; - case LT_TOK: return api::LT; - case LEQ_TOK: return api::LEQ; - case MEMBER_TOK: return api::MEMBER; - case SETS_CARD_TOK: return api::CARD; - case FMF_CARD_TOK: return api::CARDINALITY_CONSTRAINT; - - // arithmeticBinop - case PLUS_TOK: return api::PLUS; - case MINUS_TOK: return api::MINUS; - case STAR_TOK: return api::MULT; - case INTDIV_TOK: return api::INTS_DIVISION; - case MOD_TOK: return api::INTS_MODULUS; - case DIV_TOK: return api::DIVISION; - case EXP_TOK: return api::POW; - - // bvBinop - case CONCAT_TOK: return api::BITVECTOR_CONCAT; - case BAR: return api::BITVECTOR_OR; - case BVAND_TOK: return api::BITVECTOR_AND; - - } - - std::stringstream ss; - ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type]; - throw ParserException(ss.str()); - -}/* getOperatorKind() */ - -unsigned findPivot(const std::vector<unsigned>& operators, - unsigned startIndex, unsigned stopIndex) { - unsigned pivot = startIndex; - unsigned pivotRank = getOperatorPrecedence(operators[pivot]); - /*Debug("prec") << "initial pivot at " << pivot - << "(" << CvcParserTokenNames[operators[pivot]] << ") " - << "level " << pivotRank << std::endl;*/ - for(unsigned i = startIndex + 1; i <= stopIndex; ++i) { - unsigned current = getOperatorPrecedence(operators[i]); - bool rtl = isRightToLeft(operators[i]); - if(current > pivotRank || (current == pivotRank && !rtl)) { - /*Debug("prec") << "new pivot at " << i - << "(" << CvcParserTokenNames[operators[i]] << ") " - << "level " << current << " rtl == " << rtl << std::endl;*/ - pivot = i; - pivotRank = current; - } - } - return pivot; -}/* findPivot() */ - -cvc5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, - const std::vector<cvc5::api::Term>& expressions, - const std::vector<unsigned>& operators, - unsigned startIndex, unsigned stopIndex) { - Assert(expressions.size() == operators.size() + 1); - Assert(startIndex < expressions.size()); - Assert(stopIndex < expressions.size()); - Assert(startIndex <= stopIndex); - - if(stopIndex == startIndex) { - return expressions[startIndex]; - } - - unsigned pivot = findPivot(operators, startIndex, stopIndex - 1); - //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; - bool negate; - api::Kind k = getOperatorKind(operators[pivot], negate); - cvc5::api::Term lhs = createPrecedenceTree( - parser, solver, expressions, operators, startIndex, pivot); - cvc5::api::Term rhs = createPrecedenceTree( - parser, solver, expressions, operators, pivot + 1, stopIndex); - - if (lhs.getSort().isSet()) - { - switch (k) - { - case api::LEQ: k = api::SUBSET; break; - case api::MINUS: k = api::SETMINUS; break; - case api::BITVECTOR_AND: k = api::INTERSECTION; break; - case api::BITVECTOR_OR: k = api::UNION; break; - default: break; - } - } - else if (lhs.getSort().isString()) - { - switch (k) - { - case api::MEMBER: k = api::STRING_IN_REGEXP; break; - default: break; - } - } - - api::Term e = solver->mkTerm(k, lhs, rhs); - return negate ? e.notTerm() : e; -}/* createPrecedenceTree() recursive variant */ - -api::Term createPrecedenceTree(Parser* parser, api::Solver* s, - const std::vector<cvc5::api::Term>& expressions, - const std::vector<unsigned>& operators) { - if(Debug.isOn("prec") && operators.size() > 1) { - for(unsigned i = 0; i < expressions.size(); ++i) { - Debug("prec") << expressions[i]; - if(operators.size() > i) { - Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' '; - } - } - Debug("prec") << std::endl; - } - - api::Term e = createPrecedenceTree( - parser, s, expressions, operators, 0, expressions.size() - 1); - if(Debug.isOn("prec") && operators.size() > 1) { - language::SetLanguage::Scope ls(Debug("prec"), Language::LANG_AST); - Debug("prec") << "=> " << e << std::endl; - } - return e; -}/* createPrecedenceTree() base variant */ - -/** Add n NOTs to the front of e and return the result. */ -api::Term addNots(api::Solver* s, size_t n, api::Term e) { - while(n-- > 0) { - e = e.notTerm(); - } - return e; -}/* addNots() */ - -}/* @parser::members */ - -@header { -/* **************************************************************************** - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - */ -}/* @header */ - -@lexer::includes { - -/** This suppresses warnings about the redefinition of token symbols between different - * parsers. The redefinitions should be harmless as long as no client: (a) #include's - * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ -#pragma GCC system_header - -#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK) -/* This improves performance by ~10 percent on big inputs. - * This option is only valid if we know the input is ASCII (or some 8-bit encoding). - * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. - * Otherwise, we have to let the lexer detect the encoding at runtime. - */ -# define ANTLR3_INLINE_INPUT_ASCII -# define ANTLR3_INLINE_INPUT_8BIT -#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ - -#include "parser/antlr_input.h" -#include "parser/antlr_tracing.h" -#include "parser/parser.h" - -}/* @lexer::includes */ - -@parser::includes { - -#include <memory> - -#include "base/check.h" -#include "options/set_language.h" -#include "parser/antlr_tracing.h" -#include "parser/parser.h" -#include "smt/command.h" - -namespace cvc5 { - class Expr; -}/* cvc5 namespace */ - -}/* @parser::includes */ - -@parser::postinclude { - -#include <sstream> -#include <string> -#include <vector> - -#include "base/output.h" -#include "parser/antlr_input.h" -#include "parser/parser.h" - -#define REPEAT_COMMAND(k, CommandCtor) \ - ({ \ - unsigned __k = (k); \ - (__k <= 1) \ - ? (Command*) new CommandCtor \ - : ({ \ - CommandSequence* __seq = new CommandSequence(); \ - while(__k-- > 0) { \ - __seq->addCommand(new CommandCtor); \ - } \ - (Command*) __seq; \ - }); \ - }) - -using namespace cvc5; -using namespace cvc5::parser; - -/* These need to be macros so they can refer to the PARSER macro, which will be defined - * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ -#undef PARSER_STATE -#define PARSER_STATE ((Parser*)PARSER->super) -#undef SOLVER -#define SOLVER PARSER_STATE->getSolver() -#undef MK_TERM -#define MK_TERM SOLVER->mkTerm -#define UNSUPPORTED PARSER_STATE->unimplementedFeature - -#define ENSURE_BV_SIZE(k, f) \ -{ \ - unsigned size = f.getSort().getBVSize(); \ - if(k > size) { \ - f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_ZERO_EXTEND,k - size), f); \ - } else if (k < size) { \ - f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_EXTRACT, k - 1, 0), f); \ - } \ -} - -}/* @parser::postinclude */ - -/** - * Parses an expression. - * @return the parsed expression - */ -parseExpr returns [cvc5::api::Term expr = cvc5::api::Term()] - : formula[expr] - | EOF - ; - -/** - * Parses a command (the whole benchmark) - * @return the command of the benchmark - */ -parseCommand returns [cvc5::Command* cmd_return = NULL] -@declarations { - std::unique_ptr<cvc5::Command> cmd; -} -@after { - cmd_return = cmd.release(); -} - : c=command[&cmd] - | LPAREN IDENTIFIER - { std::string s = AntlrInput::tokenText($IDENTIFIER); - if(s == "benchmark") { - PARSER_STATE->parseError( - "In cvc5 presentation language mode, but SMT-LIBv1 format " - "detected, which is not supported anymore."); - } else if(s == "set" || s == "get" || s == "declare" || - s == "define" || s == "assert") { - PARSER_STATE->parseError( - "In cvc5 presentation language mode, but SMT-LIB format detected. " - "Use --lang smt for SMT-LIB support."); - } else { - PARSER_STATE->parseError( - "A cvc5 presentation language command cannot begin with a " - "parenthesis; expected command name."); - } - } - | EOF - ; - -/** - * Matches a command of the input. If a declaration, it will return an empty - * command. - */ -command [std::unique_ptr<cvc5::Command>* cmd] - : ( mainCommand[cmd] SEMICOLON - | SEMICOLON - | LET_TOK { PARSER_STATE->pushScope(); } - typeOrVarLetDecl[CHECK_DECLARED] ( - COMMA typeOrVarLetDecl[CHECK_DECLARED] )* - IN_TOK command[cmd] - { PARSER_STATE->popScope(); } - ) - { if(!(*cmd)) { - cmd->reset(new EmptyCommand()); - } - } - | IDENTIFIER SEMICOLON - { std::stringstream ss; - ss << "Unrecognized command `" - << AntlrInput::tokenText($IDENTIFIER) - << "'"; - PARSER_STATE->parseError(ss.str()); - } - ; - -typeOrVarLetDecl[cvc5::parser::DeclarationCheck check] -options { backtrack = true; } - : letDecl | typeLetDecl[check] - ; - -mainCommand[std::unique_ptr<cvc5::Command>* cmd] -@init { - api::Term f; - api::Term sexpr; - std::string id; - api::Sort t; - std::vector<cvc5::api::DatatypeDecl> dts; - Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; - std::string s; - api::Term func; - std::vector<api::Term> bvs; - std::vector<api::Term> funcs; - std::vector<api::Term> formulas; - std::vector<std::vector<api::Term>> formals; - std::vector<std::string> ids; - std::vector<cvc5::api::Sort> types; - bool idCommaFlag = true; - bool formCommaFlag = true; -} - /* our bread & butter */ - : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); } - - | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f)); } - | CHECKSAT_TOK formula[f]? - { - cmd->reset(f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f)); - } - /* options */ - | OPTION_TOK - ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - ( symbolicExpr[sexpr] - { if(s == "logic") { - cmd->reset(new SetBenchmarkLogicCommand(sexprToString(sexpr))); - } else { - cmd->reset(new SetOptionCommand(s, sexprToString(sexpr))); - } - } - | TRUE_TOK { cmd->reset(new SetOptionCommand(s, "true")); } - | FALSE_TOK { cmd->reset(new SetOptionCommand(s, "false")); } - | { cmd->reset(new SetOptionCommand(s, "true")); } - ) - - /* push / pop */ - | PUSH_TOK ( k=numeral { cmd->reset(REPEAT_COMMAND(k, PushCommand())); } - | { cmd->reset(new PushCommand()); } ) - | POP_TOK ( k=numeral { cmd->reset(REPEAT_COMMAND(k, PopCommand())); } - | { cmd->reset(new PopCommand()); } ) - | POPTO_TOK k=numeral? - { UNSUPPORTED("POPTO command"); } - - /* push / pop scopes */ - | PUSH_SCOPE_TOK k=numeral? - { UNSUPPORTED("PUSH_SCOPE command"); } - | POP_SCOPE_TOK k=numeral? - { UNSUPPORTED("POP_SCOPE command"); } - | POPTO_SCOPE_TOK k=numeral? - { UNSUPPORTED("POPTO_SCOPE command"); } - - | RESET_TOK - { - cmd->reset(new ResetCommand()); - // reset the state of the parser, which is independent of the symbol - // manager - PARSER_STATE->reset(); - } - - | RESET_TOK ASSERTIONS_TOK - { cmd->reset(new ResetAssertionsCommand()); - } - - // Datatypes can be mututally-recursive if they're in the same - // definition block, separated by a comma. So we parse everything - // and then ask the ExprManager to resolve everything in one go. - | DATATYPE_TOK - { /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(); } - datatypeDef[dts] - ( COMMA datatypeDef[dts] )* - END_TOK - { PARSER_STATE->popScope(); - cmd->reset(new DatatypeDeclarationCommand( - PARSER_STATE->bindMutualDatatypeTypes(dts))); - } - - | CONTEXT_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { UNSUPPORTED("CONTEXT command"); } - | { UNSUPPORTED("CONTEXT command"); } - ) - - | FORGET_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] - { UNSUPPORTED("FORGET command"); } - - | GET_TYPE_TOK formula[f] - { UNSUPPORTED("GET_TYPE command"); } - - | CHECK_TYPE_TOK formula[f] COLON type[t,CHECK_DECLARED] - { UNSUPPORTED("CHECK_TYPE command"); } - - | GET_CHILD_TOK formula[f] k=numeral - { UNSUPPORTED("GET_CHILD command"); } - - | GET_OP_TOK formula[f] - { UNSUPPORTED("GET_OP command"); } - - | GET_VALUE_TOK formula[f] - { cmd->reset(new GetValueCommand(f)); } - - | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON - type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET - identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET - { UNSUPPORTED("SUBSTITUTE command"); } - - /* Like the --debug command line option, DBG turns on both tracing - * and debugging. */ - | DBG_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { Debug.on(s); Trace.on(s); } - | { CVC5Message() << "Please specify what to debug." << std::endl; } - ) - - | TRACE_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { Trace.on(s); } - | { CVC5Message() << "Please specify something to trace." << std::endl; } - ) - | UNTRACE_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { Trace.off(s); } - | { CVC5Message() << "Please specify something to untrace." << std::endl; } - ) - - | HELP_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { CVC5Message() << "No help available for `" << s << "'." << std::endl; } - | { CVC5Message() << "Please use --help at the command line for help." - << std::endl; } - ) - - | TRANSFORM_TOK formula[f] - { cmd->reset(new SimplifyCommand(f)); } - - | PRINT_TOK formula[f] - { UNSUPPORTED("PRINT command"); } - | PRINT_TYPE_TOK type[t,CHECK_DECLARED] - { UNSUPPORTED("PRINT_TYPE command"); } - - | CALL_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] formula[f] - { UNSUPPORTED("CALL command"); } - - | ECHO_TOK - ( simpleSymbolicExpr[s] - { cmd->reset(new EchoCommand(s)); } - | { cmd->reset(new EchoCommand()); } - ) - - | EXIT_TOK - { cmd->reset(new QuitCommand()); } - - | INCLUDE_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { UNSUPPORTED("INCLUDE command"); } - | { PARSER_STATE->parseError("No filename given to INCLUDE command"); } - ) - - | DUMP_PROOF_TOK - { cmd->reset(new GetProofCommand()); } - - | DUMP_UNSAT_CORE_TOK - { cmd->reset(new GetUnsatCoreCommand()); } - - | ( DUMP_ASSUMPTIONS_TOK - | DUMP_SIG_TOK - | DUMP_TCC_TOK - | DUMP_TCC_ASSUMPTIONS_TOK - | DUMP_TCC_PROOF_TOK - | DUMP_CLOSURE_TOK - | DUMP_CLOSURE_PROOF_TOK - ) { UNSUPPORTED("DUMP* command"); } - - /* these are all synonyms */ - | ( WHERE_TOK | ASSERTIONS_TOK | ASSUMPTIONS_TOK ) - { cmd->reset(new GetAssertionsCommand()); } - - | COUNTEREXAMPLE_TOK - { cmd->reset(new GetModelCommand); } - | COUNTERMODEL_TOK - { cmd->reset(new GetModelCommand); } - - | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN - { UNSUPPORTED("ARITH_VAR_ORDER command"); } - - | CONTINUE_TOK - { UNSUPPORTED("CONTINUE command"); } - | RESTART_TOK formula[f] { UNSUPPORTED("RESTART command"); } - | RECURSIVE_FUNCTION_TOK (identifier[id,CHECK_NONE,SYM_VARIABLE] - { - if(idCommaFlag){ - idCommaFlag=false; - } - else{ - PARSER_STATE->parseError("Identifiers need to be comma separated"); - } - } - COLON type[t,CHECK_DECLARED] (COMMA { - idCommaFlag=true; - })? - { - func = PARSER_STATE->bindVar(id, t, false, true); - ids.push_back(id); - types.push_back(t); - funcs.push_back(func); - })+ - EQUAL_TOK (formula[f] - { - if(formCommaFlag){ - formCommaFlag=false; - } - else{ - PARSER_STATE->parseError("Function definitions need to be comma separated"); - } - } - (COMMA{ - formCommaFlag=true; - })? - { - if( f.getKind()==api::LAMBDA ){ - bvs.insert(bvs.end(), f[0].begin(), f[0].end()); - formals.push_back(bvs); - bvs.clear(); - f = f[1]; - formulas.push_back(f); - } - else { - formals.push_back(bvs); - formulas.push_back(f); - } - })+ - { - if(idCommaFlag){ - PARSER_STATE->parseError("Cannot end function list with comma"); - } - if(formCommaFlag){ - PARSER_STATE->parseError("Cannot end function definition list with comma"); - } - if(funcs.size()!=formulas.size()){ - PARSER_STATE->parseError("Number of functions doesn't match number of function definitions"); - } - for(unsigned int i = 0, size = funcs.size(); i < size; i++){ - if(!funcs[i].getSort().isSubsortOf(types[i])){ - PARSER_STATE->parseError("Type mismatch in definition"); - } - } - cmd->reset(new DefineFunctionRecCommand(funcs, formals, formulas, true)); - } - | toplevelDeclaration[cmd] - ; - -simpleSymbolicExpr[std::string& s] - : INTEGER_LITERAL - { s = AntlrInput::tokenText($INTEGER_LITERAL); } - | MINUS_TOK INTEGER_LITERAL - { s = std::to_string(MINUS_TOK) + AntlrInput::tokenText($INTEGER_LITERAL); } - | DECIMAL_LITERAL - { s = AntlrInput::tokenText($DECIMAL_LITERAL); } - | HEX_LITERAL - { s = AntlrInput::tokenText($HEX_LITERAL); } - | BINARY_LITERAL - { s = AntlrInput::tokenText($BINARY_LITERAL); } - | str[s] - | IDENTIFIER - { s = AntlrInput::tokenText($IDENTIFIER); } - ; - -symbolicExpr[cvc5::api::Term& sexpr] -@declarations { - std::string s; - std::vector<api::Term> children; -} - : simpleSymbolicExpr[s] - { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } - | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN - { sexpr = SOLVER->mkTerm(cvc5::api::SEXPR, children); } - ; - -/** - * Match a top-level declaration. - */ -toplevelDeclaration[std::unique_ptr<cvc5::Command>* cmd] -@init { - std::vector<std::string> ids; - api::Sort t; - Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) - << std::endl; -} - : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON - ( declareVariables[cmd,t,ids,true] - | declareTypes[cmd,ids] ) - ; - -/** - * A bound variable declaration. - */ -boundVarDecl[std::vector<std::string>& ids, cvc5::api::Sort& t] -@init { - std::unique_ptr<Command> local_cmd; -} - : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON - declareVariables[&local_cmd,t,ids,false] - ; - -/** - * A series of bound variable declarations. - */ -boundVarDecls -@init { - std::vector<std::string> ids; - api::Sort t; -} - : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )* - ; - -boundVarDeclsReturn[std::vector<cvc5::api::Term>& terms, - std::vector<cvc5::api::Sort>& types] -@init { - std::vector<std::string> ids; - api::Sort t; - terms.clear(); - types.clear(); -} - : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )* - ; - -boundVarDeclReturn[std::vector<cvc5::api::Term>& terms, - std::vector<cvc5::api::Sort>& types] -@init { - std::vector<std::string> ids; - api::Sort t; - // NOTE: do not clear the vectors here! -} - : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] - { const std::vector<api::Term>& vars = PARSER_STATE->bindBoundVars(ids, t); - terms.insert(terms.end(), vars.begin(), vars.end()); - for(unsigned i = 0; i < vars.size(); ++i) { - types.push_back(t); - } - } - ; - -/** - * Match the right-hand-side of a type declaration. Unlike - * declareVariables[] below, don't need to return the Type, since it's - * always the KindType (the type of types). Also don't need toplevel - * because type declarations are always top-level, except for - * type-lets, which don't use this rule. - */ -declareTypes[std::unique_ptr<cvc5::Command>* cmd, - const std::vector<std::string>& idList] -@init { - api::Sort t; -} - /* A sort declaration (e.g., "T : TYPE") */ - : TYPE_TOK - { std::unique_ptr<DeclarationSequence> seq(new DeclarationSequence()); - for(std::vector<std::string>::const_iterator i = idList.begin(); - i != idList.end(); ++i) { - // Don't allow a type variable to clash with a previously - // declared type variable, however a type variable and a - // non-type variable can clash unambiguously. Break from CVC3 - // behavior here. - PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); - api::Sort sort = PARSER_STATE->mkSort(*i); - Command* decl = new DeclareSortCommand(*i, 0, sort); - seq->addCommand(decl); - } - cmd->reset(seq.release()); - } - - /* A type alias "T : TYPE = foo..." */ - | TYPE_TOK EQUAL_TOK type[t,CHECK_DECLARED] - { for(std::vector<std::string>::const_iterator i = idList.begin(); - i != idList.end(); - ++i) { - PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); - PARSER_STATE->defineType(*i, t); - } - } - ; - -/** - * Match the right-hand side of a variable declaration. Returns the - * type. Some IDs might have been declared previously, and are not - * re-declared if topLevel is true (CVC allows re-declaration if the - * types are compatible---if they aren't compatible, an error is - * thrown). Also if topLevel is true, variable definitions are - * permitted and "cmd" is output. If topLevel is false, bound vars - * are created - */ -declareVariables[std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t, - const std::vector<std::string>& idList, bool topLevel] -@init { - api::Term f; - Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - /* A variable declaration (or definition) */ - : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? - { std::unique_ptr<DeclarationSequence> seq; - if(topLevel) { - seq.reset(new DeclarationSequence()); - } - if(f.isNull()) { - Debug("parser") << "working on " << idList.front() << " : " << t - << std::endl; - // CVC language allows redeclaration of variables if types are the same - for(std::vector<std::string>::const_iterator i = idList.begin(), - i_end = idList.end(); - i != i_end; - ++i) { - if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) { - api::Sort oldType = PARSER_STATE->getVariable(*i).getSort(); - Debug("parser") << " " << *i << " was declared previously " - << "with type " << oldType << std::endl; - if(oldType != t) { - std::stringstream ss; - ss << language::SetLanguage(Language::LANG_CVC) - << "incompatible type for `" << *i << "':" << std::endl - << " old type: " << oldType << std::endl - << " new type: " << t << std::endl; - PARSER_STATE->parseError(ss.str()); - } else { - Debug("parser") << " types " << t << " and " << oldType - << " are compatible" << std::endl; - } - } else { - Debug("parser") << " " << *i << " not declared" << std::endl; - if(topLevel) { - api::Term func = PARSER_STATE->bindVar(*i, t); - Command* decl = new DeclareFunctionCommand(*i, func, t); - seq->addCommand(decl); - } else { - PARSER_STATE->bindBoundVar(*i, t); - } - } - } - } else { - // f is not null-- meaning this is a definition not a declaration - //Check if the formula f has the correct type, declared as t. - if(!f.getSort().isSubsortOf(t)){ - PARSER_STATE->parseError("Type mismatch in definition"); - } - if(!topLevel) { - // must be top-level; doesn't make sense to write something - // like e.g. FORALL(x:INT = 4): [...] - PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET"); - } - Assert(!idList.empty()); - api::Term fterm = f; - std::vector<api::Term> formals; - if (f.getKind()==api::LAMBDA) - { - formals.insert(formals.end(), f[0].begin(), f[0].end()); - f = f[1]; - } - for(std::vector<std::string>::const_iterator i = idList.begin(), - i_end = idList.end(); - i != i_end; - ++i) { - Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl; - PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); - api::Term func = SOLVER->mkConst(t, *i); - PARSER_STATE->defineVar(*i, fterm); - Command* decl = new DefineFunctionCommand(*i, func, formals, f, true); - seq->addCommand(decl); - } - } - if(topLevel) { - cmd->reset(seq.release()); - } - } - ; - -/** - * Matches a list of identifiers separated by a comma and puts them in the - * given list. - * @param idList the list to fill with identifiers. - * @param check what kinds of check to perform on the symbols - */ -identifierList[std::vector<std::string>& idList, - cvc5::parser::DeclarationCheck check, - cvc5::parser::SymbolType type] -@init { - std::string id; - idList.clear(); -} - : identifier[id,check,type] { idList.push_back(id); } - ( COMMA identifier[id,check,type] { idList.push_back(id); } )* - ; - -/** - * Matches an identifier and returns a string. - */ -identifier[std::string& id, - cvc5::parser::DeclarationCheck check, - cvc5::parser::SymbolType type] - : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); - PARSER_STATE->checkDeclaration(id, check, type); } - ; - -/** - * Match the type in a declaration and do the declaration binding. If - * "check" is CHECK_NONE, then identifiers occurring in the type need - * not exist! They are created as "unresolved" types and linked up in - * a type-substitution pass. Right now, only datatype definitions are - * supported in this way (since type names can occur without any - * forward-declaration in CVC language datatype definitions, we have - * to create types for them on-the-fly). Before passing CHECK_NONE - * you really should have a clear idea of WHY you need to parse that - * way; then you should trace through Parser::bindMutualDatatypeType() - * to figure out just what you're in for. - */ -type[cvc5::api::Sort& t, - cvc5::parser::DeclarationCheck check] -@init { - api::Sort t2; - bool lhs; - std::vector<api::Sort> args; -} - /* a type, possibly a function */ - : restrictedTypePossiblyFunctionLHS[t,check,lhs] - { if(lhs) { - Assert(t.isTuple()); - args = t.getTupleSorts(); - } else { - args.push_back(t); - } - } - ( ARROW_TOK type[t2,check] )? - { if(t2.isNull()) { - if(lhs) { - PARSER_STATE->parseError("improperly-placed type list; expected `->' after to define a function; or else maybe these parentheses were meant to be square brackets, to define a tuple type?"); - } - } else { - t = SOLVER->mkFunctionSort(args, t2); - } - } - - /* type-lets: typeLetDecl defines the types, we just manage the - * scopes here. NOTE that LET in the CVC language is always - * sequential! */ - | LET_TOK { PARSER_STATE->pushScope(); } - typeLetDecl[check] ( COMMA typeLetDecl[check] )* IN_TOK type[t,check] - { PARSER_STATE->popScope(); } - ; - -// A restrictedType is one that is not a "bare" function type (it can -// be enclosed in parentheses) and is not a type list. To support the -// syntax -// -// f : (nat, nat) -> nat; -// -// we have to permit restrictedTypes to be type lists (as on the LHS -// there). The "type" rule above uses restictedTypePossiblyFunctionLHS -// directly in order to implement that; this rule allows a type list to -// parse but then issues an error. -restrictedType[cvc5::api::Sort& t, - cvc5::parser::DeclarationCheck check] -@init { - bool lhs; -} - : restrictedTypePossiblyFunctionLHS[t,check,lhs] - { if(lhs) { PARSER_STATE->parseError("improperly-placed type list; maybe these parentheses were meant to be square brackets, to define a tuple type?"); } } - ; - -/** - * lhs is set to "true" on output if we have a list of types, so an - * ARROW must follow. An ARROW can always follow; lhs means it MUST. - */ -restrictedTypePossiblyFunctionLHS[cvc5::api::Sort& t, - cvc5::parser::DeclarationCheck check, - bool& lhs] -@init { - api::Sort t2; - api::Term f, f2; - std::string id; - std::vector<api::Sort> types; - std::vector< std::pair<std::string, api::Sort> > typeIds; - //SymbolTable* symtab; - Parser* parser; - lhs = false; -} - /* named types */ - : identifier[id,check,SYM_SORT] - parameterization[check,types]? - { - if(check == CHECK_DECLARED || - PARSER_STATE->isDeclared(id, SYM_SORT)) { - Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) - << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; - if(types.size() != PARSER_STATE->getArity(id)) { - std::stringstream ss; - ss << "incorrect arity for symbol `" << id << "': expected " - << PARSER_STATE->getArity( id ) << " type arguments, got " - << types.size(); - PARSER_STATE->parseError(ss.str()); - } - if(types.size() > 0) { - t = PARSER_STATE->getSort(id, types); - }else{ - t = PARSER_STATE->getSort(id); - } - } else { - if(types.empty()) { - t = PARSER_STATE->mkUnresolvedType(id); - Debug("parser-param") << "param: make unres type " << id << std::endl; - }else{ - t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types); - t = t.instantiate( types ); - Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " - << PARSER_STATE->getArity( id ) << std::endl; - } - } - } - - /* array types */ - | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check] - { t = SOLVER->mkArraySort(t, t2); } - | SET_TOK OF_TOK restrictedType[t,check] - { t = SOLVER->mkSetSort(t); } - - /* subtypes */ - | SUBTYPE_TOK LPAREN - /* A bit tricky: this LAMBDA expression cannot refer to constants - * declared in the outer context. What follows isn't quite right, - * though, since type aliases and function definitions should be - * retained in the set of current declarations. */ - formula[f] ( COMMA formula[f2] )? RPAREN - { - PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release"); - } - - /* tuple types / old-style function types */ - | LBRACKET ( type[t,check] { types.push_back(t); } - ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET - { if(types.size() == 1 && types.front().isFunction()) { - // old style function syntax [ T -> U ] - PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax"); - } else { - // tuple type [ T, U, V... ] - t = SOLVER->mkTupleSort(types); - } - } - - /* record types */ - | SQHASH ( identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } - ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* )? HASHSQ - { t = SOLVER->mkRecordSort(typeIds); } - - /* bitvector types */ - | BITVECTOR_TOK LPAREN k=numeral RPAREN - { if(k == 0) { - PARSER_STATE->parseError("Illegal bitvector size: 0"); - } - t = SOLVER->mkBitVectorSort(k); - } - - /* string type */ - | STRING_TOK { t = SOLVER->getStringSort(); } - - /* basic types */ - | BOOLEAN_TOK { t = SOLVER->getBooleanSort(); } - | REAL_TOK { t = SOLVER->getRealSort(); } - | INT_TOK { t = SOLVER->getIntegerSort(); } - - /* Parenthesized general type, or the lhs of an ARROW (a list of - * types). These two things are combined to avoid conflicts in - * parsing. */ - | LPAREN type[t,check] { types.push_back(t); } - ( COMMA type[t,check] { lhs = true; types.push_back(t); } )* RPAREN - { if(lhs) { t = SOLVER->mkTupleSort(types); } - // if !lhs, t is already set up correctly, nothing to do.. - } - ; - -parameterization[cvc5::parser::DeclarationCheck check, - std::vector<cvc5::api::Sort>& params] -@init { - api::Sort t; -} - : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } - ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET - ; - -typeLetDecl[cvc5::parser::DeclarationCheck check] -@init { - api::Sort t; - std::string id; -} - : identifier[id,CHECK_NONE,SYM_SORT] (COLON TYPE_TOK)? EQUAL_TOK restrictedType[t,check] - { PARSER_STATE->defineType(id, t); } - ; - -/** - * Matches a cvc5 expression. Formulas and terms are not really - * distinguished during parsing; please ignore the naming of the - * grammar rules. - * - * @return the expression representing the formula/term - */ -formula[cvc5::api::Term& f] -@init { - Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; - api::Term f2; - std::vector<cvc5::api::Term> expressions; - std::vector<unsigned> operators; - unsigned op; -} - : n=nots - ( prefixFormula[f] - { f = addNots(SOLVER, n, f); } - | comparison[f] - { f = addNots(SOLVER, n, f); - expressions.push_back(f); - } - morecomparisons[expressions,operators]? - { - f = createPrecedenceTree(PARSER_STATE, SOLVER, expressions, operators); - } - ) - ; - -morecomparisons[std::vector<cvc5::api::Term>& expressions, - std::vector<unsigned>& operators] returns [size_t i = 0] -@init { - unsigned op; - api::Term f; - $i = expressions.size(); -} - : booleanBinop[op] { operators.push_back(op); } - n=nots - ( prefixFormula[f] - { expressions.push_back(addNots(SOLVER, n, f)); } - | comparison[f] - { f = addNots(SOLVER, n, f); - expressions.push_back(f); - } - morecomparisons[expressions,operators]? - ) - ; - -/** Matches 0 or more NOTs. */ -nots returns [size_t n = 0] - : ( NOT_TOK { ++$n; } )* - ; - -prefixFormula[cvc5::api::Term& f] -@init { - std::vector<std::string> ids; - std::vector<api::Term> terms; - std::vector<api::Sort> types; - std::vector<api::Term> bvs; - api::Sort t; - api::Kind k; - api::Term ipl; -} - /* quantifiers */ - : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } ) - { PARSER_STATE->pushScope(); } LPAREN - boundVarDecl[ids,t] - { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { - bvs.push_back(PARSER_STATE->bindBoundVar(*i, t)); - } - ids.clear(); - } - ( COMMA boundVarDecl[ids,t] - { - for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { - bvs.push_back(PARSER_STATE->bindBoundVar(*i, t)); - } - ids.clear(); - } - )* RPAREN { - terms.push_back( MK_TERM( api::BOUND_VAR_LIST, bvs ) ); } - COLON instantiationPatterns[ipl]? formula[f] - { PARSER_STATE->popScope(); - terms.push_back(f); - if(! ipl.isNull()) { - terms.push_back(ipl); - } - f = MK_TERM(k, terms); - } - - /* lets: letDecl defines the variables and functionss, we just - * manage the scopes here. NOTE that LET in the CVC language is - * always sequential! */ - | LET_TOK { PARSER_STATE->pushScope(); } - letDecl ( COMMA letDecl )* - IN_TOK formula[f] { PARSER_STATE->popScope(); } - - /* lambda */ - | LAMBDA_TOK { PARSER_STATE->pushScope(); } LPAREN - boundVarDeclsReturn[terms,types] - RPAREN COLON formula[f] - { PARSER_STATE->popScope(); - api::Term bvl = MK_TERM( api::BOUND_VAR_LIST, terms ); - f = MK_TERM( api::LAMBDA, bvl, f ); - } - ; - -instantiationPatterns[ cvc5::api::Term& expr ] -@init { - std::vector<api::Term> args; - api::Term f; - std::vector<api::Term> patterns; -} - : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON - { patterns.push_back( MK_TERM( api::INST_PATTERN, args ) ); - args.clear(); - } )+ - { if(! patterns.empty()) { - expr = MK_TERM( api::INST_PATTERN_LIST, patterns ); - } - } - ; - -/** - * Matches (and defines) a single LET declaration. - */ -letDecl -@init { - api::Term e; - std::string name; -} - : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e] - { - Debug("parser") << language::SetLanguage(Language::LANG_CVC) - << e.getSort() << std::endl; - PARSER_STATE->defineVar(name, e); - Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: " - << name << std::endl - << " ==>" << " " << e << std::endl; - } - ; - -booleanBinop[unsigned& op] -@init { - op = LT(1)->getType(LT(1)); -} - : IFF_TOK - | IMPLIES_TOK - | OR_TOK - | XOR_TOK - | AND_TOK - ; - -comparison[cvc5::api::Term& f] -@init { - std::vector<cvc5::api::Term> expressions; - std::vector<unsigned> operators; - unsigned op; -} - : term[f] { expressions.push_back(f); } - ( comparisonBinop[op] term[f] - { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(PARSER_STATE, SOLVER, expressions, operators); } - ; - -comparisonBinop[unsigned& op] -@init { - op = LT(1)->getType(LT(1)); -} - : EQUAL_TOK - | DISEQUAL_TOK - | GT_TOK - | GEQ_TOK - | LT_TOK - | LEQ_TOK - | MEMBER_TOK - | FMF_CARD_TOK - ; - -arithmeticBinop[unsigned& op] -@init { - op = LT(1)->getType(LT(1)); -} - : PLUS_TOK - | MINUS_TOK - | STAR_TOK - | INTDIV_TOK - | MOD_TOK - | DIV_TOK - | EXP_TOK - ; - -/** Parses an array/tuple/record assignment term. */ -term[cvc5::api::Term& f] -@init { - std::vector<cvc5::api::Term> expressions; - std::vector<unsigned> operators; - unsigned op; - api::Sort t; -} - : uminusTerm[f] - ( WITH_TOK - ( arrayStore[f] ( COMMA arrayStore[f] )* - | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )* - | recordStore[f] ( COMMA DOT recordStore[f] )* ) ) - | { expressions.push_back(f); } - ( arithmeticBinop[op] uminusTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(PARSER_STATE, SOLVER, expressions, operators); } - ) - ; - -/** - * Parses just part of the array assignment (and constructs - * the store terms). - */ -arrayStore[cvc5::api::Term& f] -@init { - api::Term f2, k; -} - : LBRACKET formula[k] RBRACKET - { f2 = MK_TERM(cvc5::api::SELECT, f, k); } - ( ( arrayStore[f2] - | DOT ( tupleStore[f2] - | recordStore[f2] ) ) - | ASSIGN_TOK term[f2] ) - { f = MK_TERM(cvc5::api::STORE, f, k, f2); } - ; - -/** - * Parses just part of the tuple assignment (and constructs - * the store terms). - */ -tupleStore[cvc5::api::Term& f] -@init { - api::Term f2; -} - : k=numeral - { api::Sort t = f.getSort(); - if(! t.isTuple()) { - PARSER_STATE->parseError("tuple-update applied to non-tuple"); - } - size_t length = t.getTupleLength(); - if(k >= length) { - std::stringstream ss; - ss << "tuple is of length " << length << "; cannot update index " << k; - PARSER_STATE->parseError(ss.str()); - } - const api::Datatype& dt = t.getDatatype(); - f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, dt[0][k].getSelectorTerm(), f); - } - ( ( arrayStore[f2] - | DOT ( tupleStore[f2] - | recordStore[f2] ) ) - | ASSIGN_TOK term[f2] ) - { - const api::Datatype& dt = f.getSort().getDatatype(); - f = SOLVER->mkTerm( - api::APPLY_UPDATER, dt[0][k].getUpdaterTerm(), f, f2); - } - ; - -/** - * Parses just part of the record assignment (and constructs - * the store terms). - */ -recordStore[cvc5::api::Term& f] -@init { - std::string id; - api::Term f2; -} - : identifier[id,CHECK_NONE,SYM_VARIABLE] - { api::Sort t = f.getSort(); - if(! t.isRecord()) { - std::stringstream ss; - ss << "record-update applied to non-record term" << std::endl - << "the term: " << f << std::endl - << "its type: " << t; - PARSER_STATE->parseError(ss.str()); - } - const api::Datatype& dt = t.getDatatype(); - f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, dt[0][id].getSelectorTerm(), f); - } - ( ( arrayStore[f2] - | DOT ( tupleStore[f2] - | recordStore[f2] ) ) - | ASSIGN_TOK term[f2] ) - { - const api::Datatype& dt = f.getSort().getDatatype(); - f = SOLVER->mkTerm( - api::APPLY_UPDATER, dt[0][id].getUpdaterTerm(), f, f2); - } - ; - -/** Parses a unary minus term. */ -uminusTerm[cvc5::api::Term& f] -@init { - unsigned minusCount = 0; -} - /* Unary minus */ - : (MINUS_TOK { ++minusCount; })* bvBinaryOpTerm[f] - { - while (minusCount > 0) - { - --minusCount; - f = MK_TERM(cvc5::api::UMINUS, f); - } - }; - -/** Parses bitvectors. Starts with binary operators @, &, and |. */ -bvBinaryOpTerm[cvc5::api::Term& f] -@init { - std::vector<cvc5::api::Term> expressions; - std::vector<unsigned> operators; - unsigned op; -} - : bvNegTerm[f] { expressions.push_back(f); } - ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(PARSER_STATE, SOLVER, expressions, operators); } - ; -bvBinop[unsigned& op] -@init { - op = LT(1)->getType(LT(1)); -} - : CONCAT_TOK - | BAR // bitwise OR - | BVAND_TOK - ; - -bvNegTerm[cvc5::api::Term& f] - /* BV neg */ - : BVNEG_TOK bvNegTerm[f] - { - f = f.getSort().isSet() ? MK_TERM(cvc5::api::COMPLEMENT, f) - : MK_TERM(cvc5::api::BITVECTOR_NOT, f); - } - | relationBinopTerm[f] - ; - -relationBinop[unsigned& op] -@init { - op = LT(1)->getType(LT(1)); -} - : JOIN_TOK - | PRODUCT_TOK - | JOIN_IMAGE_TOK - ; - -relationBinopTerm[cvc5::api::Term& f] -@init { - std::vector<cvc5::api::Term> expressions; - std::vector<unsigned> operators; - unsigned op; -} - : postfixTerm[f] { expressions.push_back(f); } - ( relationBinop[op] postfixTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(PARSER_STATE, SOLVER, expressions, operators); } - ; - -/** - * Parses an array select / bitvector extract / bitvector shift / - * function or constructor application. These are all parsed the same - * way because they are all effectively post-fix operators and can - * continue piling onto an expression. Array selects and bitvector - * extracts even share similar syntax with their use of [ square - * brackets ], so we left-factor as much out as possible to make ANTLR - * happy. - */ -postfixTerm[cvc5::api::Term& f] -@init { - api::Term f2; - bool extract = false, left = false; - std::vector<api::Term> args; - std::string id; - api::Sort t; -} - : ( relationTerm[f] - ( /* array select / bitvector extract */ - LBRACKET - ( formula[f2] { extract = false; } - | k1=numeral COLON k2=numeral { extract = true; } ) - RBRACKET - { if(extract) { - /* bitvector extract */ - f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_EXTRACT,k1,k2), f); - } else { - /* array select */ - f = MK_TERM(cvc5::api::SELECT, f, f2); - } - } - /* left- or right-shift */ - | ( LEFTSHIFT_TOK { left = true; } - | RIGHTSHIFT_TOK { left = false; } ) k=numeral - { - if(left) { - f = MK_TERM(api::BITVECTOR_CONCAT, f, SOLVER->mkBitVector(k)); - } else { - unsigned bv_size = f.getSort().getBVSize(); - f = MK_TERM(api::BITVECTOR_CONCAT, - SOLVER->mkBitVector(k), - SOLVER->mkTerm( - SOLVER->mkOp(api::BITVECTOR_EXTRACT, bv_size - 1, k), f)); - } - } - - /* function/constructor application */ - | LPAREN { args.push_back(f); } - formula[f] { args.push_back(f); } - ( COMMA formula[f] { args.push_back(f); } )* RPAREN - { - PARSER_STATE->checkFunctionLike(args.front()); - api::Kind kind = PARSER_STATE->getKindForFunction(args.front()); - Debug("parser") << "expr is " << args.front() << std::endl; - Debug("parser") << "kind is " << kind << std::endl; - f = SOLVER->mkTerm(kind,args); - } - - /* record / tuple select */ - | DOT - ( identifier[id,CHECK_NONE,SYM_VARIABLE] - { api::Sort type = f.getSort(); - if(! type.isRecord()) { - PARSER_STATE->parseError("record-select applied to non-record"); - } - const api::Datatype& dt = type.getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR, - dt[0][id].getSelectorTerm(), - f); - } - | k=numeral - { - api::Sort type = f.getSort(); - if(! type.isTuple()) { - PARSER_STATE->parseError("tuple-select applied to non-tuple"); - } - size_t length = type.getTupleLength(); - if(k >= length) { - std::stringstream ss; - ss << "tuple is of length " << length << "; cannot access index " << k; - PARSER_STATE->parseError(ss.str()); - } - const api::Datatype& dt = type.getDatatype(); - f = SOLVER->mkTerm(api::APPLY_SELECTOR, - dt[0][k].getSelectorTerm(), - f); - } - ) - )* - | FLOOR_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::TO_INTEGER, f); } - | IS_INTEGER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::IS_INTEGER, f); } - | ABS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::ABS, f); } - | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN - { f = MK_TERM(SOLVER->mkOp(cvc5::api::DIVISIBLE, n), f); } - | DISTINCT_TOK LPAREN - formula[f] { args.push_back(f); } - ( COMMA formula[f] { args.push_back(f); } )* RPAREN - { - f = (args.size() == 1) ? SOLVER->mkTrue() - : MK_TERM(cvc5::api::DISTINCT, args); - } - ) - ( typeAscription[f, t] - { - f = PARSER_STATE->applyTypeAscription(f,t); - } - )? - ; - -relationTerm[cvc5::api::Term& f] - /* relation terms */ - : TRANSPOSE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::TRANSPOSE, f); } - | TRANSCLOSURE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::TCLOSURE, f); } - | TUPLE_TOK LPAREN formula[f] RPAREN - { std::vector<api::Sort> types; - std::vector<api::Term> args; - args.push_back(f); - types.push_back(f.getSort()); - api::Sort t = SOLVER->mkTupleSort(types); - const api::Datatype& dt = t.getDatatype(); - args.insert(args.begin(), dt[0].getConstructorTerm()); - f = MK_TERM(api::APPLY_CONSTRUCTOR, args); - } - | IDEN_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::IDEN, f); } - | bvTerm[f] - ; - -bvTerm[cvc5::api::Term& f] -@init { - api::Term f2; - std::vector<api::Term> args; -} - /* BV xor */ - : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_XOR, f, f2); } - | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_NAND, f, f2); } - | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_NOR, f, f2); } - | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_COMP, f, f2); } - | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_XNOR, f, f2); } - - /* BV unary minus */ - | BVUMINUS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_NEG, f); } - /* BV addition */ - | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); } - ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { - if (k <= 0) { - PARSER_STATE->parseError("BVPLUS(k,_,_) must have k > 0"); - } - for (unsigned i = 0; i < args.size(); ++ i) { - ENSURE_BV_SIZE(k, args[i]); - } - f = MK_TERM(cvc5::api::BITVECTOR_ADD, args); - } - /* BV subtraction */ - | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN - { - if (k <= 0) { - PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0"); - } - ENSURE_BV_SIZE(k, f); - ENSURE_BV_SIZE(k, f2); - f = MK_TERM(cvc5::api::BITVECTOR_SUB, f, f2); - } - /* BV multiplication */ - | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN - { - if (k <= 0) { - PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0"); - } - ENSURE_BV_SIZE(k, f); - ENSURE_BV_SIZE(k, f2); - f = MK_TERM(cvc5::api::BITVECTOR_MULT, f, f2); - } - /* BV unsigned division */ - | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_UDIV, f, f2); } - /* BV signed division */ - | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SDIV, f, f2); } - /* BV unsigned remainder */ - | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_UREM, f, f2); } - /* BV signed remainder */ - | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SREM, f, f2); } - /* BV signed modulo */ - | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SMOD, f, f2); } - /* BV left shift */ - | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SHL, f, f2); } - /* BV arithmetic right shift */ - | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_ASHR, f, f2); } - /* BV logical left shift */ - | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_LSHR, f, f2); } - /* BV sign extension */ - | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN - { unsigned n = f.getSort().getBVSize(); - // Sign extension in TheoryBitVector is defined as in SMT-LIB - // which is different than in the CVC language - // SX(BITVECTOR(k), n) in CVC language extends to n bits - // In SMT-LIB, such a thing expands to k + n bits - f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_SIGN_EXTEND,k-n), f); - } - /* BV zero extension */ - | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN - { unsigned n = f.getSort().getBVSize(); - // Zero extension in TheoryBitVector is defined as in SMT-LIB - // which is the same as in CVC3, but different than SX! - // SX(BITVECTOR(k), n) in CVC language extends to n bits - // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits - f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_ZERO_EXTEND,k), f); - } - /* BV repeat operation */ - | BVREPEAT_TOK LPAREN formula[f] COMMA k=numeral RPAREN - { f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_REPEAT,k), f); } - /* BV rotate right */ - | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN - { f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_ROTATE_RIGHT,k), f); } - /* BV rotate left */ - | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN - { f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_ROTATE_LEFT,k), f); } - - /* BV comparisons */ - | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_ULT, f, f2); } - | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_ULE, f, f2); } - | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_UGT, f, f2); } - | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_UGE, f, f2); } - | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SLT, f, f2); } - | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SLE, f, f2); } - | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SGT, f, f2); } - | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::BITVECTOR_SGE, f, f2); } - | stringTerm[f] - ; - -stringTerm[cvc5::api::Term& f] -@init { - api::Term f2; - api::Term f3; - std::string s; - std::vector<api::Term> args; -} - /* String prefix operators */ - : STRING_CONCAT_TOK LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(cvc5::api::STRING_CONCAT, args); } - | STRING_LENGTH_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_LENGTH, f); } - | STRING_CONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::STRING_CONTAINS, f, f2); } - | STRING_SUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(cvc5::api::STRING_SUBSTR, f, f2, f3); } - | STRING_CHARAT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::STRING_CHARAT, f, f2); } - | STRING_INDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(cvc5::api::STRING_INDEXOF, f, f2, f3); } - | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(cvc5::api::STRING_REPLACE, f, f2, f3); } - | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(cvc5::api::STRING_REPLACE_ALL, f, f2, f3); } - | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::STRING_PREFIX, f, f2); } - | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::STRING_SUFFIX, f, f2); } - | STRING_STOI_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_TO_INT, f); } - | STRING_ITOS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_FROM_INT, f); } - | STRING_TO_REGEXP_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_TO_REGEXP, f); } - | STRING_TOLOWER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_TOLOWER, f); } - | STRING_TOUPPER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_TOUPPER, f); } - | STRING_REV_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::STRING_REV, f); } - | REGEXP_CONCAT_TOK LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(cvc5::api::REGEXP_CONCAT, args); } - | REGEXP_UNION_TOK LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(cvc5::api::REGEXP_UNION, args); } - | REGEXP_INTER_TOK LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(cvc5::api::REGEXP_INTER, args); } - | REGEXP_STAR_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::REGEXP_STAR, f); } - | REGEXP_PLUS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::REGEXP_PLUS, f); } - | REGEXP_OPT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::REGEXP_OPT, f); } - | REGEXP_RANGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(cvc5::api::REGEXP_RANGE, f, f2); } - | REGEXP_LOOP_TOK LPAREN formula[f] COMMA lo=numeral COMMA hi=numeral RPAREN - { - api::Op lop = SOLVER->mkOp(cvc5::api::REGEXP_LOOP, lo, hi); - f = MK_TERM(lop, f); - } - | REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::REGEXP_COMPLEMENT, f); } - | SEQ_UNIT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::SEQ_UNIT, f); } - | REGEXP_EMPTY_TOK - { f = MK_TERM(cvc5::api::REGEXP_EMPTY, std::vector<api::Term>()); } - | REGEXP_SIGMA_TOK - { f = MK_TERM(cvc5::api::REGEXP_SIGMA, std::vector<api::Term>()); } - - /* string literal */ - | str[s] - { f = PARSER_STATE->mkStringConstant(s); } - - | setsTerm[f] - ; - -setsTerm[cvc5::api::Term& f] -@init { -} - /* Sets prefix operators */ - : SETS_CARD_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::CARD, f); } - | SETS_CHOOSE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(cvc5::api::CHOOSE, f); } - | simpleTerm[f] - ; - - -/** Parses a simple term. */ -simpleTerm[cvc5::api::Term& f] -@init { - std::string name; - std::vector<api::Term> args; - std::vector<std::string> names; - api::Term e; - Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; - api::Sort t, t2; -} - /* if-then-else */ - : iteTerm[f] - - /* parenthesized sub-formula / tuple literals */ - | LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f] { args.push_back(f); } )* RPAREN - { if(args.size() > 1) { - /* If args has elements, we must be a tuple literal. - * Otherwise, f is already the sub-formula, and - * there's nothing to do */ - std::vector<api::Sort> types; - for (std::vector<api::Term>::const_iterator i = args.begin(); - i != args.end(); - ++i) - { - types.push_back((*i).getSort()); - } - api::Sort dtype = SOLVER->mkTupleSort(types); - const api::Datatype& dt = dtype.getDatatype(); - args.insert(args.begin(), dt[0].getConstructorTerm()); - f = MK_TERM(api::APPLY_CONSTRUCTOR, args); - } - } - - /* empty tuple literal */ - | LPAREN RPAREN - { std::vector<api::Sort> types; - api::Sort dtype = SOLVER->mkTupleSort(types); - const api::Datatype& dt = dtype.getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm()); - } - - /* empty record literal */ - | PARENHASH HASHPAREN - { - api::Sort dtype = SOLVER->mkRecordSort( - std::vector<std::pair<std::string, api::Sort>>()); - const api::Datatype& dt = dtype.getDatatype(); - f = MK_TERM(api::APPLY_CONSTRUCTOR, dt[0].getConstructorTerm()); - } - /* empty set literal */ - | LBRACE RBRACE - { //boolean is placeholder - f = SOLVER->mkEmptySet(SOLVER->mkSetSort(SOLVER->getBooleanSort())); - } - | UNIVSET_TOK - { //boolean is placeholder - f = SOLVER->mkUniverseSet(SOLVER->mkSetSort(SOLVER->getBooleanSort())); - } - - /* finite set literal */ - | LBRACE formula[f] { args.push_back(f); } - ( COMMA formula[f] { args.push_back(f); } )* RBRACE - { f = MK_TERM(api::SINGLETON, args[0]); - for(size_t i = 1; i < args.size(); ++i) { - f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i])); - } - } - - /* set cardinality literal */ - | BAR BAR formula[f] { args.push_back(f); } BAR BAR - { f = MK_TERM(api::CARD, args[0]); - } - - /* array literals */ - | ARRAY_TOK LPAREN - restrictedType[t, CHECK_DECLARED] OF_TOK restrictedType[t2, CHECK_DECLARED] - RPAREN COLON simpleTerm[f] - { t = SOLVER->mkArraySort(t, t2); - if(!t2.isComparableTo(f.getSort())) { - std::stringstream ss; - ss << "type mismatch inside array constant term:" << std::endl - << "array type: " << t << std::endl - << "expected const type: " << t2 << std::endl - << "computed const type: " << f.getSort(); - PARSER_STATE->parseError(ss.str()); - } - f = SOLVER->mkConstArray(t, f); - } - - /* boolean literals */ - | TRUE_TOK { f = SOLVER->mkTrue(); } - | FALSE_TOK { f = SOLVER->mkFalse(); } - /* arithmetic literals */ - /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot! - * This is a rational constant! Otherwise the parser interprets it as a tuple - * selector! */ - | DECIMAL_LITERAL { - f = SOLVER->mkReal(AntlrInput::tokenText($DECIMAL_LITERAL)); - } - | INTEGER_LITERAL { - f = SOLVER->mkInteger(AntlrInput::tokenText($INTEGER_LITERAL)); - } - /* bitvector literals */ - | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); - f = SOLVER->mkBitVector(hexString.size() * 4, hexString, 16); - } - | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); - f = SOLVER->mkBitVector(binString.size(), binString, 2); - } - /* record literals */ - | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } - ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN - { std::vector< std::pair<std::string, api::Sort> > typeIds; - Assert(names.size() == args.size()); - for(unsigned i = 0; i < names.size(); ++i) { - typeIds.push_back(std::make_pair(names[i], args[i].getSort())); - } - api::Sort dtype = SOLVER->mkRecordSort(typeIds); - const api::Datatype& dt = dtype.getDatatype(); - args.insert(args.begin(), dt[0].getConstructorTerm()); - f = MK_TERM(api::APPLY_CONSTRUCTOR, args); - } - - /* variable / zero-ary constructor application */ - | identifier[name,CHECK_DECLARED,SYM_VARIABLE] - /* ascriptions will be required for parameterized zero-ary constructors */ - { f = PARSER_STATE->getVariable(name); - // datatypes: zero-ary constructors - api::Sort dtype = f.getSort(); - if(dtype.isConstructor() && dtype.getConstructorArity() == 0) { - // don't require parentheses, immediately turn it into an apply - f = MK_TERM(cvc5::api::APPLY_CONSTRUCTOR, f); - } - } - ; - -/** - * Matches a type ascription. - * The f arg is the term to check (it is an input-only argument). - */ -typeAscription[const cvc5::api::Term& f, cvc5::api::Sort& t] -@init { -} - : COLON COLON type[t,CHECK_DECLARED] - ; - -/** - * Matches an entry in a record literal. - */ -recordEntry[std::string& name, cvc5::api::Term& ex] - : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex] - ; - -/** - * Parses an ITE term. - */ -iteTerm[cvc5::api::Term& f] -@init { - std::vector<api::Term> args; - Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : IF_TOK formula[f] { args.push_back(f); } - THEN_TOK formula[f] { args.push_back(f); } - iteElseTerm[f] { args.push_back(f); } - ENDIF_TOK - { f = MK_TERM(cvc5::api::ITE, args); } - ; - -/** - * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... - */ -iteElseTerm[cvc5::api::Term& f] -@init { - std::vector<api::Term> args; - Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : ELSE_TOK formula[f] - | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } - THEN_TOK iteThen = formula[f] { args.push_back(f); } - iteElse = iteElseTerm[f] { args.push_back(f); } - { f = MK_TERM(cvc5::api::ITE, args); } - ; - -/** - * Parses a datatype definition - */ -datatypeDef[std::vector<cvc5::api::DatatypeDecl>& datatypes] -@init { - std::string id, id2; - api::Sort t; - std::vector< api::Sort > params; -} - /* This really needs to be CHECK_NONE, or mutually-recursive - * datatypes won't work, because this type will already be - * "defined" as an unresolved type; don't worry, we check - * below. */ - : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } - ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); - params.push_back( t ); - } - ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); - params.push_back( t ); } - )* RBRACKET - )? - { - datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, false)); - if(!PARSER_STATE->isUnresolvedType(id)) { - // if not unresolved, must be undeclared - PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); - } - } - EQUAL_TOK constructorDef[datatypes.back()] - ( BAR constructorDef[datatypes.back()] )* - { PARSER_STATE->popScope(); } - ; - -/** - * Parses a constructor defintion for type - */ -constructorDef[cvc5::api::DatatypeDecl& type] -@init { - std::string id; - std::unique_ptr<cvc5::api::DatatypeConstructorDecl> ctor; -} - : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { - ctor.reset(new cvc5::api::DatatypeConstructorDecl( - SOLVER->mkDatatypeConstructorDecl(id))); - } - ( LPAREN - selector[&ctor] - ( COMMA selector[&ctor] )* - RPAREN - )? - { // make the constructor - type.addConstructor(*ctor.get()); - Debug("parser-idt") << "constructor: " << id.c_str() << std::endl; - } - ; - -selector[std::unique_ptr<cvc5::api::DatatypeConstructorDecl>* ctor] -@init { - std::string id; - api::Sort t, t2; -} - : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE] - { - (*ctor)->addSelector(id, t); - Debug("parser-idt") << "selector: " << id.c_str() << std::endl; - } - ; - -/** - * Matches an identifier from the input. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a letter. - */ -IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*; - -/** - * Same as an integer literal converted to an unsigned int, but - * slightly more convenient AND works around a strange ANTLR bug (?) - * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was - * returning a reference to the wrong token?! - */ -numeral returns [unsigned k = 0] - : INTEGER_LITERAL - { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); } - ; - -/** - * Similar to numeral but for strings. - */ -str[std::string& s] - : STRING_LITERAL - { s = AntlrInput::tokenText($STRING_LITERAL); - /* strip off the quotes */ - s = s.substr(1, s.size() - 2); - } - ; - -/** - * Matches a hexadecimal constant. - */ -HEX_LITERAL - : '0hex' HEX_DIGIT+ - ; - -/** - * Matches a binary constant. - */ -BINARY_LITERAL - : '0bin' ('0' | '1')+ - ; - -/** - * Matches a double quoted string literal. Escaping is supported, and - * escape character '\' has to be escaped. - */ -STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"'; - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -fragment ALPHA : 'a'..'z' | 'A'..'Z'; - -/** - * Matches the decimal digits (0-9) - */ -fragment DIGIT : '0'..'9'; - -// This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121 -// which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/) -// -// Special rule that uses parsing tricks to identify numbers and ranges; it's all about -// the dot ('.'). -// Recognizes: -// '.' as DOT -// '..' as DOTDOT -// INTEGER_LITERAL (digit+) -// DECIMAL_LITERAL (digit* . digit+) -// Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10"). -// -// This doesn't ever generate the NUMBER_OR_RANGEOP token, it -// manipulates the $type inside to return the right token. -NUMBER_OR_RANGEOP - : DIGIT+ - ( - { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; } - | { $type = INTEGER_LITERAL; } - ) - | '.' - ( '.' {$type = DOTDOT; } - | {$type = DOT; } - ) - ; - -// these empty fragments remove "no lexer rule corresponding to token" warnings -fragment INTEGER_LITERAL:; -fragment DECIMAL_LITERAL:; -fragment DOT:; -fragment DOTDOT:; - -/** - * Matches the hexadecimal digits (0-9, a-f, A-F) - */ -fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; - -/** - * Matches and skips whitespace in the input and ignores it. - */ -WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }; - -/** - * Matches the comments and ignores them - */ -COMMENT : '%' (~('\n' | '\r'))* { SKIP(); }; - -/** - * Matches an allowed escaped character. - */ -fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r'); diff --git a/src/parser/cvc/README b/src/parser/cvc/README deleted file mode 100644 index df6c82de9..000000000 --- a/src/parser/cvc/README +++ /dev/null @@ -1,98 +0,0 @@ -Notes on cvc5's CVC language parser. - -This language parser attempts to maintain some backward compatibility -with previous versions of the language. However, as the language -evolves, new features need to be supported, and deprecated, -difficult-to-maintain, or grammar-conflicting syntax and features -need to be removed. - -In order to support our users, we have tried to parse what CVC3 could -and (at least) offer an error when a feature is unavailable or -unimplemented. But this is not always possible. Please report a -bug if a particular discrepancy between CVC3 and cvc5 handling of -the CVC language is a concern to you; we may be able to add a -compatibility mode, or at least offer better warnings or errors. - -Below is a list of the known differences between CVC3's and cvc5's -version of the CVC language. This is the list of differences in -language design and parsing ONLY. The featureset of cvc5 is -rapidly expanding, but does not match CVC3's breadth yet. However, -cvc5 should tell you of an unimplemented feature if you try to use -it (rather than giving a cryptic parse or assertion error). - -* cvc5 does not add the current assumptions to the scope after - SAT/INVALID responses like CVC3 did. - -* cvc5 no longer supports the "old" function syntax: - - f : [INT -> INT]; - - This syntax was deprecated in CVC3, and will no longer be - supported. Functions are now written as follows: - - unary : INT -> INT; - binary : (INT, INT) -> INT; - ternary : (INT, INT, INT) -> INT; - -* QUERY and CHECKSAT do not add their argument to the current - list of assertions like CVC3 did. - -* cvc5 allows datatypes to hold complex types that contain self- - or mutual references. For example, - - DATATYPE tree = node(children:ARRAY INT OF tree) | leaf(data:INT) END; - - is permissible in cvc5 but not in CVC3. - -* cvc5 supports parameterized types in datatype definitions, e.g. - - DATATYPE list[T] = cons(car:T) | nil END; - - You can then declare "x : list[INT];" or "x : list[list[INT]];", - for example. - -* cvc5 supports type ascriptions, e.g. - - U : TYPE; - f : INT -> U; - QUERY f(5) : U = f(6); - QUERY f(5) : U = f(6) : U; - QUERY ( f(5) = f(6) ) : BOOLEAN; - QUERY f(5) : U = f(6) : U : BOOLEAN; - - You probably won't need it that much, but it can be handy for - debugging. If a term (or formula) isn't the same type as its - ascription, and it cannot be "up-casted" safely, an error is - immediately generated at parse time. Sometimes this up-cast is - necessary; consider the "nil" constructor of list[T] above. - To use "nil," you must cast it to something: - - DATATYPE Item = Carrots | Butter | Milk | Bread END; - groceries : list[Item] = cons(Butter, cons(Bread, nil:list[INT])); - -* cvc5 supports stronger distinction between type and variable names. - This means that cvc5 may allow you to declare things that CVC3 does - not: - - a : TYPE; - a : INT; % CVC3 complains - a : a; % cvc5 complains, `a' cannot both be INT and `a' - b : a; % No problem, `a' is both the type of `b', and an INT - -* cvc5 supports a command-level LET syntax, e.g.: - - LET double = LAMBDA(x:INT) : 2*x IN - QUERY double(5) = 10; - - It works for types also, and mixes of the two: - - LET x = INT, y = 5, z = x IN - w : x = y; - QUERY y = 5; % error: y undefined - QUERY w = 5; % valid - - The scope of such a LET is exactly one command (until a semicolon). - (It would conflict with POP_SCOPE if it lasted longer.) - --- Morgan Deters <mdeters@cs.nyu.edu> Wed, 20 Apr 2011 18:32:32 -0400 - diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp deleted file mode 100644 index 0f87e42cd..000000000 --- a/src/parser/cvc/cvc.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The parser class for the CVC language. - */ - -#include "parser/cvc/cvc.h" -#include "smt/command.h" - -namespace cvc5 { -namespace parser { - -void Cvc::forceLogic(const std::string& logic) -{ - Parser::forceLogic(logic); - preemptCommand(new SetBenchmarkLogicCommand(logic)); -} - -bool Cvc::getTesterName(api::Term cons, std::string& name) -{ - std::stringstream ss; - ss << "is_" << cons; - name = ss.str(); - return true; -} - -} // namespace parser -} // namespace cvc5 diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h deleted file mode 100644 index e20e041cc..000000000 --- a/src/parser/cvc/cvc.h +++ /dev/null @@ -1,51 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The parser class for the CVC language. - */ - -#include "cvc5parser_private.h" - -#ifndef CVC5__PARSER__CVC_H -#define CVC5__PARSER__CVC_H - -#include "api/cpp/cvc5.h" -#include "parser/parser.h" - -namespace cvc5 { - -namespace parser { - -class Cvc : public Parser -{ - friend class ParserBuilder; - - public: - void forceLogic(const std::string& logic) override; - - /** Updates name to the tester name of cons, e.g. "is_cons" */ - bool getTesterName(api::Term cons, std::string& name) override; - - protected: - Cvc(api::Solver* solver, - SymbolManager* sm, - bool strictMode = false, - bool parseOnly = false) - : Parser(solver, sm, strictMode, parseOnly) - { - } -}; - -} // namespace parser -} // namespace cvc5 - -#endif /* CVC5__PARSER__CVC_H */ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp deleted file mode 100644 index 1592e06fb..000000000 --- a/src/parser/cvc/cvc_input.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Christopher L. Conway, Morgan Deters, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - */ - -#include "parser/cvc/cvc_input.h" - -#include <antlr3.h> - -#include "base/check.h" -#include "parser/antlr_input.h" -#include "parser/cvc/CvcLexer.h" -#include "parser/cvc/CvcParser.h" -#include "parser/parser_exception.h" - -namespace cvc5 { -namespace parser { - -/* Use lookahead=3 */ -CvcInput::CvcInput(AntlrInputStream& inputStream) : - AntlrInput(inputStream,6) { - pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - Assert(input != NULL); - - d_pCvcLexer = CvcLexerNew(input); - if( d_pCvcLexer == NULL ) { - throw ParserException("Failed to create CVC lexer."); - } - - setAntlr3Lexer( d_pCvcLexer->pLexer ); - - pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - Assert(tokenStream != NULL); - - d_pCvcParser = CvcParserNew(tokenStream); - if( d_pCvcParser == NULL ) { - throw ParserException("Failed to create CVC parser."); - } - - setAntlr3Parser(d_pCvcParser->pParser); -} - - -CvcInput::~CvcInput() { - d_pCvcLexer->free(d_pCvcLexer); - d_pCvcParser->free(d_pCvcParser); -} - -Command* CvcInput::parseCommand() { - return d_pCvcParser->parseCommand(d_pCvcParser); -} - -api::Term CvcInput::parseExpr() -{ - return d_pCvcParser->parseExpr(d_pCvcParser); -} - -/* -pANTLR3_LEXER CvcInput::getLexer() { - return d_pCvcLexer->pLexer; -} -*/ - -} // namespace parser -} // namespace cvc5 diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h deleted file mode 100644 index 128acbd29..000000000 --- a/src/parser/cvc/cvc_input.h +++ /dev/null @@ -1,79 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Christopher L. Conway, Mathias Preiner, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - */ - -#include "cvc5parser_private.h" - -#ifndef CVC5__PARSER__CVC_INPUT_H -#define CVC5__PARSER__CVC_INPUT_H - -#include "parser/antlr_input.h" -#include "parser/cvc/CvcLexer.h" -#include "parser/cvc/CvcParser.h" - -// extern void CvcParserSetAntlrParser(cvc5::parser::AntlrParser* -// newAntlrParser); - -namespace cvc5 { - -class Command; -class Expr; - -namespace parser { - -class CvcInput : public AntlrInput { - /** The ANTLR3 CVC lexer for the input. */ - pCvcLexer d_pCvcLexer; - - /** The ANTLR3 CVC parser for the input. */ - pCvcParser d_pCvcParser; - - public: - /** Create an input. - * - * @param inputStream the input to parse - */ - CvcInput(AntlrInputStream& inputStream); - - /** Destructor. Frees the lexer and the parser. */ - virtual ~CvcInput(); - - protected: - /** Parse a command from the input. Returns <code>NULL</code> if there is - * no command there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - Command* parseCommand() override; - - /** Parse an expression from the input. Returns a null <code>api::Term</code> - * if there is no expression there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - api::Term parseExpr() override; - - private: - /** Initialize the class. Called from the constructors once the input stream - * is initialized. */ - void init(); - -}; // class CvcInput - -} // namespace parser -} // namespace cvc5 - -#endif /* CVC5__PARSER__CVC_INPUT_H */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index b1bb9a432..25e08b84e 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -20,7 +20,6 @@ #include "api/cpp/cvc5.h" #include "base/check.h" -#include "cvc/cvc.h" #include "parser/antlr_input.h" #include "parser/input.h" #include "parser/parser.h" @@ -58,17 +57,14 @@ void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) Parser* ParserBuilder::build() { Parser* parser = NULL; - if (d_lang == "LANG_SYGUS_V2" || d_lang == "LANG_SMTLIB_V2_6") - { - parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); - } - else if (d_lang == "LANG_TPTP") + if (d_lang == "LANG_TPTP") { parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly); } else { - parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly); + Assert(d_lang == "LANG_SYGUS_V2" || d_lang == "LANG_SMTLIB_V2_6"); + parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); } if( d_checksEnabled ) { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 40716d908..fc75ac552 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -604,6 +604,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::PRODUCT, "product"); addOperator(api::TRANSPOSE, "transpose"); addOperator(api::TCLOSURE, "tclosure"); + addOperator(api::JOIN_IMAGE, "join_image"); + addOperator(api::IDEN, "iden"); } if (d_logic.isTheoryEnabled(theory::THEORY_BAGS)) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp deleted file mode 100644 index 04274ddc3..000000000 --- a/src/printer/cvc/cvc_printer.cpp +++ /dev/null @@ -1,1558 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Dejan Jovanovic - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The pretty-printer interface for the CVC output language. - */ - -#include "printer/cvc/cvc_printer.h" - -#include <algorithm> -#include <iostream> -#include <iterator> -#include <stack> -#include <string> -#include <typeinfo> -#include <vector> - -#include "expr/array_store_all.h" -#include "expr/ascription_type.h" -#include "expr/datatype_index.h" -#include "expr/dtype.h" -#include "expr/dtype_cons.h" -#include "expr/dtype_selector.h" -#include "expr/emptyset.h" -#include "expr/node_manager_attributes.h" // for VarNameAttr -#include "expr/node_visitor.h" -#include "expr/sequence.h" -#include "options/language.h" // for LANG_AST -#include "options/smt_options.h" -#include "printer/let_binding.h" -#include "smt/command.h" -#include "smt/node_command.h" -#include "smt/smt_engine.h" -#include "theory/arrays/theory_arrays_rewriter.h" -#include "theory/substitutions.h" -#include "theory/theory_model.h" -#include "util/bitvector.h" -#include "util/divisible.h" -#include "util/rational.h" -#include "util/string.h" - -using namespace std; - -namespace cvc5 { -namespace printer { -namespace cvc { - -void CvcPrinter::toStream(std::ostream& out, - TNode n, - int toDepth, - size_t dag) const -{ - if(dag != 0) { - LetBinding lbind(dag + 1); - toStreamNodeWithLetify(out, n, toDepth, false, &lbind); - } else { - toStreamNode(out, n, toDepth, false, nullptr); - } -} - -void toStreamRational(std::ostream& out, Node n, bool forceRational) -{ - Assert(n.getKind() == kind::CONST_RATIONAL); - const Rational& rat = n.getConst<Rational>(); - if (rat.isIntegral() && !forceRational) - { - out << rat.getNumerator(); - } - else - { - out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; - } -} - -void CvcPrinter::toStreamNode(std::ostream& out, - TNode n, - int depth, - bool bracket, - LetBinding* lbind) const -{ - if (depth == 0) { - out << "(...)"; - } else { - --depth; - } - - // null - if(n.getKind() == kind::NULL_EXPR) { - out << "null"; - return; - } - - // variables - if(n.isVar()) { - string s; - if(n.getAttribute(expr::VarNameAttr(), s)) { - out << s; - } else { - if(n.getKind() == kind::VARIABLE) { - out << "var_"; - } else { - out << n.getKind() << '_'; - } - out << n.getId(); - } - return; - } - if(n.isNullaryOp()) { - if( n.getKind() == kind::UNIVERSE_SET ){ - out << "UNIVERSE :: " << n.getType(); - }else{ - //unknown printer - out << n.getKind(); - } - return; - } - - // constants - if(n.getMetaKind() == kind::metakind::CONSTANT) { - switch(n.getKind()) { - case kind::BITVECTOR_TYPE: - out << "BITVECTOR(" << n.getConst<BitVectorSize>().d_size << ")"; - break; - case kind::CONST_BITVECTOR: { - const BitVector& bv = n.getConst<BitVector>(); - const Integer& x = bv.getValue(); - out << "0bin"; - unsigned size = bv.getSize(); - while (size-- > 0) - { - out << (x.testBit(size) ? '1' : '0'); - } - break; - } - case kind::CONST_BOOLEAN: - // the default would print "1" or "0" for bool, that's not correct - // for our purposes - out << (n.getConst<bool>() ? "TRUE" : "FALSE"); - break; - case kind::CONST_RATIONAL: { - toStreamRational(out, n, false); - break; - } - case kind::CONST_STRING: - { - out << '"' << n.getConst<String>().toString() << '"'; - break; - } - case kind::CONST_SEQUENCE: - { - const Sequence& sn = n.getConst<Sequence>(); - const std::vector<Node>& snvec = sn.getVec(); - if (snvec.size() > 1) - { - out << "CONCAT("; - } - bool first = true; - for (const Node& snvc : snvec) - { - if (!first) - { - out << ", "; - } - out << "SEQ_UNIT(" << snvc << ")"; - first = false; - } - if (snvec.size() > 1) - { - out << ")"; - } - break; - } - case kind::TYPE_CONSTANT: - switch(TypeConstant tc = n.getConst<TypeConstant>()) { - case REAL_TYPE: - out << "REAL"; - break; - case INTEGER_TYPE: - out << "INT"; - break; - case BOOLEAN_TYPE: - out << "BOOLEAN"; - break; - case STRING_TYPE: - out << "STRING"; - break; - default: - out << tc; - break; - } - break; - - case kind::DATATYPE_TYPE: { - const DType& dt = NodeManager::currentNM()->getDTypeForIndex( - n.getConst<DatatypeIndexConstant>().getIndex()); - if( dt.isTuple() ){ - out << '['; - for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { - if (i > 0) { - out << ", "; - } - TypeNode t = dt[0][i].getRangeType(); - out << t; - } - out << ']'; - } - else if (dt.isRecord()) - { - out << "[# "; - for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { - if (i > 0) { - out << ", "; - } - TypeNode t = dt[0][i].getRangeType(); - out << dt[0][i].getSelector() << ":" << t; - } - out << " #]"; - }else{ - out << dt.getName(); - } - } - break; - - case kind::EMPTYSET: - out << "{} :: " << n.getConst<EmptySet>().getType(); - break; - - case kind::STORE_ALL: { - const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); - out << "ARRAY(" << asa.getType().getArrayIndexType() << " OF " - << asa.getType().getArrayConstituentType() - << ") : " << asa.getValue(); - break; - } - - default: - // Fall back to whatever operator<< does on underlying type; we - // might luck out and print something reasonable. - kind::metakind::NodeValueConstPrinter::toStream(out, n); - } - - return; - } - - enum OpType { - PREFIX, - INFIX, - POSTFIX - } opType; - - //The default operation type is PREFIX - opType = PREFIX; - - stringstream op; // operation (such as '+') - - switch(n.getKind()) { - - // BUILTIN - case kind::EQUAL: - if( n[0].getType().isBoolean() ){ - op << "<=>"; - }else{ - op << '='; - } - opType = INFIX; - break; - case kind::ITE: - out << "IF "; - toStreamNode(out, n[0], depth, true, lbind); - out << " THEN "; - toStreamNode(out, n[1], depth, true, lbind); - out << " ELSE "; - toStreamNode(out, n[2], depth, true, lbind); - out << " ENDIF"; - return; - break; - case kind::SEXPR: - // no-op - break; - case kind::LAMBDA: - out << "(LAMBDA"; - toStreamNode(out, n[0], depth, true, lbind); - out << ": "; - toStreamNodeWithLetify(out, n[1], depth, true, lbind); - out << ")"; - return; - break; - case kind::WITNESS: - out << "(WITNESS"; - toStreamNode(out, n[0], depth, true, lbind); - out << " : "; - toStreamNodeWithLetify(out, n[1], depth, true, lbind); - out << ')'; - return; - case kind::DISTINCT: - // distinct not supported directly, blast it away with the rewriter - toStreamNode(out, theory::Rewriter::rewrite(n), depth, true, lbind); - return; - case kind::SORT_TYPE: - { - string name; - if(n.getAttribute(expr::VarNameAttr(), name)) { - out << name; - return; - } - } - break; - - // BOOL - case kind::AND: - op << "AND"; - opType = INFIX; - break; - case kind::OR: - op << "OR"; - opType = INFIX; - break; - case kind::NOT: - op << "NOT"; - opType = PREFIX; - break; - case kind::XOR: - op << "XOR"; - opType = INFIX; - break; - case kind::IMPLIES: - op << "=>"; - opType = INFIX; - break; - - // UF - case kind::APPLY_UF: - toStreamNode(op, n.getOperator(), depth, false, lbind); - break; - case kind::CARDINALITY_CONSTRAINT: - case kind::COMBINED_CARDINALITY_CONSTRAINT: - out << "CARDINALITY_CONSTRAINT"; - break; - - case kind::FUNCTION_TYPE: - if (n.getNumChildren() > 1) { - if (n.getNumChildren() > 2) { - out << '('; - } - for (unsigned i = 1; i < n.getNumChildren(); ++i) { - if (i > 1) { - out << ", "; - } - toStreamNode(out, n[i - 1], depth, false, lbind); - } - if (n.getNumChildren() > 2) { - out << ')'; - } - } - out << " -> "; - toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); - return; - break; - - // DATATYPES - case kind::PARAMETRIC_DATATYPE: { - const DType& dt = NodeManager::currentNM()->getDTypeForIndex( - n[0].getConst<DatatypeIndexConstant>().getIndex()); - out << dt.getName() << '['; - for (unsigned i = 1; i < n.getNumChildren(); ++i) - { - if (i > 1) - { - out << ','; - } - out << n[i]; - } - out << ']'; - } - return; - break; - case kind::APPLY_TYPE_ASCRIPTION: { - toStreamNode(out, n[0], depth, false, lbind); - out << "::"; - TypeNode t = n.getOperator().getConst<AscriptionType>().getType(); - out << (t.isFunctionLike() ? t.getRangeType() : t); - } - return; - break; - case kind::APPLY_CONSTRUCTOR: { - TypeNode t = n.getType(); - if( t.isTuple() ){ - if( n.getNumChildren()==1 ){ - out << "TUPLE"; - } - } - else if (t.isRecord()) - { - const DType& dt = t.getDType(); - const DTypeConstructor& recCons = dt[0]; - out << "(# "; - for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++) - { - if (i != 0) - { - out << ", "; - } - out << recCons[i].getName() << " := "; - toStreamNode(out, n[i], depth, false, lbind); - } - out << " #)"; - return; - } - else - { - toStreamNode(op, n.getOperator(), depth, false, lbind); - if (n.getNumChildren() == 0) - { - // for datatype constants d, we print "d" and not "d()" - out << op.str(); - return; - } - } - } - break; - case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: { - TypeNode t = n[0].getType(); - Node opn = n.getOperator(); - if (!t.isDatatype()) - { - toStreamNode(op, opn, depth, false, lbind); - } - else if (t.isTuple() || t.isRecord()) - { - toStreamNode(out, n[0], depth, true, lbind); - out << '.'; - const DType& dt = t.getDType(); - if (t.isTuple()) - { - int sindex; - if (n.getKind() == kind::APPLY_SELECTOR) - { - sindex = DType::indexOf(opn); - } - else - { - sindex = dt[0].getSelectorIndexInternal(opn); - } - Assert(sindex >= 0); - out << sindex; - } - else - { - toStreamNode(out, opn, depth, false, lbind); - } - return; - }else{ - toStreamNode(op, opn, depth, false, lbind); - } - } - break; - case kind::APPLY_TESTER: { - Assert(!n.getType().isTuple() && !n.getType().isRecord()); - op << "is_"; - unsigned cindex = DType::indexOf(n.getOperator()); - const DType& dt = DType::datatypeOf(n.getOperator()); - toStreamNode(op, dt[cindex].getConstructor(), depth, false, lbind); - } - break; - case kind::CONSTRUCTOR_TYPE: - case kind::SELECTOR_TYPE: - if(n.getNumChildren() > 1) { - if(n.getNumChildren() > 2) { - out << '('; - } - for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { - if(i > 0) { - out << ", "; - } - toStreamNode(out, n[i], depth, false, lbind); - } - if(n.getNumChildren() > 2) { - out << ')'; - } - out << " -> "; - } - toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); - return; - case kind::TESTER_TYPE: - toStreamNode(out, n[0], depth, false, lbind); - out << " -> BOOLEAN"; - return; - break; - - // ARRAYS - case kind::ARRAY_TYPE: - out << "ARRAY "; - toStreamNode(out, n[0], depth, false, lbind); - out << " OF "; - toStreamNode(out, n[1], depth, false, lbind); - return; - break; - case kind::SELECT: - toStreamNode(out, n[0], depth, true, lbind); - out << '['; - toStreamNode(out, n[1], depth, false, lbind); - out << ']'; - return; - break; - case kind::STORE: { - stack<TNode> stk; - stk.push(n); - while(stk.top()[0].getKind() == kind::STORE) { - stk.push(stk.top()[0]); - } - if (bracket) { - out << '('; - } - TNode x = stk.top(); - toStreamNode(out, x[0], depth, false, lbind); - out << " WITH ["; - toStreamNode(out, x[1], depth, false, lbind); - out << "] := "; - toStreamNode(out, x[2], depth, false, lbind); - stk.pop(); - while(!stk.empty()) { - x = stk.top(); - out << ", ["; - toStreamNode(out, x[1], depth, false, lbind); - out << "] := "; - toStreamNode(out, x[2], depth, false, lbind); - stk.pop(); - } - if (bracket) { - out << ')'; - } - return; - break; - } - - // ARITHMETIC - case kind::PLUS: - op << '+'; - opType = INFIX; - break; - case kind::MULT: - case kind::NONLINEAR_MULT: - op << '*'; - opType = INFIX; - break; - case kind::MINUS: - op << '-'; - opType = INFIX; - break; - case kind::UMINUS: - op << '-'; - opType = PREFIX; - break; - case kind::DIVISION: - case kind::DIVISION_TOTAL: - op << '/'; - opType = INFIX; - break; - case kind::INTS_DIVISION: - case kind::INTS_DIVISION_TOTAL: - op << "DIV"; - opType = INFIX; - break; - case kind::INTS_MODULUS: - case kind::INTS_MODULUS_TOTAL: - op << "MOD"; - opType = INFIX; - break; - case kind::LT: - op << '<'; - opType = INFIX; - break; - case kind::LEQ: - op << "<="; - opType = INFIX; - break; - case kind::GT: - op << '>'; - opType = INFIX; - break; - case kind::GEQ: - op << ">="; - opType = INFIX; - break; - case kind::POW: - op << '^'; - opType = INFIX; - break; - case kind::ABS: - op << "ABS"; - opType = PREFIX; - break; - case kind::IS_INTEGER: - op << "IS_INTEGER"; - opType = PREFIX; - break; - case kind::TO_INTEGER: - op << "FLOOR"; - opType = PREFIX; - break; - case kind::TO_REAL: - case kind::CAST_TO_REAL: - { - if (n[0].getKind() == kind::CONST_RATIONAL) - { - // print the constant as a rational - toStreamRational(out, n[0], true); - } - else - { - // ignore, there is no to-real in CVC language - toStreamNode(out, n[0], depth, false, lbind); - } - return; - } - case kind::DIVISIBLE: - out << "DIVISIBLE("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getOperator().getConst<Divisible>().k << ")"; - return; - - // BITVECTORS - case kind::BITVECTOR_XOR: - op << "BVXOR"; - break; - case kind::BITVECTOR_NAND: - op << "BVNAND"; - break; - case kind::BITVECTOR_NOR: - op << "BVNOR"; - break; - case kind::BITVECTOR_XNOR: - op << "BVXNOR"; - break; - case kind::BITVECTOR_COMP: - op << "BVCOMP"; - break; - case kind::BITVECTOR_UDIV: - op << "BVUDIV"; - break; - case kind::BITVECTOR_UREM: - op << "BVUREM"; - break; - case kind::BITVECTOR_SDIV: - op << "BVSDIV"; - break; - case kind::BITVECTOR_SREM: - op << "BVSREM"; - break; - case kind::BITVECTOR_SMOD: - op << "BVSMOD"; - break; - case kind::BITVECTOR_SHL: - op << "BVSHL"; - break; - case kind::BITVECTOR_LSHR: - op << "BVLSHR"; - break; - case kind::BITVECTOR_ASHR: - op << "BVASHR"; - break; - case kind::BITVECTOR_ULT: - op << "BVLT"; - break; - case kind::BITVECTOR_ULE: - op << "BVLE"; - break; - case kind::BITVECTOR_UGT: - op << "BVGT"; - break; - case kind::BITVECTOR_UGE: - op << "BVGE"; - break; - case kind::BITVECTOR_SLT: - op << "BVSLT"; - break; - case kind::BITVECTOR_SLE: - op << "BVSLE"; - break; - case kind::BITVECTOR_SGT: - op << "BVSGT"; - break; - case kind::BITVECTOR_SGE: - op << "BVSGE"; - break; - case kind::BITVECTOR_NEG: - op << "BVUMINUS"; - break; - case kind::BITVECTOR_NOT: - op << "~"; - break; - case kind::BITVECTOR_AND: - op << "&"; - opType = INFIX; - break; - case kind::BITVECTOR_OR: - op << "|"; - opType = INFIX; - break; - case kind::BITVECTOR_CONCAT: - op << "@"; - opType = INFIX; - break; - case kind::BITVECTOR_ADD: - { - // This interprets a BITVECTOR_ADD as a bvadd in SMT-LIB - Assert(n.getType().isBitVector()); - unsigned numc = n.getNumChildren()-2; - unsigned child = 0; - while (child < numc) { - out << "BVPLUS("; - out << n.getType().getBitVectorSize(); - out << ','; - toStreamNode(out, n[child], depth, false, lbind); - out << ','; - ++child; - } - out << "BVPLUS("; - out << n.getType().getBitVectorSize(); - out << ','; - toStreamNode(out, n[child], depth, false, lbind); - out << ','; - toStreamNode(out, n[child + 1], depth, false, lbind); - while (child > 0) { - out << ')'; - --child; - } - out << ')'; - return; - break; - } - case kind::BITVECTOR_SUB: - out << "BVSUB("; - Assert(n.getType().isBitVector()); - out << n.getType().getBitVectorSize(); - out << ','; - toStreamNode(out, n[0], depth, false, lbind); - out << ','; - toStreamNode(out, n[1], depth, false, lbind); - out << ')'; - return; - break; - case kind::BITVECTOR_MULT: { - Assert(n.getType().isBitVector()); - unsigned numc = n.getNumChildren()-2; - unsigned child = 0; - while (child < numc) { - out << "BVMULT("; - out << n.getType().getBitVectorSize(); - out << ','; - toStreamNode(out, n[child], depth, false, lbind); - out << ','; - ++child; - } - out << "BVMULT("; - out << n.getType().getBitVectorSize(); - out << ','; - toStreamNode(out, n[child], depth, false, lbind); - out << ','; - toStreamNode(out, n[child + 1], depth, false, lbind); - while (child > 0) { - out << ')'; - --child; - } - out << ')'; - return; - break; - } - case kind::BITVECTOR_EXTRACT: - op << n.getOperator().getConst<BitVectorExtract>(); - opType = POSTFIX; - break; - case kind::BITVECTOR_BITOF: - op << n.getOperator().getConst<BitVectorBitOf>(); - opType = POSTFIX; - break; - case kind::BITVECTOR_REPEAT: - out << "BVREPEAT("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')'; - return; - break; - case kind::BITVECTOR_ZERO_EXTEND: - out << "BVZEROEXTEND("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')'; - return; - break; - case kind::BITVECTOR_SIGN_EXTEND: - out << "SX("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getType().getBitVectorSize() << ')'; - return; - break; - case kind::BITVECTOR_ROTATE_LEFT: - out << "BVROTL("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')'; - return; - break; - case kind::BITVECTOR_ROTATE_RIGHT: - out << "BVROTR("; - toStreamNode(out, n[0], depth, false, lbind); - out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')'; - return; - break; - - // SETS - case kind::SET_TYPE: - out << "SET OF "; - toStreamNode(out, n[0], depth, false, lbind); - return; - break; - case kind::UNION: - op << '|'; - opType = INFIX; - break; - case kind::INTERSECTION: - op << '&'; - opType = INFIX; - break; - case kind::SETMINUS: - op << '-'; - opType = INFIX; - break; - case kind::SUBSET: - op << "<="; - opType = INFIX; - break; - case kind::MEMBER: - op << "IS_IN"; - opType = INFIX; - break; - case kind::COMPLEMENT: - op << "~"; - opType = PREFIX; - break; - case kind::PRODUCT: - op << "PRODUCT"; - opType = INFIX; - break; - case kind::JOIN: - op << "JOIN"; - opType = INFIX; - break; - case kind::TRANSPOSE: - op << "TRANSPOSE"; - opType = PREFIX; - break; - case kind::TCLOSURE: - op << "TCLOSURE"; - opType = PREFIX; - break; - case kind::IDEN: - op << "IDEN"; - opType = PREFIX; - break; - case kind::JOIN_IMAGE: - op << "JOIN_IMAGE"; - opType = INFIX; - break; - case kind::SINGLETON: - out << "{"; - toStreamNode(out, n[0], depth, false, lbind); - out << "}"; - return; - break; - case kind::INSERT: { - if(bracket) { - out << '('; - } - out << '{'; - size_t i = 0; - toStreamNode(out, n[i++], depth, false, lbind); - for(;i+1 < n.getNumChildren(); ++i) { - out << ", "; - toStreamNode(out, n[i], depth, false, lbind); - } - out << "} | "; - toStreamNode(out, n[i], depth, true, lbind); - if(bracket) { - out << ')'; - } - return; - break; - } - case kind::CARD: { - out << "CARD("; - toStreamNode(out, n[0], depth, false, lbind); - out << ")"; - return; - break; - } - - // Quantifiers - case kind::FORALL: - out << "(FORALL"; - toStreamNode(out, n[0], depth, true, lbind); - out << " : "; - toStreamNodeWithLetify(out, n[1], depth, true, lbind); - out << ')'; - // TODO: user patterns? - return; - case kind::EXISTS: - out << "(EXISTS"; - toStreamNode(out, n[0], depth, true, lbind); - out << " : "; - toStreamNodeWithLetify(out, n[1], depth, true, lbind); - out << ')'; - // TODO: user patterns? - return; - case kind::INST_CONSTANT: - out << "INST_CONSTANT"; - break; - case kind::BOUND_VAR_LIST: - out << '('; - for(size_t i = 0; i < n.getNumChildren(); ++i) { - if(i > 0) { - out << ", "; - } - toStreamNode(out, n[i], -1, false, lbind); - out << ":"; - n[i].getType().toStream(out, Language::LANG_CVC); - } - out << ')'; - return; - case kind::INST_PATTERN: - out << "INST_PATTERN"; - break; - case kind::INST_PATTERN_LIST: - out << "INST_PATTERN_LIST"; - break; - - // string operators - case kind::STRING_CONCAT: - out << "CONCAT"; - break; - case kind::STRING_CHARAT: - out << "CHARAT"; - break; - case kind::STRING_LENGTH: - out << "LENGTH"; - break; - case kind::STRING_SUBSTR: out << "SUBSTR"; break; - - default: - Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl; - break; - } - - switch (opType) { - case PREFIX: - out << op.str(); - if (n.getNumChildren() > 0) - { - out << '('; - } - break; - case INFIX: - if (bracket) { - out << '('; - } - break; - case POSTFIX: - out << '('; - break; - } - - for (unsigned i = 0; i < n.getNumChildren(); ++ i) { - if (i > 0) { - if (opType == INFIX) { - out << ' ' << op.str() << ' '; - } else { - out << ", "; - } - } - toStreamNode(out, n[i], depth, opType == INFIX, lbind); - } - - switch (opType) { - case PREFIX: - if (n.getNumChildren() > 0) - { - out << ')'; - } - break; - case INFIX: - if (bracket) { - out << ')'; - } - break; - case POSTFIX: - out << ')' << op.str(); - break; - } -} - -template <class T> -static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode); - -template <class T> -static bool tryToStream(std::ostream& out, - const CommandStatus* s, - bool cvc3Mode); - -void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const -{ - if (tryToStream<CommandSuccess>(out, s, d_cvc3Mode) - || tryToStream<CommandFailure>(out, s, d_cvc3Mode) - || tryToStream<CommandRecoverableFailure>(out, s, d_cvc3Mode) - || tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) - || tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) - { - return; - } - - out << "ERROR: don't know how to print a CommandStatus of class: " - << typeid(*s).name() << endl; - -}/* CvcPrinter::toStream(CommandStatus*) */ - -void CvcPrinter::toStreamModelSort(std::ostream& out, - TypeNode tn, - const std::vector<Node>& elements) const -{ - if (!tn.isSort()) - { - out << "ERROR: don't know how to print a non uninterpreted sort in model: " - << tn << std::endl; - return; - } - out << "% cardinality of " << tn << " is " << elements.size() << std::endl; - toStreamCmdDeclareType(out, tn); - for (const Node& type_rep : elements) - { - if (type_rep.isVar()) - { - out << type_rep << " : " << tn << ";" << std::endl; - } - else - { - out << "% rep: " << type_rep << std::endl; - } - } -} - -void CvcPrinter::toStreamModelTerm(std::ostream& out, - const Node& n, - const Node& value) const -{ - TypeNode tn = n.getType(); - out << n << " : "; - if (tn.isFunction() || tn.isPredicate()) - { - out << "("; - for (size_t i = 0; i < tn.getNumChildren() - 1; i++) - { - if (i > 0) - { - out << ", "; - } - out << tn[i]; - } - out << ") -> " << tn.getRangeType(); - } - else - { - out << tn; - } - out << " = " << value << ";" << std::endl; -} - -void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const -{ - // print the model - out << "MODEL BEGIN" << std::endl; - this->Printer::toStream(out, m); - out << "MODEL END;" << std::endl; -} - -void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const -{ - out << "ASSERT " << n << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdPush(std::ostream& out) const -{ - out << "PUSH;" << std::endl; -} - -void CvcPrinter::toStreamCmdPop(std::ostream& out) const -{ - out << "POP;" << std::endl; -} - -void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const -{ - if (d_cvc3Mode) - { - out << "PUSH; "; - } - if (!n.isNull()) - { - out << "CHECKSAT " << n << ';'; - } - else - { - out << "CHECKSAT;"; - } - if (d_cvc3Mode) - { - out << " POP;"; - } - out << std::endl; -} - -void CvcPrinter::toStreamCmdCheckSatAssuming( - std::ostream& out, const std::vector<Node>& nodes) const -{ - if (d_cvc3Mode) - { - out << "PUSH; "; - } - out << "CHECKSAT"; - if (nodes.size() > 0) - { - out << ' ' << nodes[0]; - for (size_t i = 1, n = nodes.size(); i < n; ++i) - { - out << " AND " << nodes[i]; - } - } - out << ';'; - if (d_cvc3Mode) - { - out << " POP;"; - } - out << std::endl; -} - -void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const -{ - if (d_cvc3Mode) - { - out << "PUSH; "; - } - if (!n.isNull()) - { - out << "QUERY " << n << ';'; - } - else - { - out << "QUERY TRUE;"; - } - if (d_cvc3Mode) - { - out << " POP;"; - } - out << std::endl; -} - -void CvcPrinter::toStreamCmdReset(std::ostream& out) const -{ - out << "RESET;" << std::endl; -} - -void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const -{ - out << "RESET ASSERTIONS;" << std::endl; -} - -void CvcPrinter::toStreamCmdQuit(std::ostream& out) const -{ - // out << "EXIT;" << std::endl; -} - -void CvcPrinter::toStreamCmdCommandSequence( - std::ostream& out, const std::vector<Command*>& sequence) const -{ - for (CommandSequence::const_iterator i = sequence.cbegin(); - i != sequence.cend(); - ++i) - { - out << *i; - } -} - -void CvcPrinter::toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector<Command*>& sequence) const -{ - DeclarationSequence::const_iterator i = sequence.cbegin(); - for (;;) - { - DeclarationDefinitionCommand* dd = - static_cast<DeclarationDefinitionCommand*>(*i++); - Assert(dd != nullptr); - if (i != sequence.cend()) - { - out << dd->getSymbol() << ", "; - } - else - { - out << *dd; - break; - } - } - out << std::endl; -} - -void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out, - const std::string& id, - TypeNode type) const -{ - out << id << " : " << type << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const -{ - std::vector<TypeNode> sorts; - sorts.reserve(formals.size() + 1); - for (const Node& n : formals) - { - sorts.push_back(n.getType()); - } - sorts.push_back(range); - - out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts) - << " = "; - if (formals.size() > 0) - { - out << "LAMBDA("; - vector<Node>::const_iterator i = formals.cbegin(); - while (i != formals.end()) - { - out << (*i) << ":" << (*i).getType(); - if (++i != formals.end()) - { - out << ", "; - } - } - out << "): "; - } - out << formula << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, - TypeNode type) const -{ - size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0; - if (arity > 0) - { - out << "ERROR: Don't know how to print parameterized type declaration " - "in CVC language." - << std::endl; - } - else - { - out << type << " : TYPE;" << std::endl; - } -} - -void CvcPrinter::toStreamCmdDefineType(std::ostream& out, - const std::string& id, - const std::vector<TypeNode>& params, - TypeNode t) const -{ - if (params.size() > 0) - { - out << "ERROR: Don't know how to print parameterized type definition " - "in CVC language:" - << std::endl; - } - else - { - out << id << " : TYPE = " << t << ';' << std::endl; - } -} - -void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const -{ - out << "TRANSFORM " << n << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdGetValue(std::ostream& out, - const std::vector<Node>& nodes) const -{ - Assert(!nodes.empty()); - out << "GET_VALUE "; - copy(nodes.begin(), - nodes.end() - 1, - ostream_iterator<Node>(out, ";\nGET_VALUE ")); - out << nodes.back() << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const -{ - out << "COUNTERMODEL;" << std::endl; -} - -void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const -{ - out << "% (get-assignment)" << std::endl; -} - -void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const -{ - out << "WHERE;" << std::endl; -} - -void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const -{ - out << "DUMP_PROOF;" << std::endl; -} - -void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const -{ - out << "DUMP_UNSAT_CORE;" << std::endl; -} - -void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out, - Result::Sat status) const -{ - out << "% (set-info :status " << status << ')' << std::endl; -} - -void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out, - const std::string& logic) const -{ - out << "OPTION \"logic\" \"" << logic << "\";" << std::endl; -} - -void CvcPrinter::toStreamCmdSetInfo(std::ostream& out, - const std::string& flag, - const std::string& value) const -{ - out << "% (set-info " << flag << ' ' << value << ')' << std::endl; -} - -void CvcPrinter::toStreamCmdGetInfo(std::ostream& out, - const std::string& flag) const -{ - out << "% (get-info " << flag << ')' << std::endl; -} - -void CvcPrinter::toStreamCmdSetOption(std::ostream& out, - const std::string& flag, - const std::string& value) const -{ - out << "OPTION \"" << flag << "\" " << value << ';' << std::endl; -} - -void CvcPrinter::toStreamCmdGetOption(std::ostream& out, - const std::string& flag) const -{ - out << "% (get-option " << flag << ')' << std::endl; -} - -void CvcPrinter::toStreamCmdDatatypeDeclaration( - std::ostream& out, const std::vector<TypeNode>& datatypes) const -{ - Assert(!datatypes.empty() && datatypes[0].isDatatype()); - const DType& dt0 = datatypes[0].getDType(); - // do not print tuple/datatype internal declarations - if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord())) - { - out << "DATATYPE" << endl; - bool firstDatatype = true; - for (const TypeNode& t : datatypes) - { - if (!firstDatatype) - { - out << ',' << endl; - } - const DType& dt = t.getDType(); - out << " " << dt.getName(); - if (dt.isParametric()) - { - out << '['; - for (size_t j = 0; j < dt.getNumParameters(); ++j) - { - if (j > 0) - { - out << ','; - } - out << dt.getParameter(j); - } - out << ']'; - } - out << " = "; - for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) - { - const DTypeConstructor& cons = dt[j]; - if (j != 0) - { - out << " | "; - } - out << cons.getName(); - if (cons.getNumArgs() > 0) - { - out << '('; - for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++) - { - if (k != 0) - { - out << ", "; - } - const DTypeSelector& selector = cons[k]; - TypeNode tr = selector.getRangeType(); - if (tr.isDatatype()) - { - const DType& sdt = tr.getDType(); - out << selector.getName() << ": " << sdt.getName(); - } - else - { - out << selector.getName() << ": " << tr; - } - } - out << ')'; - } - } - firstDatatype = false; - } - out << endl << "END;" << std::endl; - } -} - -void CvcPrinter::toStreamCmdComment(std::ostream& out, - const std::string& comment) const -{ - out << "% " << comment << std::endl; -} - -void CvcPrinter::toStreamCmdEmpty(std::ostream& out, - const std::string& name) const -{ - out << std::endl; -} - -void CvcPrinter::toStreamCmdEcho(std::ostream& out, - const std::string& output) const -{ - out << "ECHO \"" << output << "\";" << std::endl; -} - -template <class T> -static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) -{ - if(typeid(*c) == typeid(T)) { - toStream(out, dynamic_cast<const T*>(c), cvc3Mode); - return true; - } - return false; -} - -static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) -{ - if(Command::printsuccess::getPrintSuccess(out)) { - out << "OK" << endl; - } -} - -static void toStream(std::ostream& out, - const CommandUnsupported* s, - bool cvc3Mode) -{ - out << "UNSUPPORTED" << endl; -} - -static void toStream(std::ostream& out, - const CommandInterrupted* s, - bool cvc3Mode) -{ - out << "INTERRUPTED" << endl; -} - -static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) -{ - out << s->getMessage() << endl; -} - -static void toStream(std::ostream& out, - const CommandRecoverableFailure* s, - bool cvc3Mode) -{ - out << s->getMessage() << endl; -} - -template <class T> -static bool tryToStream(std::ostream& out, - const CommandStatus* s, - bool cvc3Mode) -{ - if(typeid(*s) == typeid(T)) { - toStream(out, dynamic_cast<const T*>(s), cvc3Mode); - return true; - } - return false; -} - -void CvcPrinter::toStreamNodeWithLetify(std::ostream& out, - Node n, - int toDepth, - bool bracket, - LetBinding* lbind) const -{ - if (lbind == nullptr) - { - toStreamNode(out, n, toDepth, bracket, nullptr); - return; - } - std::vector<Node> letList; - lbind->letify(n, letList); - if (!letList.empty()) - { - std::map<Node, uint32_t>::const_iterator it; - out << "LET "; - bool first = true; - for (size_t i = 0, nlets = letList.size(); i < nlets; i++) - { - if (!first) - { - out << ", "; - } - else - { - first = false; - } - Node nl = letList[i]; - uint32_t id = lbind->getId(nl); - out << "_let_" << id << " = "; - Node nlc = lbind->convert(nl, "_let_", false); - toStreamNode(out, nlc, toDepth, true, lbind); - } - out << " IN "; - } - Node nc = lbind->convert(n, "_let_"); - // print the body, passing the lbind object - toStreamNode(out, nc, toDepth, bracket, lbind); - lbind->popScope(); -} - -} // namespace cvc -} // namespace printer -} // namespace cvc5 diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h deleted file mode 100644 index 4851868d3..000000000 --- a/src/printer/cvc/cvc_printer.h +++ /dev/null @@ -1,208 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Andrew Reynolds, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The pretty-printer interface for the CVC output language. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__PRINTER__CVC_PRINTER_H -#define CVC5__PRINTER__CVC_PRINTER_H - -#include <iostream> - -#include "printer/printer.h" - -namespace cvc5 { - -class LetBinding; - -namespace printer { -namespace cvc { - -class CvcPrinter : public cvc5::Printer -{ - public: - using cvc5::Printer::toStream; - CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {} - void toStream(std::ostream& out, - TNode n, - int toDepth, - size_t dag) const override; - void toStream(std::ostream& out, const CommandStatus* s) const override; - void toStream(std::ostream& out, const smt::Model& m) const override; - - /** Print empty command */ - void toStreamCmdEmpty(std::ostream& out, - const std::string& name) const override; - - /** Print echo command */ - void toStreamCmdEcho(std::ostream& out, - const std::string& output) const override; - - /** Print assert command */ - void toStreamCmdAssert(std::ostream& out, Node n) const override; - - /** Print push command */ - void toStreamCmdPush(std::ostream& out) const override; - - /** Print pop command */ - void toStreamCmdPop(std::ostream& out) const override; - - /** Print declare-fun command */ - void toStreamCmdDeclareFunction(std::ostream& out, - const std::string& id, - TypeNode type) const override; - - /** Print declare-sort command */ - void toStreamCmdDeclareType(std::ostream& out, - TypeNode type) const override; - - /** Print define-sort command */ - void toStreamCmdDefineType(std::ostream& out, - const std::string& id, - const std::vector<TypeNode>& params, - TypeNode t) const override; - - /** Print define-fun command */ - void toStreamCmdDefineFunction(std::ostream& out, - const std::string& id, - const std::vector<Node>& formals, - TypeNode range, - Node formula) const override; - - /** Print check-sat command */ - void toStreamCmdCheckSat(std::ostream& out, - Node n = Node::null()) const override; - - /** Print check-sat-assuming command */ - void toStreamCmdCheckSatAssuming( - std::ostream& out, const std::vector<Node>& nodes) const override; - - /** Print query command */ - void toStreamCmdQuery(std::ostream& out, Node n) const override; - - /** Print simplify command */ - void toStreamCmdSimplify(std::ostream& out, Node nodes) const override; - - /** Print get-value command */ - void toStreamCmdGetValue(std::ostream& out, - const std::vector<Node>& n) const override; - - /** Print get-assignment command */ - void toStreamCmdGetAssignment(std::ostream& out) const override; - - /** Print get-model command */ - void toStreamCmdGetModel(std::ostream& out) const override; - - /** Print get-proof command */ - void toStreamCmdGetProof(std::ostream& out) const override; - - /** Print get-unsat-core command */ - void toStreamCmdGetUnsatCore(std::ostream& out) const override; - - /** Print get-assertions command */ - void toStreamCmdGetAssertions(std::ostream& out) const override; - - /** Print set-info :status command */ - void toStreamCmdSetBenchmarkStatus(std::ostream& out, - Result::Sat status) const override; - - /** Print set-logic command */ - void toStreamCmdSetBenchmarkLogic(std::ostream& out, - const std::string& logic) const override; - - /** Print set-info command */ - void toStreamCmdSetInfo(std::ostream& out, - const std::string& flag, - const std::string& value) const override; - - /** Print get-info command */ - void toStreamCmdGetInfo(std::ostream& out, - const std::string& flag) const override; - - /** Print set-option command */ - void toStreamCmdSetOption(std::ostream& out, - const std::string& flag, - const std::string& value) const override; - - /** Print get-option command */ - void toStreamCmdGetOption(std::ostream& out, - const std::string& flag) const override; - - /** Print declare-datatype(s) command */ - void toStreamCmdDatatypeDeclaration( - std::ostream& out, const std::vector<TypeNode>& datatypes) const override; - - /** Print reset command */ - void toStreamCmdReset(std::ostream& out) const override; - - /** Print reset-assertions command */ - void toStreamCmdResetAssertions(std::ostream& out) const override; - - /** Print quit command */ - void toStreamCmdQuit(std::ostream& out) const override; - - /** Print comment command */ - void toStreamCmdComment(std::ostream& out, - const std::string& comment) const override; - - /** Print command sequence command */ - void toStreamCmdCommandSequence( - std::ostream& out, const std::vector<Command*>& sequence) const override; - - /** Print declaration sequence command */ - void toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector<Command*>& sequence) const override; - - private: - /** - * The main method for printing Nodes. - */ - void toStreamNode(std::ostream& out, - TNode n, - int toDepth, - bool bracket, - LetBinding* lbind) const; - /** - * To stream model sort. This prints the appropriate output for type - * tn declared via declare-sort. - */ - void toStreamModelSort(std::ostream& out, - TypeNode tn, - const std::vector<Node>& elements) const override; - - /** - * To stream model term. This prints the appropriate output for term - * n declared via declare-fun. - */ - void toStreamModelTerm(std::ostream& out, - const Node& n, - const Node& value) const override; - /** - * To stream with let binding. This prints n, possibly in the scope - * of letification generated by this method based on lbind. - */ - void toStreamNodeWithLetify(std::ostream& out, - Node n, - int toDepth, - bool bracket, - LetBinding* lbind) const; - - bool d_cvc3Mode; -}; /* class CvcPrinter */ - -} // namespace cvc -} // namespace printer -} // namespace cvc5 - -#endif /* CVC5__PRINTER__CVC_PRINTER_H */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index f1ad9212f..582c60d40 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -19,7 +19,6 @@ #include "options/base_options.h" #include "options/language.h" #include "printer/ast/ast_printer.h" -#include "printer/cvc/cvc_printer.h" #include "printer/smt2/smt2_printer.h" #include "printer/tptp/tptp_printer.h" #include "proof/unsat_core.h" @@ -44,9 +43,6 @@ unique_ptr<Printer> Printer::makePrinter(Language lang) case Language::LANG_TPTP: return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); - case Language::LANG_CVC: - return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); - case Language::LANG_SYGUS_V2: // sygus version 2.0 does not have discrepancies with smt2, hence we use // a normal smt2 variant here. |