2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization... |
blob | commitdiff | raw |
2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
blob | commitdiff | raw | diff to current |
2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
blob | commitdiff | raw | diff to current |
2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw | diff to current |
2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
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 |
2011-11-15 |
Morgan Deters | Bindings work (ocaml bindings are now sort of working... |
blob | commitdiff | raw | diff to current |
2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
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-16 |
Morgan Deters | fix numerous documentation issues; doxygen complains... |
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-08-17 |
Dejan Jovanović | new implementation of lemmas on demand |
blob | commitdiff | raw | diff to current |
2011-07-11 |
Clark Barrett | Clark's work on array theory - can now solve all QF_AX... |
blob | commitdiff | raw | diff to current |
2011-07-09 |
Dejan Jovanović | surprize surprize |
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 |
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-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-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-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-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand. |
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-04-01 |
Morgan Deters | PARSER STUFF: |
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-08 |
Dejan Jovanović | some more sat stuff for tim: assertions now go to theory_uf |
blob | commitdiff | raw | diff to current |
2010-03-03 |
Dejan Jovanović | Some SAT stuff, not doing anything special yet, just... |
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-22 |
Morgan Deters | * configure.ac: Remove doc/ from search path for Makefi... |
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-03 |
Morgan Deters | Addressed many of the concerns of bug 10 (build system... |
blob | commitdiff | raw | diff to current |
2010-02-03 |
Tim King | I hacked in a temporary way to restart minisat for... |
blob | commitdiff | raw | diff to current |
2010-02-02 |
Tim King | Switched cnf conversion to go through CnfStream. |
blob | commitdiff | raw | diff to current |
2010-01-30 |
Morgan Deters | cnf conversion (variable-introducing), cleanups, fixes... |
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-10 |
Dejan Jovanović | killing expr into node... |
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-24 |
Morgan Deters | various fixes and updates to use and support parser |
blob | commitdiff | raw | diff to current |
2009-11-23 |
Morgan Deters | fixups, file comments |
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 |
|