| 2020-01-30 |
Andrew Reynolds | Ensure literals in FMF decision strategies are in the... |
tree | commitdiff |
| 2019-09-18 |
Andrew Reynolds | Decouple fmf-bound and finite-model-find (#3297) |
tree | commitdiff |
| 2019-09-06 |
Mathias Preiner | Remove SMT1 parser. (#3228) |
tree | commitdiff |
| 2019-06-04 |
Andres Noetzli | Add check that result matches benchmark status (#3028) |
tree | commitdiff |
| 2018-12-11 |
Andrew Reynolds | Remove alternate versions of mbqi (#2742) |
tree | commitdiff |
| 2018-09-22 |
Aina Niemetz | cmake: Added regression tests and target make regress. |
tree | commitdiff |
| 2018-09-22 |
Aina Niemetz | cmake: Added initial build infrastructure. |
tree | commitdiff |
| 2018-08-28 |
Andrew Reynolds | Fix sort inference for quantified variables of interpre... |
tree | commitdiff |
| 2018-08-17 |
Andrew Reynolds | Fix spurious warning in sort inference (#2331) |
tree | commitdiff |
| 2018-08-15 |
Andrew Reynolds | Make sort inference a preprocessing pass (#2309) |
tree | commitdiff |
| 2018-04-06 |
Andres Noetzli | Python regression script (#1662) |
tree | commitdiff |
| 2018-03-23 |
Andrew Reynolds | Add a few quantifiers regressions to improve coverage... |
tree | commitdiff |
| 2018-03-21 |
Andres Noetzli | Move regression tests to single Makefile.am (#1658) |
tree | commitdiff |
| 2018-02-15 |
Andrew Reynolds | Refactor regressions (#1581) |
tree | commitdiff |
| 2017-11-04 |
Andrew Reynolds | Suppport SAT logic (#1310) |
tree | commitdiff |
| 2017-09-28 |
Andrew Reynolds | Improve finite model finding for recursive predicates... |
tree | commitdiff |
| 2017-09-10 |
Andrew Reynolds | Ensure that expand definitions is called on all non... |
tree | commitdiff |
| 2017-08-31 |
Andrew Reynolds | Answer unknown when uf-ss=no-minimal is combined with... |
tree | commitdiff |
| 2017-08-24 |
Andrew Reynolds | Merge pull request #191 from timothy-king/cleanup-regexp |
tree | commitdiff |
| 2017-08-04 |
ajreynol | Set default language to smt lib 2.6 (including as a... |
tree | commitdiff |
| 2017-05-31 |
ajreynol | Minor change to defaults, update smt comp script, minor... |
tree | commitdiff |
| 2017-05-05 |
ajreynol | Do not eliminate extended arithmetic symbols when finit... |
tree | commitdiff |
| 2017-04-28 |
ajreynol | Do not eliminate non-standard arithmetic operators... |
tree | commitdiff |
| 2017-04-24 |
ajreynol | Fixes and simplifications for fmf mbqi. |
tree | commitdiff |
| 2017-04-14 |
ajreynol | Fix for fmf-fun when the option is set by user command. |
tree | commitdiff |
| 2017-04-06 |
Clark Barrett | Merge pull request #143 from FabianWolff/master |
tree | commitdiff |
| 2017-04-05 |
Andrew Reynolds | Merge pull request #145 from 4tXJ7f/fix_lfsc_args |
tree | commitdiff |
| 2017-04-05 |
ajreynol | Caching for fun def process, add regression. |
tree | commitdiff |
| 2017-03-22 |
ajreynol | Minor fix for bounded integers. |
tree | commitdiff |
| 2017-03-15 |
Clark Barrett | Merge pull request #134 from 4tXJ7f/fix_host |
tree | commitdiff |
| 2017-03-15 |
ajreynol | Allow 0 argument recursive functions. Fixes bug 782. |
tree | commitdiff |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
tree | commitdiff |
| 2017-02-07 |
ajreynol | Generalize finite bound inference to unifiable variable... |
tree | commitdiff |
| 2017-01-18 |
Andrew Reynolds | Merge pull request #128 from 4tXJ7f/fix_lfsc_perf |
tree | commitdiff |
| 2017-01-14 |
Clark Barrett | Merge pull request #130 from chadbrewbaker/master |
tree | commitdiff |
| 2017-01-11 |
Clark Barrett | Merge pull request #129 from timothy-king/regression... |
tree | commitdiff |
| 2017-01-11 |
Clark Barrett | Merge pull request #131 from makaimann/fix_702 |
tree | commitdiff |
| 2017-01-11 |
ajreynol | Fix for when variables are (partially) bound in multipl... |
tree | commitdiff |
| 2017-01-04 |
Tim King | Marking regression test files as non-executable. |
tree | commitdiff |
| 2016-12-07 |
ajreynol | Fix boolean term conversion for INST_ATTRIBUTE, fixes... |
tree | commitdiff |
| 2016-12-07 |
guykatzz | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2016-12-07 |
ajreynol | Refactoring, generalization of bounded inference module... |
tree | commitdiff |
| 2016-12-02 |
Tim King | Merge pull request #95 from 4tXJ7f/fix_sierra_build |
tree | commitdiff |
| 2016-12-02 |
Clark Barrett | Merge pull request #113 from 4tXJ7f/remove_extract_rule |
tree | commitdiff |
| 2016-12-02 |
ajreynol | Refactor preprocessing of models in fmf. Fix options... |
tree | commitdiff |
| 2016-11-18 |
Clark Barrett | Merge pull request #110 from 4tXJ7f/fix_makefiles |
tree | commitdiff |
| 2016-11-18 |
Andres Notzli | Fix Makefiles in test |
tree | commitdiff |
| 2016-10-21 |
ajreynol | Move slow regress0 benchmarks to regress1, increment... |
tree | commitdiff |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
tree | commitdiff |
| 2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification... |
tree | commitdiff |
| 2016-05-23 |
ajreynol | Fix related to parametric sorts whose interpretation... |
tree | commitdiff |
| 2016-04-20 |
PaulMeng | update from the master |
tree | commitdiff |
| 2016-04-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip. |
tree | commitdiff |
| 2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external... |
tree | commitdiff |
| 2016-03-07 |
ajreynol | Minor change to F-Length inference in strings. No inter... |
tree | commitdiff |
| 2016-02-23 |
ajreynol | Fix term database for non-equal, congruent terms in... |
tree | commitdiff |
| 2016-02-19 |
ajreynol | Fixes and improvements for datatypes properties and... |
tree | commitdiff |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas... |
tree | commitdiff |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2016-02-09 |
ajreynol | Fix regression, minor change to output. |
tree | commitdiff |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
tree | commitdiff |
| 2016-02-01 |
ajreynol | Simplify fmc model construction, add regression. Improv... |
tree | commitdiff |
| 2016-01-20 |
ajreynol | Fix bug in fmc mbqi where modelscomputed for mbqi could... |
tree | commitdiff |
| 2016-01-19 |
ajreynol | Bug fixes for model construction with codatatypes,... |
tree | commitdiff |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs. |
tree | commitdiff |
| 2016-01-14 |
ajreynol | Ensure model construction for parametric sorts involvin... |
tree | commitdiff |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involvi... |
tree | commitdiff |
| 2015-12-22 |
ajreynol | Bug fix for cbqi, do not use model values for terms... |
tree | commitdiff |
| 2015-11-07 |
Tim King | Changing file permissions to add or remove executable... |
tree | commitdiff |
| 2015-11-05 |
Tim King | Merging the google branch back into master. |
tree | commitdiff |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
tree | commitdiff |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modul... |
tree | commitdiff |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
tree | commitdiff |
| 2015-04-28 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-04-28 |
Clark Barrett | Disambiguate namespaces in options, fix permissions |
tree | commitdiff |
| 2015-04-26 |
ajreynol | Bug fixes and improvements for mbqi with theory symbols... |
tree | commitdiff |
| 2015-04-23 |
Clark Barrett | Merge branch 'master' into google |
tree | commitdiff |
| 2015-04-23 |
Clark Barrett | A few more minor updates to match google repository... |
tree | commitdiff |
| 2015-04-23 |
Liana Hadarean | Added option for --check-unsat-cores and various core... |
tree | commitdiff |
| 2015-04-21 |
Clark Barrett | Fix file permissions |
tree | commitdiff |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in... |
tree | commitdiff |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
tree | commitdiff |
| 2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug... |
tree | commitdiff |
| 2014-04-28 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
tree | commitdiff |
| 2014-04-14 |
Andrew Reynolds | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi... |
tree | commitdiff |
| 2014-04-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-04-10 |
Andrew Reynolds | Add support for cardinality constraints logic UFC.... |
tree | commitdiff |
| 2014-04-01 |
Tim King | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
tree | commitdiff |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| next |
projects / cvc5.git / history