git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 6 Nov 2020 04:28:18 +0000 (22:28 -0600)
committer	GitHub <noreply@github.com>
	Fri, 6 Nov 2020 04:28:18 +0000 (22:28 -0600)
commit	af18cd275f340d1896c3b635dbeecbea2e521db1
tree	438137ddb999a853b543baa70e8009da212c1e05	tree
parent	ac8b2593bed81125cb1a494e4b8311e517d0e3d9	commit \| diff

Simplify printing with respect to expression types (#5394)

This removes infrastructure for stream property related to printing type annotations on all variables.

This is towards refactoring the printers.

27 files changed:

src/expr/expr_iomanip.cpp		diff \| blob \| history
src/expr/expr_iomanip.h		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		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/options/expr_options.toml		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.h		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.h		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/options_manager.cpp		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
test/unit/expr/node_black.h		diff \| blob \| history

RSS Atom