| 2010-11-16 |
Tim King | Added Theory::presolve(). |
commit | commitdiff | tree |
| 2010-11-16 |
Morgan Deters | SmtEngine now fails with a ModalException if --incremen... |
commit | commitdiff | tree |
| 2010-11-16 |
Morgan Deters | fix function signatures |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | cleanup from today's commits: delegate as-yet-unimpleme... |
commit | commitdiff | tree |
| 2010-11-15 |
Tim King | Changes to Solver and PropEngine to support lemmasOnDem... |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | Pretty-printer infrastructure created (in src/printer... |
commit | commitdiff | tree |
| 2010-11-15 |
Tim King | This commit merges the arith-prop-opt branch into the... |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | minor tweaks to last commit, testing infrastructure |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | fix some things with the build system (make dist, make... |
commit | commitdiff | tree |
| 2010-11-12 |
Dejan Jovanović | Some bug fixes in the SAT for lemmas, and an experiment... |
commit | commitdiff | tree |
| 2010-11-11 |
Morgan Deters | make addsourcedir executable |
commit | commitdiff | tree |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | command-line flag to disable theory registration, also... |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | cleanup, documentation, SMT-LIBv2 compliance |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | fix out-of-date version/copyright for minisats |
commit | commitdiff | tree |
| 2010-11-05 |
Christopher... | Moving Options fiddling to options.h |
commit | commitdiff | tree |
| 2010-11-04 |
Morgan Deters | competition mode implies --no-checking |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | Moving the post_mortem.py script out of contrib and... |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | Updates post_mortem.py script to be able to handle... |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | This commit adds the ejected and un-ejected statistics. |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds size() to RowVector. |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds statistics for the number of Uservariables and... |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds AverageStat to stats.h. |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | small fix to debug segfaults |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | enable dependence graphs in doxygen; fix lots of doxyge... |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | maximize stack limit, handle SEGV signals on an alterna... |
commit | commitdiff | tree |
| 2010-10-30 |
Tim King | Adds a hueristic from Alberto's thesis. For a fixed... |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Fix for a problem caused by using a != instead of ... |
commit | commitdiff | tree |
| 2010-10-29 |
Morgan Deters | portability updates to build system |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Adds a very small test that triggers a bug. The bug... |
commit | commitdiff | tree |
| 2010-10-29 |
Morgan Deters | minor fixes as a result of review of Chris's getType... |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Fixes RowVector::has(). |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Factors out the QF_LRA decision procedure from TheoryAr... |
commit | commitdiff | tree |
| 2010-10-28 |
Tim King | The Row implementation has no been replaced by RowVecto... |
commit | commitdiff | tree |
| 2010-10-28 |
Christopher... | Changing NodeBuilder::debugCheckType() to maybeCheckType() |
commit | commitdiff | tree |
| 2010-10-28 |
Christopher... | Disabling bottom-up algorithm in NodeManager::getType... |
commit | commitdiff | tree |
| 2010-10-28 |
Morgan Deters | fix confusing CXXTEST configure message, indicating... |
commit | commitdiff | tree |
| 2010-10-27 |
Christopher... | Small change to documentation in NodeManager::getType |
commit | commitdiff | tree |
| 2010-10-27 |
Christopher... | Slightly more efficient version of getType |
commit | commitdiff | tree |
| 2010-10-27 |
Morgan Deters | make dist-building more pleasant (put .tar.gz in builds... |
commit | commitdiff | tree |
| 2010-10-27 |
Christopher... | Changing dependency info in README |
commit | commitdiff | tree |
| 2010-10-27 |
Christopher... | Modifying getType to use a non-recursive algorithm... |
commit | commitdiff | tree |
| 2010-10-27 |
Morgan Deters | fix test Makefile |
commit | commitdiff | tree |
| 2010-10-27 |
Morgan Deters | "make dist" fixes; a distribution tarball can now build... |
commit | commitdiff | tree |
| 2010-10-27 |
Morgan Deters | support focus on a particular subpackage (e.g. "expr") |
commit | commitdiff | tree |
| 2010-10-27 |
Morgan Deters | inter-package dependence graph generation (in dot format) |
commit | commitdiff | tree |
| 2010-10-26 |
Morgan Deters | GetValueCommand now gives a TUPLE as output, with the... |
commit | commitdiff | tree |
| 2010-10-26 |
Christopher... | Cleaning up some header files |
commit | commitdiff | tree |
| 2010-10-26 |
Christopher... | Adding dependency info to README |
commit | commitdiff | tree |
| 2010-10-25 |
Morgan Deters | for static linking of driver binary, list libmain.a... |
commit | commitdiff | tree |
| 2010-10-25 |
Morgan Deters | missing case in expr output; resolves bug 226 |
commit | commitdiff | tree |
| 2010-10-24 |
Christopher... | Adding unit test for InteractiveShell |
commit | commitdiff | tree |
| 2010-10-24 |
Morgan Deters | add a CVC4_UNDEFINED keyword, for intentionally undefin... |
commit | commitdiff | tree |
| 2010-10-23 |
Tim King | Removed slack.h, and arith_activity.h. Replaced IsBasic... |
commit | commitdiff | tree |
| 2010-10-23 |
Christopher... | Adding Parser::setInput and using it in InteractiveShel... |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | removing unused functionality from util; related to... |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | fix valgrind-reported errors in parser builder; a non... |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Saving state between lines in interactive mode (Fixes... |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Using Options in ParserBuilder and InteractiveShell |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Merging main/getopt.cpp, main/usage.h, and smt/options... |
commit | commitdiff | tree |
| 2010-10-22 |
Tim King | Code cleanup for TheoryArith. |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | comment out the "interactive" check in SmtEngine::getVa... |
commit | commitdiff | tree |
| 2010-10-22 |
Tim King | Fixes to getValue for TheoryArith. |
commit | commitdiff | tree |
| 2010-10-21 |
Christopher... | * Option --no-type-checking now disables type checks... |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Changing --no-early-type-checking to --no-type-checking |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Enabling semantic checks in ParserBuilder |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Adding detection of TTY vs. piped input for interactive... |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Fixing minor whitespace bug in the parser |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Adding support for interactive mode |
commit | commitdiff | tree |
| 2010-10-20 |
Morgan Deters | fix bug #220 (assertion fails if no query/check-sat... |
commit | commitdiff | tree |
| 2010-10-14 |
Tim King | Fixed computation of infinitesimals for arithmetic... |
commit | commitdiff | tree |
| 2010-10-13 |
Tim King | Removed vector<Monomial> monos from Polynomial. Now... |
commit | commitdiff | tree |
| 2010-10-13 |
Tim King | Added test/regress/regress1/arith and populated it... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | with --stats, statistics are dumped for memouts and... |
commit | commitdiff | tree |
| 2010-10-12 |
Tim King | IDENTITY has been removed. |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | minor unit test fix-ups |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | fix debugPrintNode(), debugPrintTNode(), debugPrintNode... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | fix some leaks in parser, add debug code to node manage... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | hooked up "we are incomplete" flag after conversation... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | Merge from cc-memout branch. Here are the main points |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | check last result in (get-assignment); some context... |
commit | commitdiff | tree |
| 2010-10-11 |
Morgan Deters | use "forward" headers |
commit | commitdiff | tree |
| 2010-10-10 |
Morgan Deters | additional model gen and SMT-LIBv2 compliance work... |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | reverting some changes to parser from last commit |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | support for SMT-LIBv2 :named attributes, and attributes... |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | fix to unit tests |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | bug fixes to model gen |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
commit | commitdiff | tree |
| 2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
commit | commitdiff | tree |
| 2010-10-08 |
Morgan Deters | support (set-info) on status, source, category, difficu... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | oops, reverting a change to a regression test that... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | NodeSelfIterator implementation and unit test (resolves... |
commit | commitdiff | tree |
| 2010-10-07 |
Tim King | Small tableau optimization. |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
commit | commitdiff | tree |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
commit | commitdiff | tree |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fix gdb issues (at least for static builds); resolves... |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fix regular expressions in build system |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fixing CLN builds, which had broken the build tonight... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog