| 2017-11-15 |
Tim King | Adding garbage collection for Proof objects. (#1294) |
blob | commitdiff | raw |
| 2017-11-13 |
Andrew Reynolds | Disable sygus qe preprocessing by default (#1353) |
blob | commitdiff | raw | diff to current |
| 2017-11-09 |
Andrew Reynolds | Higher-order prep (#1338) |
blob | commitdiff | raw | diff to current |
| 2017-11-07 |
Andrew Reynolds | Allow FORALL in quantifier elimination command (#1322) |
blob | commitdiff | raw | diff to current |
| 2017-11-03 |
Andrew Reynolds | Sygus clean main (#1297) |
blob | commitdiff | raw | diff to current |
| 2017-10-28 |
Andres Noetzli | Change bvudiv semantics based on input language (#1292) |
blob | commitdiff | raw | diff to current |
| 2017-10-24 |
Aina Niemetz | CBQI BV: Add ULT/SLT inverse handling. (#1268) |
blob | commitdiff | raw | diff to current |
| 2017-10-20 |
Andrew Reynolds | Make Sygus conjectures higher-order (#1244) |
blob | commitdiff | raw | diff to current |
| 2017-10-17 |
Clark Barrett | Fix for issue 1247 (#1257) |
blob | commitdiff | raw | diff to current |
| 2017-10-11 |
Andrew Reynolds | Ho Lambda Lifting (#1116) |
blob | commitdiff | raw | diff to current |
| 2017-10-11 |
Andrew Reynolds | Move unsat core names to smt engine (#1192) |
blob | commitdiff | raw | diff to current |
| 2017-10-10 |
Andrew Reynolds | Split term database (#1206) |
blob | commitdiff | raw | diff to current |
| 2017-09-19 |
Andres Noetzli | Fix issue #1074, improve non-fatal error handling ... |
blob | commitdiff | raw | diff to current |
| 2017-09-14 |
Tim King | Simplifying the throw specifier of SmtEngine::checkSat... |
blob | commitdiff | raw | diff to current |
| 2017-09-14 |
Martin | Floating point symfpu support (#1093) |
blob | commitdiff | raw | diff to current |
| 2017-09-10 |
Andrew Reynolds | Ensure that expand definitions is called on all non... |
blob | commitdiff | raw | diff to current |
| 2017-08-24 |
Andrew Reynolds | Merge pull request #191 from timothy-king/cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-08-24 |
Andres Noetzli | Fix typos |
blob | commitdiff | raw | diff to current |
| 2017-08-07 |
ajreynol | Make quantifier elimination more robust to preprocessing. |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Merge branch 'master' into cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Moving from the gnu extensions for hash maps to the... |
blob | commitdiff | raw | diff to current |
| 2017-07-20 |
Tim King | Removing the unused CDAttribute. This makes CDHashMap... |
blob | commitdiff | raw | diff to current |
| 2017-07-13 |
Aina Niemetz | Merge pull request #188 from aniemetz/cx11 |
blob | commitdiff | raw | diff to current |
| 2017-07-12 |
ajreynol | Make type rules more strict for operators whose type... |
blob | commitdiff | raw | diff to current |
| 2017-07-10 |
ajreynol | Do not exit when value/model/unsat-core/proof is reques... |
blob | commitdiff | raw | diff to current |
| 2017-07-10 |
ajreynol | Merge datatype shared selectors/sygus comp 2017 branch... |
blob | commitdiff | raw | diff to current |
| 2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2017-05-31 |
ajreynol | Fix model construction for BV with cbqi. Minor change... |
blob | commitdiff | raw | diff to current |
| 2017-05-31 |
ajreynol | Minor change to defaults, update smt comp script, minor... |
blob | commitdiff | raw | diff to current |
| 2017-05-12 |
Andres Notzli | Make signal handlers safer |
blob | commitdiff | raw | diff to current |
| 2017-05-05 |
ajreynol | Do not eliminate extended arithmetic symbols when finit... |
blob | commitdiff | raw | diff to current |
| 2017-05-04 |
guykatzz | fixing bug 790: track dependencies when the unsatCores... |
blob | commitdiff | raw | diff to current |
| 2017-04-22 |
Clark Barrett | Merge pull request #151 from 4tXJ7f/fix_debug |
blob | commitdiff | raw | diff to current |
| 2017-04-21 |
Andres Noetzli | Move assertion out of loop for better performance |
blob | commitdiff | raw | diff to current |
| 2017-04-20 |
Andrew Reynolds | Merge pull request #149 from PaulMeng/master |
blob | commitdiff | raw | diff to current |
| 2017-04-20 |
ajreynol | Minor fixes. |
blob | commitdiff | raw | diff to current |
| 2017-04-14 |
ajreynol | Fix for fmf-fun when the option is set by user command. |
blob | commitdiff | raw | diff to current |
| 2017-04-12 |
ajreynol | Add nullary operator metakind. |
blob | commitdiff | raw | diff to current |
| 2017-04-07 |
ajreynol | Change option names for nl. |
blob | commitdiff | raw | diff to current |
| 2017-04-04 |
Clark Barrett | Merge pull request #141 from 4tXJ7f/remove_def |
blob | commitdiff | raw | diff to current |
| 2017-04-03 |
Andrew Reynolds | Merge pull request #142 from timothy-king/nlAlgMerge |
blob | commitdiff | raw | diff to current |
| 2017-04-03 |
Tim King | Adding a model based axiom instantiation scheme for... |
blob | commitdiff | raw | diff to current |
| 2017-03-30 |
Clark Barrett | Merge pull request #139 from 4tXJ7f/remove_throw |
blob | commitdiff | raw | diff to current |
| 2017-03-30 |
Andres Notzli | [Coverity] Remove throw qualifiers in src/smt |
blob | commitdiff | raw | diff to current |
| 2017-03-24 |
ajreynol | Refactor model building for quantifiers to be a single... |
blob | commitdiff | raw | diff to current |
| 2017-03-23 |
Clark Barrett | Fixing warning message. |
blob | commitdiff | raw | diff to current |
| 2017-03-23 |
guykatzz | support incremental unsat cores |
blob | commitdiff | raw | diff to current |
| 2017-03-16 |
ajreynol | Minor fixes, always expand applications of lambdas... |
blob | commitdiff | raw | diff to current |
| 2017-03-16 |
ajreynol | Parsing support for SMT LIB 2.6. Minor fixes for printi... |
blob | commitdiff | raw | diff to current |
| 2017-03-06 |
Clark Barrett | Adding support for bool-to-bv |
blob | commitdiff | raw | diff to current |
| 2017-03-02 |
ajreynol | Minor cleanup and reorganization related to last commit. |
blob | commitdiff | raw | diff to current |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
blob | commitdiff | raw | diff to current |
| 2017-01-18 |
Andrew Reynolds | Merge pull request #128 from 4tXJ7f/fix_lfsc_perf |
blob | commitdiff | raw | diff to current |
| 2017-01-14 |
Clark Barrett | Fix call to SExpr constructor for greater portability. |
blob | commitdiff | raw | diff to current |
| 2017-01-11 |
Chad Brewbaker | revert |
blob | commitdiff | raw | diff to current |
| 2017-01-07 |
Chad Brewbaker | quashing debug memory leak |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
guykatzz | Turned off nonClausalSimplify when using fewerPreproces... |
blob | commitdiff | raw | diff to current |
| 2016-12-07 |
ajreynol | Refactoring, generalization of bounded inference module... |
blob | commitdiff | raw | diff to current |
| 2016-12-06 |
Clark Barrett | Added "dump=raw-benchmark" option for dumping all user... |
blob | commitdiff | raw | diff to current |
| 2016-11-21 |
ajreynol | Refactoring related to track instantiation option. |
blob | commitdiff | raw | diff to current |
| 2016-11-18 |
Clark Barrett | Merge pull request #110 from 4tXJ7f/fix_makefiles |
blob | commitdiff | raw | diff to current |
| 2016-11-18 |
Clark Barrett | Add support for set-logic ALL, fix compiler error in... |
blob | commitdiff | raw | diff to current |
| 2016-11-12 |
Tim King | Merge pull request #105 from timothy-king/delete-maxed-out |
blob | commitdiff | raw | diff to current |
| 2016-11-11 |
Clark Barrett | Enable eager bitblasting for QF_ABV when no stores... |
blob | commitdiff | raw | diff to current |
| 2016-11-10 |
ajreynol | Add option for enabling/disabling lazy extended functio... |
blob | commitdiff | raw | diff to current |
| 2016-11-09 |
Tim King | Merge branch 'master' into uniq-ptr |
blob | commitdiff | raw | diff to current |
| 2016-11-08 |
ajreynol | Add a few options to separation logic and sets. Minor... |
blob | commitdiff | raw | diff to current |
| 2016-11-04 |
ajreynol | Fix a few more minor memory leaks. |
blob | commitdiff | raw | diff to current |
| 2016-11-02 |
ajreynol | Fix bug in separation logic for finite pto-data types... |
blob | commitdiff | raw | diff to current |
| 2016-11-01 |
ajreynol | Fix memory leak in TheorySetsRels. Minor cleanup. |
blob | commitdiff | raw | diff to current |
| 2016-11-01 |
ajreynol | Working memory leak free version, changes interface... |
blob | commitdiff | raw | diff to current |
| 2016-10-28 |
ajreynol | Add get instantiations utilities to API. |
blob | commitdiff | raw | diff to current |
| 2016-10-26 |
Andrew Reynolds | Merge pull request #98 from 4tXJ7f/fix_dist_build |
blob | commitdiff | raw | diff to current |
| 2016-10-26 |
ajreynol | New implementation of sets+cardinality. Merge Paul... |
blob | commitdiff | raw | diff to current |
| 2016-10-11 |
Paul Meng | Merge branch 'origin' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-09-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options... |
blob | commitdiff | raw | diff to current |
| 2016-09-12 |
ajreynol | Refactor prenex modes. |
blob | commitdiff | raw | diff to current |
| 2016-09-12 |
ajreynol | Remove old implementation of cbqi |
blob | commitdiff | raw | diff to current |
| 2016-09-09 |
ajreynol | Support for separation logic + EPR. Refactor preprocess... |
blob | commitdiff | raw | diff to current |
| 2016-09-03 |
ajreynol | Miniscope top level conjunctions for prenex normal... |
blob | commitdiff | raw | diff to current |
| 2016-09-03 |
ajreynol | Option for prenex normal form |
blob | commitdiff | raw | diff to current |
| 2016-09-02 |
Tim King | Merge pull request #91 from timothy-king/no-throw |
blob | commitdiff | raw | diff to current |
| 2016-09-01 |
ajreynol | Cleanup quantifier elimination in smt engine. |
blob | commitdiff | raw | diff to current |
| 2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to... |
blob | commitdiff | raw | diff to current |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions. |
blob | commitdiff | raw | diff to current |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
blob | commitdiff | raw | diff to current |
| 2016-08-12 |
guykatzz | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes |
blob | commitdiff | raw | diff to current |
| 2016-08-12 |
Andres Notzli | Add support for fewer preprocessing holes |
blob | commitdiff | raw | diff to current |
| 2016-07-07 |
ajreynol | Refactoring of strings preprocess module. When enabled... |
blob | commitdiff | raw | diff to current |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-06-20 |
Guy | Addressed a bug that occurs when proof production is... |
blob | commitdiff | raw | diff to current |
| 2016-06-20 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-06-17 |
ajreynol | Support for separation logic. Enable cbqi by default... |
blob | commitdiff | raw | diff to current |
| 2016-06-08 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-06-06 |
guykatzz | Merge pull request #85 from CVC4/master_for_proof_merge |
blob | commitdiff | raw | diff to current |
| 2016-06-03 |
ajreynol | Simple memory fixes, minor cleanup in quantifiers. |
blob | commitdiff | raw | diff to current |
| 2016-06-02 |
Guy | Merge from proof branch |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history