| 2015-04-17 |
Kshitij Bansal | Merge pull request #72 from kbansal/decision-requirephase |
tree | commitdiff |
| 2015-04-02 |
Kshitij Bansal | Merge pull request #71 from kbansal/const-are-triggers |
tree | commitdiff |
| 2015-03-25 |
Kshitij Bansal | change const are triggers from false to true in equalit... |
tree | commitdiff |
| 2015-03-04 |
ajreynol | More work on arithmetic single invocation synthesis... |
tree | commitdiff |
| 2015-02-22 |
ajreynol | New trigger options. --inst-no-entail on by default... |
tree | commitdiff |
| 2015-02-13 |
ajreynol | Minor cleanup, remove unused files. |
tree | commitdiff |
| 2015-02-13 |
ajreynol | Handle recursive singleton case for codatatypes, add... |
tree | commitdiff |
| 2015-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2015-02-04 |
ajreynol | Refactor sygus_util to TermDb. Initial work on solutio... |
tree | commitdiff |
| 2015-02-02 |
ajreynol | Single invocation module for counterexample guided... |
tree | commitdiff |
| 2015-02-02 |
ajreynol | Representative programs must be minimal size, minor... |
tree | commitdiff |
| 2015-02-01 |
ajreynol | Generalization of sygus lemmas based on arguments and... |
tree | commitdiff |
| 2015-01-31 |
ajreynol | Bug fix fairness for commutative operators in sygus... |
tree | commitdiff |
| 2015-01-31 |
ajreynol | Lemmas instead of conflicts in sygus sym break (do... |
tree | commitdiff |
| 2015-01-30 |
ajreynol | Generalize conflict clauses in sygus sym break, merge... |
tree | commitdiff |
| 2015-01-29 |
ajreynol | Apply sygus search space narrowing for all subprograms... |
tree | commitdiff |
| 2015-01-29 |
ajreynol | Apply global search space narrowing for multiple synth... |
tree | commitdiff |
| 2015-01-29 |
ajreynol | Add module for sygus search space narrowing based on... |
tree | commitdiff |
| 2015-01-26 |
ajreynol | Output solutions for synthesis conjectures with --dump... |
tree | commitdiff |
| 2015-01-26 |
ajreynol | Generalize sygus search space narrowing to arbitrary... |
tree | commitdiff |
| 2015-01-24 |
ajreynol | Add --lte-restrict-inst-closure option. Push dt.size... |
tree | commitdiff |
| 2015-01-23 |
ajreynol | Refactor sygus arg nf. Minor improvements. |
tree | commitdiff |
| 2015-01-23 |
ajreynol | CEGQI fairness based on term height. Fix sygus-nf... |
tree | commitdiff |
| 2015-01-22 |
ajreynol | Narrow sygus search space based on NNF and rewriting... |
tree | commitdiff |
| 2015-01-22 |
ajreynol | Do not drop patterns during boolean term rewriting... |
tree | commitdiff |
| 2015-01-21 |
ajreynol | Avoid redundant constant arguments for SygusNormalForm... |
tree | commitdiff |
| 2015-01-21 |
ajreynol | Initial work on sygusNormalForm. |
tree | commitdiff |
| 2015-01-20 |
ajreynol | Mark datatypes as sygus. Add option to normalize sygus... |
tree | commitdiff |
| 2015-01-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-12-28 |
ajreynol | Disable prenex by default when using fmf bound int... |
tree | commitdiff |
| 2014-12-27 |
Dejan Jovanovic | Adding an option to the equality engine constructor... |
tree | commitdiff |
| 2014-12-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-12-22 |
ajreynol | Do not collapse wrongly applied selectors for non-well... |
tree | commitdiff |
| 2014-12-11 |
ajreynol | Option to enable/disable cyclicity check in datatypes. |
tree | commitdiff |
| 2014-12-09 |
Morgan Deters | Better error description (related to bug 605). |
tree | commitdiff |
| 2014-12-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-12-06 |
ajreynol | Fix dt.size care graph. |
tree | commitdiff |
| 2014-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy... |
tree | commitdiff |
| 2014-11-17 |
Morgan Deters | New, uniform checkTime statistic for all theories ... |
tree | commitdiff |
| 2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewrite... |
tree | commitdiff |
| 2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression. |
tree | commitdiff |
| 2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup... |
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 | Minor fix for getInstCons |
tree | commitdiff |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
tree | commitdiff |
| 2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. |
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-11-01 |
ajreynol | Simplify which lemmas to communicate in dt. |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma... |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,... |
tree | commitdiff |
| 2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ... |
tree | commitdiff |
| 2014-10-20 |
ajreynol | Minor cleanup in datatypes. |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Fix assertion. |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Add dt lemma: zero size implies nullary constructor. |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Fix for bounded integers when incremental, fixes bug... |
tree | commitdiff |
| 2014-10-17 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-16 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-16 |
ajreynol | Use n-ary splits instead of binary splits in theory... |
tree | commitdiff |
| 2014-10-16 |
ajreynol | Add dt.size to datatypes theory. Add option for fairne... |
tree | commitdiff |
| 2014-10-11 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.4.x' |
tree | commitdiff |
| 2014-10-09 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-02 |
Morgan Deters | Merge branch '1.4.x'. |
tree | commitdiff |
| 2014-09-30 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-27 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-26 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-25 |
ajreynol | Fair datatype enumeration. |
tree | commitdiff |
| 2014-09-24 |
ajreynol | Fix infinite loop in datatypes enumerator. Minor work... |
tree | commitdiff |
| 2014-09-24 |
ajreynol | Partial support for codatatype models. |
tree | commitdiff |
| 2014-09-23 |
ajreynol | Do not throw error when codatatype is not well-founded... |
tree | commitdiff |
| 2014-09-17 |
Kshitij Bansal | Merge branch '1.4.x' while ignoring commit 8d5eb49. |
tree | commitdiff |
| 2014-09-17 |
Kshitij Bansal | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-09-03 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2014-09-03 |
Kshitij Bansal | check() optimization |
tree | commitdiff |
| 2014-09-03 |
ajreynol | Implement and enable --dt-var-exp-quant, cleanup trace... |
tree | commitdiff |
| 2014-08-27 |
ajreynol | Fix assertion in rep_set.cpp, avoid full check in datat... |
tree | commitdiff |
| 2014-08-26 |
ajreynol | Bug fixes for --purify-triggers, --dt-force-assignment. |
tree | commitdiff |
| 2014-08-22 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-08-22 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-08-19 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-08-18 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-07-19 |
ajreynol | Minor fix for explanations for co-datatypes. Bug fix... |
tree | commitdiff |
| 2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
tree | commitdiff |
| 2014-07-01 |
Morgan Deters | Update copyrights. |
tree | commitdiff |
| 2014-07-01 |
Morgan Deters | Merge pull request #44 from mdeters/prio-queue-updates |
tree | commitdiff |
| 2014-07-01 |
Morgan Deters | Merge pull request #45 from mdeters/turn-off-strings-exp |
tree | commitdiff |
| 2014-06-30 |
Kshitij Bansal | Merge pull request #47 from kbansal/sets |
tree | commitdiff |
| 2014-06-28 |
Morgan Deters | Fix bug in datatypes options specification |
tree | commitdiff |
| 2014-06-26 |
Morgan Deters | Merge tag 'smtcomp2014-resubmission' |
tree | commitdiff |
| next |
projects / cvc5.git / history