summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/expr/dtype.cpp2
-rw-r--r--src/expr/dtype_cons.cpp2
-rw-r--r--src/expr/dtype_selector.cpp2
-rw-r--r--src/main/CMakeLists.txt1
-rw-r--r--src/main/driver_unified.cpp5
-rw-r--r--src/main/interactive_shell.cpp12
-rw-r--r--src/options/language.cpp13
-rw-r--r--src/options/language.h2
-rw-r--r--src/parser/CMakeLists.txt6
-rw-r--r--src/parser/antlr_input.cpp7
-rw-r--r--src/parser/cvc/Cvc.g2459
-rw-r--r--src/parser/cvc/README98
-rw-r--r--src/parser/cvc/cvc.cpp37
-rw-r--r--src/parser/cvc/cvc.h51
-rw-r--r--src/parser/cvc/cvc_input.cpp77
-rw-r--r--src/parser/cvc/cvc_input.h79
-rw-r--r--src/parser/parser_builder.cpp10
-rw-r--r--src/parser/smt2/smt2.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.cpp1558
-rw-r--r--src/printer/cvc/cvc_printer.h208
-rw-r--r--src/printer/printer.cpp4
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback