Push output language inside the printing code (#7683)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 23 Nov 2021 19:04:46 +0000 (11:04 -0800)
committerGitHub <noreply@github.com>
Tue, 23 Nov 2021 19:04:46 +0000 (19:04 +0000)
commit20e2df18b5427bdc3b59ade5b0711c78b677cef9
tree24de7944d56019f462bf57289370b02d07ac4d7c
parent51f7733bec4ab2c9666173848b81cab8744359da
Push output language inside the printing code (#7683)

This PR pushes the explicit specification of the output language further inside the printing methods.
The general way to specify the output language is to attach it to the output stream. The changes simplify the interface, while we still allow printing in another output language via using a scope (as used in the lfsc and tptp printers).
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/printer/smt2/smt2_printer.cpp
src/printer/tptp/tptp_printer.cpp
src/proof/lfsc/lfsc_node_converter.cpp
src/proof/lfsc/lfsc_print_channel.cpp
src/util/result.cpp
src/util/result.h