projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 78d29da) | patch
Consolidate language types (#7065)
authorGereon Kremer <nafur42@gmail.com>
Thu, 26 Aug 2021 00:19:41 +0000 (17:19 -0700)
committerGitHub <noreply@github.com>
Thu, 26 Aug 2021 00:19:41 +0000 (00:19 +0000)
commit71f025753f734ddade5da333dfe2d144fbc13221
tree271e0a03b5612652d5fdb040fa2d7f43e8644aeatree
parent78d29da02099762374adeb694ed96c496c7e1ffccommit | diff
Consolidate language types (#7065)

This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
53 files changed:
src/expr/dtype.cpp diff | blob | history
src/expr/dtype_cons.cpp diff | blob | history
src/expr/dtype_selector.cpp diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_value.cpp diff | blob | history
src/expr/node_value.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/main/driver_unified.cpp diff | blob | history
src/main/interactive_shell.cpp diff | blob | history
src/main/main.cpp diff | blob | history
src/options/base_options.toml diff | blob | history
src/options/language.cpp diff | blob | history
src/options/language.h diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/options/options_handler.h diff | blob | history
src/options/set_language.cpp diff | blob | history
src/options/set_language.h diff | blob | history
src/parser/antlr_input.cpp diff | blob | history
src/parser/antlr_input.h diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/input.cpp diff | blob | history
src/parser/input.h diff | blob | history
src/parser/parser.cpp diff | blob | history
src/parser/parser_builder.cpp diff | blob | history
src/parser/parser_builder.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/printer.cpp diff | blob | history
src/printer/printer.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/tptp/tptp_printer.cpp diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/command.h diff | blob | history
src/smt/node_command.cpp diff | blob | history
src/smt/node_command.h diff | blob | history
src/smt/optimization_solver.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_verify.cpp diff | blob | history
src/util/result.cpp diff | blob | history
src/util/result.h diff | blob | history
test/api/ouroborous.cpp diff | blob | history
test/api/smt2_compliance.cpp diff | blob | history
test/regress/regress0/lang_opts_2_6_1.smt2 diff | blob | history
test/regress/regress0/options/set-and-get-options.smt2 diff | blob | history
test/unit/node/node_black.cpp diff | blob | history
test/unit/parser/parser_black.cpp diff | blob | history
test/unit/parser/parser_builder_black.cpp diff | blob | history
test/unit/printer/smt2_printer_black.cpp diff | blob | history
test/unit/util/boolean_simplification_black.cpp diff | blob | history