| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw |
| 2012-02-29 |
Liana Hadarean | This should fix the debian build fails: |
blob | commitdiff | raw | diff to current |
| 2012-02-29 |
Morgan Deters | consistency in how the Dump output stream is used |
blob | commitdiff | raw | diff to current |
| 2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
blob | commitdiff | raw | diff to current |
| 2012-02-20 |
Morgan Deters | fix sharing issue for portfolio (full lit-to-node map... |
blob | commitdiff | raw | diff to current |
| 2012-02-20 |
Morgan Deters | portfolio merge |
blob | commitdiff | raw | diff to current |
| 2011-11-15 |
Morgan Deters | Bindings work (ocaml bindings are now sort of working... |
blob | commitdiff | raw | diff to current |
| 2011-10-05 |
Morgan Deters | ensureLiteral() in CNF stream to support Andy's quantif... |
blob | commitdiff | raw | diff to current |
| 2011-09-30 |
Morgan Deters | fix to CNF undoTranslate(), to support incrementality |
blob | commitdiff | raw | diff to current |
| 2011-09-30 |
Morgan Deters | fixes to incremental simplification, cnf routines,... |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Dejan Jovanović | * Changing pre-registration to be context dependent... |
blob | commitdiff | raw | diff to current |
| 2011-08-17 |
Dejan Jovanović | new implementation of lemmas on demand |
blob | commitdiff | raw | diff to current |
| 2011-07-07 |
Dejan Jovanović | removing duplicate clauses in ite cnf conversion |
blob | commitdiff | raw | diff to current |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw | diff to current |
| 2011-04-10 |
Morgan Deters | merge from replay 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-02 |
Morgan Deters | minor fixes |
blob | commitdiff | raw | diff to current |
| 2011-04-01 |
Morgan Deters | minor bugfixes (fixes broken dynamic-library build... |
blob | commitdiff | raw | diff to current |
| 2011-03-21 |
Dejan Jovanović | more bugfixes, some basic propagation, and testcases... |
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-10-31 |
Morgan Deters | enable dependence graphs in doxygen; fix lots of doxyge... |
blob | commitdiff | raw | diff to current |
| 2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
blob | commitdiff | raw | diff to current |
| 2010-08-19 |
Morgan Deters | UF theory bug fixes, code cleanup, and extra debugging... |
blob | commitdiff | raw | diff to current |
| 2010-08-16 |
Dejan Jovanović | Fixing failures in minisat |
blob | commitdiff | raw | diff to current |
| 2010-08-15 |
Dejan Jovanović | (no commit message) |
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-06-29 |
Tim King | Merging the unate-propagator branch into the 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-06-01 |
Dejan Jovanović | In order for splitting on demand to be able to retract... |
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 |
Morgan Deters | Remove isAtomic() as per 4/27/2010 meeting. Add commen... |
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-21 |
Tim King | Small fixes to TheoryArith. Added a hack to make Integ... |
blob | commitdiff | raw | diff to current |
| 2010-05-14 |
Christopher L. Conway | Adding debugging code in PropEngine/CnfStream |
blob | commitdiff | raw | diff to current |
| 2010-05-14 |
Christopher L. Conway | Adding rudimentary ITE handling in CnfStream |
blob | commitdiff | raw | diff to current |
| 2010-05-14 |
Christopher L. Conway | Virtualizing interface between CnfStream and SatSolver |
blob | commitdiff | raw | diff to current |
| 2010-05-13 |
Christopher L. Conway | Minor refactorings and corrections to comments |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | PARSER STUFF: |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Dejan Jovanović | Changing const TNode& to TNode in the CNF conversion... |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Dejan Jovanović | Boolean variables were marked as theory literals by... |
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-03-05 |
Morgan Deters | * public/private code untangled (smt/smt_engine.h no... |
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-22 |
Dejan Jovanović | Merging from branch branches/Liana r241 |
blob | commitdiff | raw | diff to current |
| 2010-02-13 |
Dejan Jovanović | Improvements to CNF conversion when already in CNF |
blob | commitdiff | raw | diff to current |
| 2010-02-09 |
Dejan Jovanović | Changes to the CNF conversion and the SAT solver. All... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Dejan Jovanović | beautification of the prop engine |
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 |
Tim King | Changed mapping from atoms to literals in the prop... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | minor fix for update-copyright.pl; ran update-copyright... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Tim King | Fixes to the cnf converter. Also a barebones utility... |
blob | commitdiff | raw | diff to current |
| 2010-02-02 |
Dejan Jovanović | (no commit message) |
blob | commitdiff | raw | diff to current |
| 2010-02-02 |
Dejan Jovanović | for tim |
blob | commitdiff | raw | diff to current |
| 2010-02-02 |
Tim King | Switched cnf conversion to go through CnfStream. |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history