| 2017-03-21 |
ajreynol | Improve computeCareGraph functions to check shared... |
blob | commitdiff | raw |
| 2017-03-03 |
ajreynol | Fix for collectModelInfo related to finite types +... |
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 |
| 2016-12-02 |
Tim King | Merge pull request #95 from 4tXJ7f/fix_sierra_build |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
Clark Barrett | Merge pull request #113 from 4tXJ7f/remove_extract_rule |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
ajreynol | Bug fixes and refactoring of parametric datatypes,... |
blob | commitdiff | raw | diff to current |
| 2016-08-24 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-08-16 |
ajreynol | Initial infrastructure for ExtTheory, generalize extend... |
blob | commitdiff | raw | diff to current |
| 2016-08-12 |
ajreynol | Minor fixes to model construction to take singleton... |
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-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-04 |
ajreynol | Remove NodeListMap from datatypes and equality inferenc... |
blob | commitdiff | raw | diff to current |
| 2016-06-03 |
ajreynol | Simple memory fixes, minor cleanup in quantifiers. |
blob | commitdiff | raw | diff to current |
| 2016-05-23 |
ajreynol | Fix related to parametric sorts whose interpretation... |
blob | commitdiff | raw | diff to current |
| 2016-05-20 |
ajreynol | Minor fix to strings, cleanup in datatypes. |
blob | commitdiff | raw | diff to current |
| 2016-05-20 |
ajreynol | Improvements to theory combination + strings: do not... |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
| 2016-04-12 |
ajreynol | Bug fixes related to parametric datatypes + theory... |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-03-30 |
ajreynol | Updates to E-matching to avoid entailed instantiations... |
blob | commitdiff | raw | diff to current |
| 2016-03-23 |
Tim King | Garbage collecting the EqcInfo s in TheoryDatatypes... |
blob | commitdiff | raw | diff to current |
| 2016-02-29 |
ajreynol | Minor options to datatypes. |
blob | commitdiff | raw | diff to current |
| 2016-02-24 |
ajreynol | Add entailment checks between length terms to reduce... |
blob | commitdiff | raw | diff to current |
| 2016-02-16 |
ajreynol | More simplification to internal implementation of tuple... |
blob | commitdiff | raw | diff to current |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastru... |
blob | commitdiff | raw | diff to current |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
blob | commitdiff | raw | diff to current |
| 2016-02-05 |
ajreynol | Add two optimizations for datatypes, currently disabled... |
blob | commitdiff | raw | diff to current |
| 2016-01-28 |
Tim King | Adding listeners to Options. |
blob | commitdiff | raw | diff to current |
| 2016-01-19 |
ajreynol | Bug fixes for model construction with codatatypes,... |
blob | commitdiff | raw | diff to current |
| 2016-01-13 |
ajreynol | Lemma cache datatypes. Do not send true lemma in quanti... |
blob | commitdiff | raw | diff to current |
| 2016-01-06 |
Tim King | Add SmtGlobals Class |
blob | commitdiff | raw | diff to current |
| 2015-12-22 |
ajreynol | Bug fix uf-ss-totality. |
blob | commitdiff | raw | diff to current |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involvi... |
blob | commitdiff | raw | diff to current |
| 2015-12-15 |
Tim King | Refactoring Options Handler & Library Cycle Breaking |
blob | commitdiff | raw | diff to current |
| 2015-09-11 |
ajreynol | Minor cleanup related to codatatypes. |
blob | commitdiff | raw | diff to current |
| 2015-09-10 |
ajreynol | Models for codatatypes. Fixes bug 662. |
blob | commitdiff | raw | diff to current |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2015-08-21 |
ajreynol | Minor changes related to codatatypes for 1.5 release. |
blob | commitdiff | raw | diff to current |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
blob | commitdiff | raw | diff to current |
| 2015-05-02 |
ajreynol | Minor fix for corner cases of fmf-fun, fix for --dt... |
blob | commitdiff | raw | diff to current |
| 2015-04-17 |
Kshitij Bansal | Merge pull request #72 from kbansal/decision-requirephase |
blob | commitdiff | raw | diff to current |
| 2015-04-02 |
Kshitij Bansal | Merge pull request #71 from kbansal/const-are-triggers |
blob | commitdiff | raw | diff to current |
| 2015-03-25 |
Kshitij Bansal | change const are triggers from false to true in equalit... |
blob | commitdiff | raw | diff to current |
| 2015-03-04 |
ajreynol | More work on arithmetic single invocation synthesis... |
blob | commitdiff | raw | diff to current |
| 2015-02-22 |
ajreynol | New trigger options. --inst-no-entail on by default... |
blob | commitdiff | raw | diff to current |
| 2015-02-13 |
ajreynol | Handle recursive singleton case for codatatypes, add... |
blob | commitdiff | raw | diff to current |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-02-04 |
ajreynol | Refactor sygus_util to TermDb. Initial work on solutio... |
blob | commitdiff | raw | diff to current |
| 2015-02-02 |
ajreynol | Single invocation module for counterexample guided... |
blob | commitdiff | raw | diff to current |
| 2015-02-01 |
ajreynol | Generalization of sygus lemmas based on arguments and... |
blob | commitdiff | raw | diff to current |
| 2015-01-31 |
ajreynol | Lemmas instead of conflicts in sygus sym break (do... |
blob | commitdiff | raw | diff to current |
| 2015-01-30 |
ajreynol | Generalize conflict clauses in sygus sym break, merge... |
blob | commitdiff | raw | diff to current |
| 2015-01-29 |
ajreynol | Apply global search space narrowing for multiple synth... |
blob | commitdiff | raw | diff to current |
| 2015-01-29 |
ajreynol | Add module for sygus search space narrowing based on... |
blob | commitdiff | raw | diff to current |
| 2015-01-24 |
ajreynol | Add --lte-restrict-inst-closure option. Push dt.size... |
blob | commitdiff | raw | diff to current |
| 2015-01-23 |
ajreynol | CEGQI fairness based on term height. Fix sygus-nf... |
blob | commitdiff | raw | diff to current |
| 2015-01-22 |
ajreynol | Do not drop patterns during boolean term rewriting... |
blob | commitdiff | raw | diff to current |
| 2015-01-21 |
ajreynol | Initial work on sygusNormalForm. |
blob | commitdiff | raw | diff to current |
| 2015-01-20 |
ajreynol | Mark datatypes as sygus. Add option to normalize sygus... |
blob | commitdiff | raw | diff to current |
| 2015-01-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-12-27 |
Dejan Jovanovic | Adding an option to the equality engine constructor... |
blob | commitdiff | raw | diff to current |
| 2014-12-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-12-22 |
ajreynol | Do not collapse wrongly applied selectors for non-well... |
blob | commitdiff | raw | diff to current |
| 2014-12-11 |
ajreynol | Option to enable/disable cyclicity check in datatypes. |
blob | commitdiff | raw | diff to current |
| 2014-12-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-12-06 |
ajreynol | Fix dt.size care graph. |
blob | commitdiff | raw | diff to current |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy... |
blob | commitdiff | raw | diff to current |
| 2014-11-17 |
Morgan Deters | New, uniform checkTime statistic for all theories ... |
blob | commitdiff | raw | diff to current |
| 2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewrite... |
blob | commitdiff | raw | diff to current |
| 2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression. |
blob | commitdiff | raw | diff to current |
| 2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup... |
blob | commitdiff | raw | diff to current |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in... |
blob | commitdiff | raw | diff to current |
| 2014-11-06 |
ajreynol | Minor fix for getInstCons |
blob | commitdiff | raw | diff to current |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
blob | commitdiff | raw | diff to current |
| 2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. |
blob | commitdiff | raw | diff to current |
| 2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug... |
blob | commitdiff | raw | diff to current |
| 2014-11-01 |
ajreynol | Simplify which lemmas to communicate in dt. |
blob | commitdiff | raw | diff to current |
| 2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma... |
blob | commitdiff | raw | diff to current |
| 2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,... |
blob | commitdiff | raw | diff to current |
| 2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ... |
blob | commitdiff | raw | diff to current |
| 2014-10-20 |
ajreynol | Minor cleanup in datatypes. |
blob | commitdiff | raw | diff to current |
| 2014-10-18 |
ajreynol | Add dt lemma: zero size implies nullary constructor. |
blob | commitdiff | raw | diff to current |
| 2014-10-18 |
ajreynol | Fix for bounded integers when incremental, fixes bug... |
blob | commitdiff | raw | diff to current |
| 2014-10-17 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-10-16 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-10-16 |
ajreynol | Use n-ary splits instead of binary splits in theory... |
blob | commitdiff | raw | diff to current |
| 2014-10-16 |
ajreynol | Add dt.size to datatypes theory. Add option for fairne... |
blob | commitdiff | raw | diff to current |
| 2014-10-11 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-10-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.4.x' |
blob | commitdiff | raw | diff to current |
| 2014-10-09 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history