| 2011-04-18 |
Tim King | This commit merges the branch arithmetic/propagation... |
blob | commitdiff | raw |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
| 2011-04-05 |
Morgan Deters | Minor adjustments to the Registrar commit in 1644,... |
blob | commitdiff | raw | diff to current |
| 2011-04-04 |
Tim King | Merging the satliteral-before-prereg branch into trunk... |
blob | commitdiff | raw | diff to current |
| 2011-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
blob | commitdiff | raw | diff to current |
| 2011-03-30 |
Morgan Deters | Add Valuation::getSatValue() so that theories can acces... |
blob | commitdiff | raw | diff to current |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
| 2011-03-17 |
Tim King | Adds debugging output to EngineOutputChannel::lemma. |
blob | commitdiff | raw | diff to current |
| 2011-03-08 |
Morgan Deters | Clean up Theory base class as per code review bug ... |
blob | commitdiff | raw | diff to current |
| 2011-02-27 |
Tim King | - Adds a path for Theory to be passed a reference to... |
blob | commitdiff | raw | diff to current |
| 2011-02-26 |
Morgan Deters | Merge from theory-break-dependences branch to break... |
blob | commitdiff | raw | diff to current |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-11-19 |
Morgan Deters | Merge from ufprop branch, including: |
blob | commitdiff | raw | diff to current |
| 2010-11-16 |
Tim King | Added Theory::presolve(). |
blob | commitdiff | raw | diff to current |
| 2010-11-15 |
Tim King | Changes to Solver and PropEngine to support lemmasOnDem... |
blob | commitdiff | raw | diff to current |
| 2010-11-15 |
Tim King | This commit merges the arith-prop-opt branch into the... |
blob | commitdiff | raw | diff to current |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
blob | commitdiff | raw | diff to current |
| 2010-11-08 |
Morgan Deters | command-line flag to disable theory registration, also... |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Christopher L. Conway | Merging main/getopt.cpp, main/usage.h, and smt/options... |
blob | commitdiff | raw | diff to current |
| 2010-10-21 |
Christopher L. Conway | * Option --no-type-checking now disables type checks... |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | hooked up "we are incomplete" flag after conversation... |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | Merge from cc-memout branch. Here are the main points |
blob | commitdiff | raw | diff to current |
| 2010-10-10 |
Morgan Deters | additional model gen and SMT-LIBv2 compliance work... |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
blob | commitdiff | raw | diff to current |
| 2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
blob | commitdiff | raw | diff to current |
| 2010-09-24 |
Dejan Jovanović | basic union find for bitvectors |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Change TheoryEngine to use pointers to theories instead of |
blob | commitdiff | raw | diff to current |
| 2010-07-22 |
Morgan Deters | incorporate a fix from smtcomp2010 version for handling... |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Clark Barrett | Moved registration to theory engine |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Morgan Deters | Fixes for doubled-statistics (bug 171), a fix to muzzle... |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | enable arrays |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | With "-d extra-checking", rewrites are now checked... |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | re-generated comment headers of source files |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | * Added white-box TheoryEngine test that tests the... |
blob | commitdiff | raw | diff to current |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
| 2010-06-29 |
Tim King | Merging the unate-propagator branch into the trunk... |
blob | commitdiff | raw | diff to current |
| 2010-06-24 |
Tim King | Added post_mortem.py a statistics collector for user... |
blob | commitdiff | raw | diff to current |
| 2010-06-18 |
Tim King | Merging the statistics branch into the main trunk.... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-05-28 |
Tim King | A few changes to the organization of TheoryEngine rewri... |
blob | commitdiff | raw | diff to current |
| 2010-05-28 |
Tim King | Moving the ITE removal from CnfStream to TheoryEngine... |
blob | commitdiff | raw | diff to current |
| 2010-05-27 |
Tim King | Preregistration has been turned on. Highly experimental... |
blob | commitdiff | raw | diff to current |
| 2010-05-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand. |
blob | commitdiff | raw | diff to current |
| 2010-05-20 |
Tim King | Added the division symbol to the parser, and minimal... |
blob | commitdiff | raw | diff to current |
| 2010-05-19 |
Tim King | Significant revision to theory/arith. The new draft... |
blob | commitdiff | raw | diff to current |
| 2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive |
blob | commitdiff | raw | diff to current |
| 2010-04-13 |
Christopher L. Conway | Doxygen fixes |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | PARSER STUFF: |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Morgan Deters | Highlights of this commit are: |
blob | commitdiff | raw | diff to current |
| 2010-03-15 |
Morgan Deters | This checkin resolves bug #57. |
blob | commitdiff | raw | diff to current |
| 2010-03-12 |
Dejan Jovanović | Fixing unnecessary construction of NOT nodes when... |
blob | commitdiff | raw | diff to current |
| 2010-03-12 |
Morgan Deters | * Added shutdown() functions to SmtEngine, TheoryEngine... |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Morgan Deters | naive rewriting to fix minisat invariant; rewrite ... |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Dejan Jovanović | Fix for the main bug that was bugging me -- Bug 49... |
blob | commitdiff | raw | diff to current |
| 2010-03-08 |
Dejan Jovanović | adding simple-uf to the regressions, and the code that... |
blob | commitdiff | raw | diff to current |
| 2010-03-08 |
Dejan Jovanović | some more sat stuff for tim: assertions now go to theory_uf |
blob | commitdiff | raw | diff to current |
| 2010-02-26 |
Morgan Deters | * test/unit/context/context_black.h: Test CDList<>... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Morgan Deters | * src/expr/node.h: add a copy constructor. Apparently... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | minor interface changes to TheoryEngine/Theory after... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | remove -*- c++ -*- emacs tag from source files (it... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | Added theory output channel interfaces and "Interrupted... |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | update-copyright.pl now retrieves and incorporates... |
blob | commitdiff | raw | diff to current |
| 2009-12-08 |
Morgan Deters | work on propositional layer, expression builder support... |
blob | commitdiff | raw | diff to current |
| 2009-11-19 |
Morgan Deters | testing framework, configure fixes, incorporations... |
blob | commitdiff | raw | diff to current |
| 2009-11-17 |
Morgan Deters | from meeting |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history