* Added white-box TheoryEngine test that tests the rewriter
authorMorgan Deters <mdeters@gmail.com>
Fri, 2 Jul 2010 00:09:52 +0000 (00:09 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 2 Jul 2010 00:09:52 +0000 (00:09 +0000)
commit83a143b1dd78e5d7f07666fbec1362dd60348116
tree08400222d94f4760c7155fea787ac7e78b7b0dfc
parenta8566c313e9b5eb8248eaeea642a9c72c803dcfa
* Added white-box TheoryEngine test that tests the rewriter

* Added regression documentation to test/regress/README

* Added ability to print types of vars in expr printouts
  with iomanipulator Node::printtypes(true)... for example,
    Warning() << Node::printtypes(true) << n << std::endl;

* Types-printing can be specified on the command line with
  --print-expr-types

* Improved type handling facilities and theoryOf().
  For now, SORT_TYPE moved from builtin theory to UF theory
  to match old behavior.

* Additional gdb debug functionality.  Now we have:

    debugPrintNode(Node)            debugPrintRawNode(Node)
    debugPrintTNode(TNode)          debugPrintRawTNode(TNode)
    debugPrintTypeNode(TypeNode)    debugPrintRawTypeNode(TypeNode)
    debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)

  they all print a {Node,TNode,NodeValue*} from the debugger.
  The "Raw" versions print a very low-level AST-like form.
  The regular versions do the same as operator<<, but force
  full printing on (no depth-limiting).

* Other trivial fixes
24 files changed:
contrib/update-copyright.pl
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/node.h
src/expr/node_builder.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/node_value.cpp
src/expr/node_value.h
src/expr/type_node.cpp
src/expr/type_node.h
src/main/getopt.cpp
src/main/usage.h
src/parser/antlr_input_imports.cpp
src/theory/builtin/kinds
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/kinds
src/util/stats.cpp
src/util/stats.h
test/regress/README [new file with mode: 0644]
test/unit/Makefile.am
test/unit/theory/theory_engine_white.h [new file with mode: 0644]