Age | Commit message (Expand) | Author |
2011-03-05 | - Made Rational::sgn() function const. | Tim King |
2011-03-03 | fix for bug #244, "Segfault if file cannot be found and --stats is on" | Morgan Deters |
2011-03-03 | resurrecting triple.h from r1023 (after which it was removed) | Morgan Deters |
2011-02-28 | CongruenceClosure module now should support nullary congruence operators (now... | Morgan Deters |
2011-02-28 | Review of statistics code. Added lots of documentation, and fixed an issue (... | Morgan Deters |
2011-02-27 | - Adds a path for Theory to be passed a reference to Options. | Tim King |
2011-02-26 | Commit to fix bug 241 (improper "using namespace std" in a header). This cau... | Morgan Deters |
2010-12-16 | minor fixes for correct doxygen output | Morgan Deters |
2010-12-14 | make some CC module methods private that should not have been public | Morgan Deters |
2010-12-14 | congruence closure module now supports things other than APPLY_UF; ported fro... | Morgan Deters |
2010-11-19 | Merge from ufprop branch, including: | Morgan Deters |
2010-11-19 | add statistics support information to --show-config | Morgan Deters |
2010-11-17 | add some stats to UF/CC | Morgan Deters |
2010-11-17 | The "UF engineering issues" release, after much profiling. | Morgan Deters |
2010-11-15 | Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer | Morgan Deters |
2010-11-09 | Lemmas on demand work, push-pop, some cleanup. | Dejan Jovanović |
2010-11-08 | command-line flag to disable theory registration, also SMT-LIBv2 compliance (... | Morgan Deters |
2010-11-08 | cleanup, documentation, SMT-LIBv2 compliance | Morgan Deters |
2010-11-05 | Moving Options fiddling to options.h | Christopher L. Conway |
2010-11-03 | Adds AverageStat to stats.h. | Tim King |
2010-10-31 | enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d... | Morgan Deters |
2010-10-24 | add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like pri... | Morgan Deters |
2010-10-22 | removing unused functionality from util; related to bug #222 | Morgan Deters |
2010-10-22 | Using Options in ParserBuilder and InteractiveShell | Christopher L. Conway |
2010-10-22 | Merging main/getopt.cpp, main/usage.h, and smt/options.h in | Christopher L. Conway |
2010-10-20 | fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug... | Morgan Deters |
2010-10-12 | Merge from cc-memout branch. Here are the main points | Morgan Deters |
2010-10-12 | check last result in (get-assignment); some context cleanup | Morgan Deters |
2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp... | Morgan Deters |
2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ... | Morgan Deters |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
2010-10-08 | * (define-fun...) now has proper type checking in non-debug builds | Morgan Deters |
2010-10-07 | type checking for define-fun in production builds; related to (and might reso... | Morgan Deters |
2010-10-07 | SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre... | Morgan Deters |
2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ... | Morgan Deters |
2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti... | Morgan Deters |
2010-10-04 | fixing CLN builds, which had broken the build tonight; will re-run regression... | Morgan Deters |
2010-10-04 | remove/shuffle some #include dependencies; fix some documentation; apply codi... | Morgan Deters |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-10-01 | replacement implementation for clock_gettime() on mac os x, build portability... | Morgan Deters |
2010-09-30 | fixed a number of problems with mac os x builds. build now works on mac os x... | Morgan Deters |
2010-09-28 | fix TLS support for platforms (e.g. Mac OS X) where __thread storage class do... | Morgan Deters |
2010-09-27 | add workaround for systems (i.e., Mac OS X) that don't support __thread; also... | ACSYS |
2010-09-27 | - This update adds DynamicArray<T>. This is a bare bones heap allocated arra... | Tim King |
2010-09-20 | bitvector rewriting for the core theory and testcases | Dejan Jovanović |
2010-09-14 | ensure uf/congruence closure debugging stuff isn't called in production builds | Morgan Deters |
2010-09-02 | fix an error in TimerStat | Morgan Deters |
2010-09-02 | * add TimerStat statistic type | Morgan Deters |
2010-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters |
2010-08-18 | more tests, configuration for UF | Morgan Deters |