Dagification of output expressions.
authorMorgan Deters <mdeters@gmail.com>
Sat, 9 Jun 2012 00:35:38 +0000 (00:35 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 9 Jun 2012 00:35:38 +0000 (00:35 +0000)
commit700689a4e4ed42b5198816611eac5bcc1278284d
tree0d6029f9bc4f46a721930a27a47ac487771c452e
parenta0411d4baad389ce88d4bd26edc8ed811625887c
Dagification of output expressions.

By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.

If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.
24 files changed:
src/expr/command.cpp
src/expr/command.h
src/expr/expr.i
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/node.h
src/expr/node_value.cpp
src/expr/node_value.h
src/expr/type_node.h
src/printer/Makefile.am
src/printer/ast/ast_printer.cpp
src/printer/ast/ast_printer.h
src/printer/cvc/cvc_printer.cpp
src/printer/cvc/cvc_printer.h
src/printer/dagification_visitor.h [new file with mode: 0644]
src/printer/printer.h
src/printer/smt/smt_printer.cpp
src/printer/smt/smt_printer.h
src/printer/smt2/smt2_printer.cpp
src/printer/smt2/smt2_printer.h
src/theory/substitutions.h
src/util/node_visitor.h
src/util/options.cpp
test/unit/expr/node_black.h