summaryrefslogtreecommitdiff
path: root/src/theory/builtin/Makefile
AgeCommit message (Collapse)Author
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
* added TheoryArith::preRewrite() to test and demonstrate the use of pre-rewriting. * array types and type checking now supported * array type checking now supported * theoryOf() dispatching properly to arrays now * theories now required to implement a (simple) identify() function that returns a string identifying them for debugging/user output purposes * added "builtin" theory to hold all built-in kinds and their type rules and rewriting (currently only exploding distinct) * fixed production build failure (regarding NodeSetDepth) * removed an errant "using namespace std" in util/bitvector.h (and made associated trivial fixes elsewhere) * fixes to make unexpected exceptions more verbose in debug builds * fixes to make multiple, cascading assertion fails simpler * minor other fixes to comments etc.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback