| 2015-04-26 |
ajreynol | Bug fixes and improvements for mbqi with theory symbols...
|
commit | commitdiff | tree |
| 2015-04-24 |
ajreynol | More parser related bug fixes (define-funs-rec, declare...
|
commit | commitdiff | tree |
| 2015-04-24 |
ajreynol | Fix sygus parser for non-tokenized operators, reenable...
|
commit | commitdiff | tree |
| 2015-04-21 |
ajreynol | Fix bug in fmf mbqi=fmc with arrays. Add two datatypes...
|
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Fix option --quant-fun-wd. Add mk_starexec script...
|
commit | commitdiff | tree |
| 2015-04-16 |
ajreynol | Handle (degenerate) case of synthesis conjectures for...
|
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix unsat-core issues related to rewrite rules, quantifiers...
|
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Fix performance issue with variable triggers + instantiation...
|
commit | commitdiff | tree |
| 2015-04-09 |
ajreynol | Bug fix negative contains cache.
|
commit | commitdiff | tree |
| 2015-04-08 |
ajreynol | Make fun-def quantifiers carry the function app they...
|
commit | commitdiff | tree |
| 2015-04-07 |
ajreynol | Minor fixes for cegqi.
|
commit | commitdiff | tree |
| 2015-04-01 |
ajreynol | Improvements and bug fixes related to cbqi/cegqi. ...
|
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Parsing support for define-fun-rec/define-funs-rec.
|
commit | commitdiff | tree |
| 2015-03-23 |
ajreynol | Decouple counter-example guided quantifier instantiation...
|
commit | commitdiff | tree |
| 2015-03-11 |
ajreynol | Strings split on constant lengths, add length=0 to...
|
commit | commitdiff | tree |
| 2015-03-11 |
ajreynol | Minor fixes and improvements to cegqi-si for linear...
|
commit | commitdiff | tree |
| 2015-03-10 |
ajreynol | CNF proofs. Infrastructure for preprocessing proofs...
|
commit | commitdiff | tree |
| 2015-03-05 |
ajreynol | Minor fixes. Extend cegqi-si to real arithmetic.
|
commit | commitdiff | tree |
| 2015-03-04 |
ajreynol | More work on arithmetic single invocation synthesis...
|
commit | commitdiff | tree |
| 2015-02-26 |
ajreynol | Robust strategy for single invocation LIA synthesis...
|
commit | commitdiff | tree |
| 2015-02-22 |
ajreynol | New trigger options. --inst-no-entail on by default...
|
commit | commitdiff | tree |
| 2015-02-14 |
ajreynol | Fix unit tests.
|
commit | commitdiff | tree |
| 2015-02-13 |
ajreynol | Minor cleanup, remove unused files.
|
commit | commitdiff | tree |
| 2015-02-13 |
ajreynol | Handle recursive singleton case for codatatypes, add...
|
commit | commitdiff | tree |
| 2015-02-11 |
ajreynol | Better support for solving multiple functions with...
|
commit | commitdiff | tree |
| 2015-02-11 |
ajreynol | Move si solution reconstruction to own file, make more...
|
commit | commitdiff | tree |
| 2015-02-06 |
ajreynol | Handle missing cases for single inv solution reconstruction...
|
commit | commitdiff | tree |
| 2015-02-05 |
ajreynol | Working version of sygus solution reconstruction from...
|
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Initial draft of solution reconstruction into syntax...
|
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Work on solution reconstruction for single inv. Fix...
|
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Refactor sygus_util to TermDb. Initial work on solution...
|
commit | commitdiff | tree |
| 2015-02-04 |
ajreynol | Start work on simplifying single inv solutions. Minor.
|
commit | commitdiff | tree |
| 2015-02-03 |
ajreynol | Simple variable elimination for single inv properties...
|
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Solutions for single invocation conjectures.
|
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Single invocation module for counterexample guided...
|
commit | commitdiff | tree |
| 2015-02-02 |
ajreynol | Representative programs must be minimal size, minor...
|
commit | commitdiff | tree |
| 2015-02-01 |
ajreynol | Generalization of sygus lemmas based on arguments and...
|
commit | commitdiff | tree |
| 2015-01-31 |
ajreynol | Bug fix fairness for commutative operators in sygus...
|
commit | commitdiff | tree |
| 2015-01-31 |
ajreynol | Lemmas instead of conflicts in sygus sym break (do...
|
commit | commitdiff | tree |
| 2015-01-30 |
ajreynol | Generalize conflict clauses in sygus sym break, merge...
|
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Apply sygus search space narrowing for all subprograms...
|
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Restrict LtePartialInst instantiations based on E-matching...
|
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Apply global search space narrowing for multiple synth...
|
commit | commitdiff | tree |
| 2015-01-29 |
ajreynol | Add module for sygus search space narrowing based on...
|
commit | commitdiff | tree |
| 2015-01-28 |
ajreynol | Minor refactor CEGQI.
|
commit | commitdiff | tree |
| 2015-01-27 |
ajreynol | Always miniscope nested quantifiers. Disable miniscoping...
|
commit | commitdiff | tree |
| 2015-01-27 |
ajreynol | Recognize when synthesis conjectures are in single...
|
commit | commitdiff | tree |
| 2015-01-26 |
ajreynol | Output solutions for synthesis conjectures with --dump...
|
commit | commitdiff | tree |
| 2015-01-26 |
ajreynol | Generalize sygus search space narrowing to arbitrary...
|
commit | commitdiff | tree |
| 2015-01-24 |
ajreynol | Variable patterns only look at eligible terms. Minor...
|
commit | commitdiff | tree |
| 2015-01-24 |
ajreynol | Add --lte-restrict-inst-closure option. Push dt.size...
|
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | Refactor sygus arg nf. Minor improvements.
|
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | CEGQI fairness based on term height. Fix sygus-nf...
|
commit | commitdiff | tree |
| 2015-01-23 |
ajreynol | Rework inst-closure.
|
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Narrow sygus search space based on NNF and rewriting...
|
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Add option --lte-partial-inst. Remove inst-closure.
|
commit | commitdiff | tree |
| 2015-01-22 |
ajreynol | Do not drop patterns during boolean term rewriting...
|
commit | commitdiff | tree |
| 2015-01-21 |
ajreynol | Avoid redundant constant arguments for SygusNormalForm...
|
commit | commitdiff | tree |
| 2015-01-21 |
ajreynol | Initial work on sygusNormalForm.
|
commit | commitdiff | tree |
| 2015-01-20 |
ajreynol | Mark datatypes as sygus. Add option to normalize sygus...
|
commit | commitdiff | tree |
| 2015-01-20 |
ajreynol | Handle miniscoping of conjunctions in synthesis properties...
|
commit | commitdiff | tree |
| 2015-01-17 |
ajreynol | Avoid name conflicts for multiple synth-fun.
|
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Linearize multiplication by constants in sygus grammars...
|
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Allow uninterpreted/defined functions in Sygus grammars...
|
commit | commitdiff | tree |
| 2015-01-16 |
ajreynol | Minor: Ensure indexed terms are in EE. Add support...
|
commit | commitdiff | tree |
| 2014-12-28 |
ajreynol | Disable prenex by default when using fmf bound int...
|
commit | commitdiff | tree |
| 2014-12-22 |
ajreynol | Do not collapse wrongly applied selectors for non-well...
|
commit | commitdiff | tree |
| 2014-12-21 |
ajreynol | Add misc trigger options.
|
commit | commitdiff | tree |
| 2014-12-12 |
ajreynol | Add cvc parsing support for cardinality constraints...
|
commit | commitdiff | tree |
| 2014-12-11 |
ajreynol | Option to enable/disable cyclicity check in datatypes.
|
commit | commitdiff | tree |
| 2014-12-06 |
ajreynol | Fix dt.size care graph.
|
commit | commitdiff | tree |
| 2014-11-28 |
ajreynol | Synchronize conjecture generation with E-matching....
|
commit | commitdiff | tree |
| 2014-11-25 |
ajreynol | Fix bug in --term-db-mode=relevant with variable triggers...
|
commit | commitdiff | tree |
| 2014-11-21 |
ajreynol | Throw error when pattern is not list of terms.
|
commit | commitdiff | tree |
| 2014-11-21 |
ajreynol | Change default option to --inst-when=full-last-call...
|
commit | commitdiff | tree |
| 2014-11-20 |
ajreynol | Disable constants sharing in eq engine, disable hack...
|
commit | commitdiff | tree |
| 2014-11-18 |
ajreynol | Compute model basis only for fmf. Add another co-datatype...
|
commit | commitdiff | tree |
| 2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy...
|
commit | commitdiff | tree |
| 2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewriter...
|
commit | commitdiff | tree |
| 2014-11-14 |
ajreynol | Be lazier to consider EQC in UF+cardinality solver...
|
commit | commitdiff | tree |
| 2014-11-13 |
ajreynol | Remove two obsolete versions of MBQI.
|
commit | commitdiff | tree |
| 2014-11-13 |
ajreynol | More preparation for filtering relevant terms in TermDb.
|
commit | commitdiff | tree |
| 2014-11-11 |
ajreynol | Work on synchronizing decision=justification and E...
|
commit | commitdiff | tree |
| 2014-11-10 |
ajreynol | Do not eliminate variables only occurring in patterns...
|
commit | commitdiff | tree |
| 2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression.
|
commit | commitdiff | tree |
| 2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup...
|
commit | commitdiff | tree |
| 2014-11-07 |
ajreynol | Enable --quant-cf by default. Fix bug in qcf for mixed...
|
commit | commitdiff | tree |
| 2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in...
|
commit | commitdiff | tree |
| 2014-11-06 |
ajreynol | Minor fix for getInstCons
|
commit | commitdiff | tree |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes...
|
commit | commitdiff | tree |
| 2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.
|
commit | commitdiff | tree |
| 2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug...
|
commit | commitdiff | tree |
| 2014-11-01 |
ajreynol | Fix cegqi for synthesis without syntax.
|
commit | commitdiff | tree |
| 2014-11-01 |
ajreynol | Simplify which lemmas to communicate in dt.
|
commit | commitdiff | tree |
| 2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma...
|
commit | commitdiff | tree |
| 2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,...
|
commit | commitdiff | tree |
| 2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ...
|
commit | commitdiff | tree |
| 2014-10-28 |
ajreynol | Preprocessing step for finding finite runs of well...
|
commit | commitdiff | tree |
| 2014-10-28 |
ajreynol | Initial infrastructure for function definition quantifiers...
|
commit | commitdiff | tree |
| 2014-10-28 |
ajreynol | Improve stats in conjecture generator, minor cleanup.
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search