summaryrefslogtreecommitdiff
path: root/src/theory/arith/tableau.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-07-02 00:09:52 +0000
committerMorgan Deters <mdeters@gmail.com>2010-07-02 00:09:52 +0000
commit83a143b1dd78e5d7f07666fbec1362dd60348116 (patch)
tree08400222d94f4760c7155fea787ac7e78b7b0dfc /src/theory/arith/tableau.h
parenta8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff)
* 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
Diffstat (limited to 'src/theory/arith/tableau.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback