| 2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
blob | commitdiff | raw |
| 2011-10-28 |
Liana Hadarean | merged the proofgen3 branch into trunk: |
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-09-30 |
Morgan Deters | fixes to incremental simplification, cnf routines,... |
blob | commitdiff | raw | diff to current |
| 2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
blob | commitdiff | raw | diff to current |
| 2011-09-20 |
Morgan Deters | Merge from "swig" branch: language binding for Java... |
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-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw | diff to current |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
| 2011-05-02 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
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-19 |
Morgan Deters | Merge from ufprop branch, including: |
blob | commitdiff | raw | diff to current |
| 2010-11-16 |
Morgan Deters | SmtEngine now fails with a ModalException if --incremen... |
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 | cleanup, documentation, SMT-LIBv2 compliance |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Morgan Deters | removing unused functionality from util; related to... |
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 | 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 | support for SMT-LIBv2 :named attributes, and attributes... |
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-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
blob | commitdiff | raw | diff to current |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
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-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-05 |
Morgan Deters | * public/private code untangled (smt/smt_engine.h no... |
blob | commitdiff | raw | diff to current |
| 2010-02-27 |
Morgan Deters | A bag of unrelated fixes to bring trunk more in-line... |
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-22 |
Dejan Jovanović | Small changes to the smt-engine, removed the assertions... |
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 |
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-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 |
| 2010-01-30 |
Morgan Deters | cnf conversion (variable-introducing), cleanups, fixes... |
blob | commitdiff | raw | diff to current |
| 2010-01-29 |
Morgan Deters | fixed CNF conversion, and more modular; CNF conversion... |
blob | commitdiff | raw | diff to current |
| 2010-01-26 |
Morgan Deters | cnf conversion |
blob | commitdiff | raw | diff to current |
| 2010-01-26 |
Morgan Deters | fixes to build structure, util classes, lots of 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-11 |
Dejan Jovanović | Extracted the public Expr and ExprManager interface... |
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-12-07 |
Morgan Deters | big check-in of various fixes and adjustments |
blob | commitdiff | raw | diff to current |
| 2009-12-03 |
Morgan Deters | parsing/expr/command/result/various other fixes |
blob | commitdiff | raw | diff to current |
| 2009-11-25 |
Morgan Deters | additional work on parser hookup, configuration + build |
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-24 |
Morgan Deters | configure option adjustments as per 11/24 meeting;... |
blob | commitdiff | raw | diff to current |
| 2009-11-23 |
Morgan Deters | fixups, file comments |
blob | commitdiff | raw |
| 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