summaryrefslogtreecommitdiff
path: root/src/util/configuration_private.h
AgeCommit message (Collapse)Author
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
(resolves bug #212) * also closed some other type checking loopholes in SmtEngine * small fixes to define-sort (resolves bug #214) * infrastructural support for printing expressions in languages other than the internal representation language using an IO manipulator, e.g.: cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr; main() sets the output language for all streams to correspond to the input language * support delaying type checking in debug builds, so that one can debug the type checker itself (before it was difficult, because debug builds did all the type checking on Node creation!): new command-line flag --no-early-type-checking (only makes sense for debug builds) * disallowed copy-construction of ExprManager and NodeManager, and made other constructors explicit; previously it was easy to unintentionally create duplicate managers, with really weird results (i.e., disappearing attributes!)
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply ↵Morgan Deters
coding standards
2010-10-03file header documentation regenerated with contributors names; no code ↵Morgan Deters
modified in this commit
2010-09-27add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵ACSYS
also configure script auto-detection of __thread support and syntax
2010-07-29Adding configuration_private.h to allow inlining of configuration checksChristopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback