Refactor how options are passed to the printer (#8827)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 1 Jun 2022 03:57:52 +0000 (20:57 -0700)
committerGitHub <noreply@github.com>
Wed, 1 Jun 2022 03:57:52 +0000 (03:57 +0000)
commit735cbadb137362fbc876fd056ed6ba3a9768caf1
treedf2d85457d2924e8d55b3a89b4ff71fb7b663910
parent04ceb6d3a1719e616c0e2bc28cbba89f83865f8f
Refactor how options are passed to the printer (#8827)

Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)
48 files changed:
src/CMakeLists.txt
src/expr/node.h
src/expr/node_value.cpp
src/expr/node_value.h
src/expr/type_node.cpp
src/expr/type_node.h
src/options/base_options.toml
src/options/bv_options.toml
src/options/expr_options.toml
src/options/io_utils.cpp [deleted file]
src/options/io_utils.h [deleted file]
src/options/io_utils_template.cpp [new file with mode: 0644]
src/options/io_utils_template.h [new file with mode: 0644]
src/options/mkoptions.py
src/options/options_handler.cpp
src/options/options_handler.h
src/options/options_public_template.cpp
src/options/printer_options.toml
src/options/proof_options.toml
src/printer/ast/ast_printer.cpp
src/printer/ast/ast_printer.h
src/printer/printer.cpp
src/printer/printer.h
src/printer/smt2/smt2_printer.cpp
src/printer/smt2/smt2_printer.h
src/printer/tptp/tptp_printer.cpp
src/printer/tptp/tptp_printer.h
src/proof/dot/dot_printer.cpp
src/proof/lfsc/lfsc_node_converter.cpp
src/proof/lfsc/lfsc_print_channel.cpp
src/proof/unsat_core.cpp
src/smt/command.cpp
src/smt/command.h
src/smt/env.cpp
src/smt/env.h
src/smt/model.cpp
src/smt/optimization_solver.cpp
src/smt/process_assertions.cpp
src/smt/solver_engine.cpp
src/smt/solver_engine.h
src/theory/quantifiers/instantiation_list.cpp
src/theory/quantifiers/query_generator.cpp
src/theory/quantifiers/term_database.cpp
src/util/result.cpp
test/unit/node/node_black.cpp
test/unit/printer/smt2_printer_black.cpp
test/unit/theory/theory_arith_coverings_white.cpp
test/unit/util/boolean_simplification_black.cpp