| 2020-02-29 |
Andrew Reynolds | Replace conditional rewrite pass in quantifiers with... |
tree | commitdiff |
| 2020-02-08 |
Andres Noetzli | Make "unknown" non-critical for unsat cores check ... |
tree | commitdiff |
| 2019-09-04 |
Mathias Preiner | Remove duplicate regression tests. (#3227) |
tree | commitdiff |
| 2019-06-04 |
Andres Noetzli | Add check that result matches benchmark status (#3028) |
tree | commitdiff |
| 2019-04-16 |
Andrew Reynolds | Minor simplifications to theory quantifiers (#2953) |
tree | commitdiff |
| 2018-11-05 |
yoni206 | Increasing coverage (#2683) |
tree | commitdiff |
| 2018-09-25 |
Andrew Reynolds | Fix quantifiers selector over store rewrite (#2510) |
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-09-06 |
Andrew Reynolds | Refactor and document quantifiers variable elimination... |
tree | commitdiff |
| 2018-09-04 |
Andrew Reynolds | Make quantifiers strategies exit immediately when in... |
tree | commitdiff |
| 2018-08-21 |
Andres Noetzli | Remove support for *.expect files in regressions (... |
tree | commitdiff |
| 2018-08-07 |
Andrew Reynolds | Fix inference of pre and post conditions for non variab... |
tree | commitdiff |
| 2018-06-01 |
Andrew Reynolds | Fix quantified bv variable elimination (#2039) |
tree | commitdiff |
| 2018-06-01 |
Andrew Reynolds | Use monomial sum utility to solve for quantifiers... |
tree | commitdiff |
| 2018-05-23 |
Andres Noetzli | Set same options for proofs as for unsat cores (#1957) |
tree | commitdiff |
| 2018-04-25 |
Andrew Reynolds | Fix issue with multi-triggers that include variable... |
tree | commitdiff |
| 2018-03-21 |
Andres Noetzli | Move regression tests to single Makefile.am (#1658) |
tree | commitdiff |
| 2018-03-20 |
Andrew Reynolds | Enable CEGQI for non-linear (#1674) |
tree | commitdiff |
| 2018-02-15 |
Andrew Reynolds | Refactor regressions (#1581) |
tree | commitdiff |
| 2018-01-08 |
Andrew Reynolds | Improvements to quant+BV/Bool variable elimination... |
tree | commitdiff |
| 2018-01-03 |
Andrew Reynolds | Global negate (#1466) |
tree | commitdiff |
| 2017-12-21 |
Andrew Reynolds | Fixes for cbqi-bv (#1449) |
tree | commitdiff |
| 2017-12-21 |
Aina Niemetz | Add explicit disequality handling when generating side... |
tree | commitdiff |
| 2017-12-08 |
Aina Niemetz | Fixed side conditions for CBQI BV, added unit tests... |
tree | commitdiff |
| 2017-11-21 |
Andrew Reynolds | Cegqi bv remove extract terms preprocess pass (#1376) |
tree | commitdiff |
| 2017-11-15 |
Andrew Reynolds | Reenable some regressions, minor. (#1369) |
tree | commitdiff |
| 2017-11-14 |
Andrew Reynolds | Clean Ceg Instantiators (#1365) |
tree | commitdiff |
| 2017-11-01 |
Andrew Reynolds | CBQI BV choice expressions (#1296) |
tree | commitdiff |
| 2017-10-25 |
Aina Niemetz | CBQI BV: Add handling for missing operators. (#1274) |
tree | commitdiff |
| 2017-10-24 |
Aina Niemetz | CBQI BV: Add ULT/SLT inverse handling. (#1268) |
tree | commitdiff |
| 2017-10-13 |
Aina Niemetz | CBQI BV: Added EXTRACT handling. (#1240) |
tree | commitdiff |
| 2017-10-13 |
Andrew Reynolds | CBQI BV quick heuristics (#1239) |
tree | commitdiff |
| 2017-10-12 |
Andrew Reynolds | Initial support for solving bit-vector inequalities... |
tree | commitdiff |
| 2017-10-12 |
Aina Niemetz | Enable regressions for CBQI BV and fix inverse for... |
tree | commitdiff |
| 2017-10-12 |
Mathias Preiner | Add side conditions for UDIV_TOTAL, SHL, CONCAT. (... |
tree | commitdiff |
| 2017-10-11 |
Andrew Reynolds | Adds infrastructure for a rewriting pass in BvInstantia... |
tree | commitdiff |
| 2017-10-10 |
Aina Niemetz | CBQI BV: Add inverse for more operators. (#1213) |
tree | commitdiff |
| 2017-09-29 |
Andrew Reynolds | Simplify representation of inversion Skolems for bv... |
tree | commitdiff |
| 2017-09-29 |
Andrew Reynolds | Initial working version of BV word-level instantiation... |
tree | commitdiff |
| 2017-09-14 |
Andrew Reynolds | Remove unhandled subtypes (#1098) |
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-06-30 |
ajreynol | Minor change to trigger selection, fixes related to... |
tree | commitdiff |
| 2017-06-21 |
Andrew Reynolds | Merge pull request #175 from CVC4/fix_uninit |
tree | commitdiff |
| 2017-06-15 |
ajreynol | Add regression. |
tree | commitdiff |
| 2017-05-31 |
ajreynol | Fix model construction for BV with cbqi. Minor change... |
tree | commitdiff |
| 2017-05-31 |
ajreynol | Minor change to defaults, update smt comp script, minor... |
tree | commitdiff |
| 2017-04-04 |
ajreynol | Enable multi-trigger-linear by default, add option. |
tree | commitdiff |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
tree | commitdiff |
| 2017-01-04 |
Tim King | Marking regression test files as non-executable. |
tree | commitdiff |
| 2017-01-04 |
Tim King | Reverting two files encoding with DOS linebreaks back... |
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-11 |
Paul Meng | Merge branch 'origin' of https://github.com/CVC4/CVC4.git |
tree | commitdiff |
| 2016-10-01 |
Tim King | Merge pull request #93 from timothy-king/clang-format |
tree | commitdiff |
| 2016-09-20 |
ajreynol | More refactoring of cbqi. Add a few regressions. Add... |
tree | commitdiff |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2016-08-15 |
ajreynol | Enable bounded set membership with --fmf-bound. Map... |
tree | commitdiff |
| 2016-08-03 |
barrettcw | Merge pull request #87 from 4tXJ7f/fix_oob_access |
tree | commitdiff |
| 2016-07-28 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2016-07-28 |
ajreynol | Fix bug 749. |
tree | commitdiff |
| 2016-07-19 |
ajreynol | Add infrastructure for tracking instantiation lemmas... |
tree | commitdiff |
| 2016-07-05 |
ajreynol | Add option --trigger-active-sel. Recognize simple trigg... |
tree | commitdiff |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
tree | commitdiff |
| 2016-06-01 |
ajreynol | Fix to ignore a case of triggers with no free variables. |
tree | commitdiff |
| 2016-05-26 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2016-05-26 |
ajreynol | Use term indexing in TheoryUF::computeCareGraph. Do... |
tree | commitdiff |
| 2016-05-10 |
ajreynol | Fix for --inst-max-level |
tree | commitdiff |
| 2016-05-02 |
ajreynol | Clean up issues related to compiled scc in LFSC. Refact... |
tree | commitdiff |
| 2016-04-20 |
PaulMeng | update from the master |
tree | commitdiff |
| 2016-04-12 |
ajreynol | Bug fixes related to parametric datatypes + theory... |
tree | commitdiff |
| 2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of varia... |
tree | commitdiff |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational... |
tree | commitdiff |
| 2016-03-18 |
ajreynol | Limit duplicate propagating instances to avoid exponent... |
tree | commitdiff |
| 2016-03-12 |
ajreynol | Add options related to interleaving quantifiers and... |
tree | commitdiff |
| 2016-03-02 |
ajreynol | Work towards complete instantiation for datatypes. |
tree | commitdiff |
| 2016-03-01 |
ajreynol | Shorter explanations for strings based on tracking... |
tree | commitdiff |
| 2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for... |
tree | commitdiff |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2016-02-11 |
ajreynol | More aggressive conditional rewriting for quantified... |
tree | commitdiff |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
tree | commitdiff |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checkin... |
tree | commitdiff |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes... |
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-05 |
Tim King | Fixes some initialization and desctruction problems... |
tree | commitdiff |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
tree | commitdiff |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers. |
tree | commitdiff |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended... |
tree | commitdiff |
| 2015-10-22 |
ajreynol | Enable counterexample-guided quantifier instantiation... |
tree | commitdiff |
| 2015-09-24 |
ajreynol | Counterexample-guided instantiation for datatypes.... |
tree | commitdiff |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2015-08-27 |
ajreynol | Modify slow regressions. |
tree | commitdiff |
| 2015-08-24 |
ajreynol | Improvements to vts in cbqi, bug fix vts for non-atomic... |
tree | commitdiff |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for... |
tree | commitdiff |
| 2015-08-19 |
ajreynol | Implementation of model-based projection in cbqi, clean... |
tree | commitdiff |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split... |
tree | commitdiff |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested... |
tree | commitdiff |
| next |
projects / cvc5.git / history