Age | Commit message (Expand) | Author |
2010-10-22 | Code cleanup for TheoryArith. | Tim King |
2010-10-22 | comment out the "interactive" check in SmtEngine::getValue() for now (resolve... | Morgan Deters |
2010-10-22 | Fixes to getValue for TheoryArith. | Tim King |
2010-10-21 | * Option --no-type-checking now disables type checks in SmtEngine | Christopher L. Conway |
2010-10-20 | Changing --no-early-type-checking to --no-type-checking | Christopher L. Conway |
2010-10-20 | Enabling semantic checks in ParserBuilder | Christopher L. Conway |
2010-10-20 | Adding detection of TTY vs. piped input for interactive mode | Christopher L. Conway |
2010-10-20 | Fixing minor whitespace bug in the parser | Christopher L. Conway |
2010-10-20 | Adding support for interactive mode | 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-14 | Fixed computation of infinitesimals for arithmetic model generation. | Tim King |
2010-10-13 | Removed vector<Monomial> monos from Polynomial. Now using expr::NodeSelfIter... | Tim King |
2010-10-13 | Added test/regress/regress1/arith and populated it with some fast SMT LIB pro... | Tim King |
2010-10-12 | with --stats, statistics are dumped for memouts and (normal) exceptions. | Morgan Deters |
2010-10-12 | IDENTITY has been removed. | Tim King |
2010-10-12 | minor unit test fix-ups | Morgan Deters |
2010-10-12 | fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTyp... | Morgan Deters |
2010-10-12 | fix some leaks in parser, add debug code to node manager to find more | Morgan Deters |
2010-10-12 | hooked up "we are incomplete" flag after conversation with Tim (a theory noti... | 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-11 | use "forward" headers | Morgan Deters |
2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp... | Morgan Deters |
2010-10-09 | reverting some changes to parser from last commit | Morgan Deters |
2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ... | Morgan Deters |
2010-10-09 | fix to unit tests | Morgan Deters |
2010-10-09 | bug fixes to model gen | 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-08 | support (set-info) on status, source, category, difficulty, smt-lib-version, ... | Morgan Deters |
2010-10-07 | oops, reverting a change to a regression test that had intentionally caused a... | Morgan Deters |
2010-10-07 | type checking for define-fun in production builds; related to (and might reso... | Morgan Deters |
2010-10-07 | NodeSelfIterator implementation and unit test (resolves bug #204); also fix P... | Morgan Deters |
2010-10-07 | Small tableau optimization. | Tim King |
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 | fix gdb issues (at least for static builds); resolves bug 194 | Morgan Deters |
2010-10-04 | fix regular expressions in build system | Morgan Deters |
2010-10-04 | fixing CLN builds, which had broken the build tonight; will re-run regression... | Morgan Deters |
2010-10-04 | re-add a dependency to fix compile warnings | Morgan Deters |
2010-10-04 | remove/shuffle some #include dependencies; fix some documentation; apply codi... | Morgan Deters |
2010-10-04 | Fix to bug 211. ArithVar is now typedefed to uint32_t. | Tim King |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-10-02 | revert a workaround fix to CDMap that was committed as part of the arith-inde... | Morgan Deters |
2010-10-02 | dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout... | Morgan Deters |
2010-10-02 | branches/arith-indexed-variables merged into the main trunk. | Tim King |
2010-10-01 | re-add no-deprecated to C sources; update some file-level documentation; firs... | Morgan Deters |
2010-10-01 | last update broke the parser inadvertently, fixing... | Morgan Deters |
2010-10-01 | replacement implementation for clock_gettime() on mac os x, build portability... | Morgan Deters |