summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-12-14permit PARAMETERIZED operators to be zero-aryMorgan Deters
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan Deters
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-29minor fixes as a result of review of Chris's getType() rewrite; also fix some...Morgan Deters
2010-10-28Changing NodeBuilder::debugCheckType() to maybeCheckType()Christopher L. Conway
2010-10-28Disabling bottom-up algorithm in NodeManager::getType() when type checkingChristopher L. Conway
2010-10-27Small change to documentation in NodeManager::getTypeChristopher L. Conway
2010-10-27Slightly more efficient version of getTypeChristopher L. Conway
2010-10-27Modifying getType to use a non-recursive algorithm (Fixes: #228)Christopher L. Conway
2010-10-26GetValueCommand now gives a TUPLE as output, with the first operand the input...Morgan Deters
2010-10-25missing case in expr output; resolves bug 226Morgan Deters
2010-10-24add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like pri...Morgan Deters
2010-10-22comment out the "interactive" check in SmtEngine::getValue() for now (resolve...Morgan Deters
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-12IDENTITY has been removed.Tim King
2010-10-12fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTyp...Morgan Deters
2010-10-12fix some leaks in parser, add debug code to node manager to find moreMorgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-11use "forward" headersMorgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-09support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ...Morgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-10-07type checking for define-fun in production builds; related to (and might reso...Morgan Deters
2010-10-07NodeSelfIterator implementation and unit test (resolves bug #204); also fix P...Morgan Deters
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre...Morgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
2010-10-04re-add a dependency to fix compile warningsMorgan Deters
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply codi...Morgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-10-02revert a workaround fix to CDMap that was committed as part of the arith-inde...Morgan Deters
2010-09-28node iterator workMorgan Deters
2010-09-28fix TLS support for platforms (e.g. Mac OS X) where __thread storage class do...Morgan Deters
2010-09-27add workaround for systems (i.e., Mac OS X) that don't support __thread; also...ACSYS
2010-09-24Fix build system for Mac OS X builds (resolves bug #203)Morgan Deters
2010-09-21Rm'ing automatic type check in NodeBuilder for vars/constantsChristopher L. Conway
2010-09-21remove assertion in TNode destructor and ensure all TNode methods check rc > ...Morgan Deters
2010-09-21some code cleanup, documentation, review of "kinded-iterator" code, and addit...Morgan Deters
2010-09-21iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wantsDejan Jovanović
2010-09-21Moving automatic type check to NodeBuilder (Fixes: #199)Christopher L. Conway
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-09-13make Node iterators more STL-friendly, resolves bug #196Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
2010-09-02"Leftist NodeBuilders" are now supported.Morgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback