Tuesday end-of-day commit.
authorMorgan Deters <mdeters@gmail.com>
Wed, 20 Apr 2011 05:37:38 +0000 (05:37 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 20 Apr 2011 05:37:38 +0000 (05:37 +0000)
commit12c1e41862e4b12c3953272416a1edc103d299ee
tree9c7d3a044c33ffc3be177e6ca692eb4149add27c
parent08df44e6b61999a14dd24a7a134146694dcb3596
Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
47 files changed:
src/expr/declaration_scope.cpp
src/expr/declaration_scope.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/kind_template.h
src/expr/mkkind
src/expr/node.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/type.cpp
src/expr/type.h
src/expr/type_node.cpp
src/expr/type_node.h
src/parser/antlr_input.h
src/parser/cvc/Cvc.g
src/parser/cvc/cvc_input.h
src/parser/input.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/parser_builder.h
src/parser/smt/Smt.g
src/parser/smt/smt.cpp
src/parser/smt/smt.h
src/parser/smt/smt_input.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.h
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv_type_rules.h
src/theory/theory.h
src/theory/theory_engine.h
src/util/boolean_simplification.h
src/util/datatype.cpp
src/util/datatype.h
src/util/options.cpp
test/regress/regress0/bv/Makefile.am
test/regress/regress0/bv/bvcomp.cvc [new file with mode: 0644]
test/regress/regress0/bv/bvsimple.cvc
test/regress/regress0/error.cvc
test/system/ouroborous.cpp
test/unit/parser/parser_black.h