| 2011-02-17 |
Tim King | Updates based on the group code review of arithmetic... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Deleting depricated files. |
commit | commitdiff | tree |
| 2011-02-17 |
Dejan Jovanović | getting ready for slicing bitvectors |
commit | commitdiff | tree |
| 2011-02-16 |
Tim King | Overview of the changes: |
commit | commitdiff | tree |
| 2011-02-16 |
Dejan Jovanović | updates for the rewriter, added some statistics |
commit | commitdiff | tree |
| 2011-02-14 |
Tim King | Reverses the order of the d_possiblyInconsistent queue... |
commit | commitdiff | tree |
| 2011-02-13 |
Tim King | 3 heuristics were added to arithmetic. A heuristic... |
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | fix for build errors |
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
commit | commitdiff | tree |
| 2010-12-17 |
Morgan Deters | tls.h, rational.h, and integer.h are only re-generated... |
commit | commitdiff | tree |
| 2010-12-16 |
Morgan Deters | minor fixes for correct doxygen output |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | make some CC module methods private that should not... |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | congruence closure module now supports things other... |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | permit PARAMETERIZED operators to be zero-ary |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | fix to static learning application in UF, resolves... |
commit | commitdiff | tree |
| 2010-11-24 |
Dejan Jovanović | Changin the get() semantics to a CDQeue-sque semantics. |
commit | commitdiff | tree |
| 2010-11-19 |
Morgan Deters | Merge from ufprop branch, including: |
commit | commitdiff | tree |
| 2010-11-19 |
Morgan Deters | add statistics support information to --show-config |
commit | commitdiff | tree |
| 2010-11-18 |
Morgan Deters | small changes to documentation; also, '\''make doc... |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | fix improper CongruenceClosureWhite test by merging... |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | add some stats to UF/CC |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | The "UF engineering issues" release, after much profiling. |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog