| 2015-06-13 |
ajreynol | Disable sort inference for SMT COMP
|
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Fix for sort inference involving mixed Int/Real equalities.
|
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Avoid instantiating with array constants.
|
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Ensure mkRep instantiation strategies do not violate...
|
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Fix crash in non-linear cbqi.
|
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Make sygus an output language. Parse declare-fun in...
|
commit | commitdiff | tree |
| 2015-06-12 |
ajreynol | Accelerate sygus solution reconstruction for constants...
|
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Avoid naming conflicts in sygus, refactor. Add missing...
|
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Handle duplicate operators in sygus grammars. Parse...
|
commit | commitdiff | tree |
| 2015-06-11 |
ajreynol | Update experimental scripts. Support top-level non...
|
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Bug fix parsing constant constructor sygus.
|
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Support for printing solutions involving LetGTerm sygus...
|
commit | commitdiff | tree |
| 2015-06-10 |
ajreynol | Parse support for sygus LetGTerm.
|
commit | commitdiff | tree |
| 2015-06-09 |
ajreynol | Bug fix instantiations for fmf-bound-int. Disable...
|
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Fix for last commit.
|
commit | commitdiff | tree |
| 2015-06-04 |
ajreynol | Minor changes to smt comp script for quantified arith...
|
commit | commitdiff | tree |
| 2015-06-03 |
ajreynol | Refactoring of sygus parsing, properly parse Constant...
|
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Flatten sygus grammars during parsing. Remove duplicate...
|
commit | commitdiff | tree |
| 2015-06-02 |
ajreynol | Add casc 25 tfn script. Change tff script to output...
|
commit | commitdiff | tree |
| 2015-06-01 |
ajreynol | When proof enabled, disable uf sym break. Add regression.
|
commit | commitdiff | tree |
| 2015-05-29 |
ajreynol | Do not enforce dt fairness when single invocation sygus.
|
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Add missing regression
|
commit | commitdiff | tree |
| 2015-05-25 |
ajreynol | Bug fix for CNF proofs (and/or case 1), thanks to Alain...
|
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Fixes related to cbqi + E-matching.
|
commit | commitdiff | tree |
| 2015-05-15 |
ajreynol | Avoid ensureLiteral on unpreprocessed formulas in cbqi.
|
commit | commitdiff | tree |
| 2015-05-13 |
ajreynol | Refactor interface for incompleteness in quantifiers...
|
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Allow sygus with no syntactic restrictions for LIA...
|
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Add missing regression.
|
commit | commitdiff | tree |
| 2015-05-11 |
ajreynol | Support for arbitrary constants/variables in Sygus...
|
commit | commitdiff | tree |
| 2015-05-10 |
ajreynol | Minor improvements to infrastructure. Minor changes...
|
commit | commitdiff | tree |
| 2015-05-08 |
ajreynol | Add casc25 fnt script.
|
commit | commitdiff | tree |
| 2015-05-02 |
ajreynol | Minor fix for corner cases of fmf-fun, fix for --dt...
|
commit | commitdiff | tree |
| 2015-04-28 |
ajreynol | Fix smt2 printing of fun-def. Simplification of mbqi...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search