projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec4e1bd) | patch
Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
authorMorgan Deters <mdeters@gmail.com>
Mon, 15 Nov 2010 22:57:14 +0000 (22:57 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 15 Nov 2010 22:57:14 +0000 (22:57 +0000)
commit5e5956d492ab18b5b4d4bb51117ac760867a525d
tree0c151baa58810722288ad986dfa13123de273739tree
parentec4e1bdba56565d6372cb19ded12c9cadc506870commit | diff
Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)
26 files changed:
config/mkbuilddir diff | blob | history
src/Makefile.am diff | blob | history
src/expr/expr_template.h diff | blob | history
src/expr/metakind_template.h diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_builder.h diff | blob | history
src/expr/node_value.cpp diff | blob | history
src/printer/Makefile [new file with mode: 0644] blob
src/printer/Makefile.am [new file with mode: 0644] blob
src/printer/ast/ast_printer.cpp [new file with mode: 0644] blob
src/printer/ast/ast_printer.h [new file with mode: 0644] blob
src/printer/cvc/cvc_printer.cpp [new file with mode: 0644] blob
src/printer/cvc/cvc_printer.h [new file with mode: 0644] blob
src/printer/printer.cpp [new file with mode: 0644] blob
src/printer/printer.h [new file with mode: 0644] blob
src/printer/smt/smt_printer.cpp [new file with mode: 0644] blob
src/printer/smt/smt_printer.h [new file with mode: 0644] blob
src/printer/smt2/smt2_printer.cpp [new file with mode: 0644] blob
src/printer/smt2/smt2_printer.h [new file with mode: 0644] blob
src/theory/bv/theory_bv_rewrite_rules.cpp diff | blob | history
src/util/bitvector.h diff | blob | history
src/util/integer_cln_imp.h diff | blob | history
src/util/integer_gmp_imp.h diff | blob | history
src/util/language.h diff | blob | history
test/unit/expr/node_builder_black.h diff | blob | history
test/unit/util/integer_black.h diff | blob | history