| 2015-09-11 |
ajreynol | Minor cleanup related to codatatypes.
|
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Models for codatatypes. Fixes bug 662.
|
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Normalization of codatatype constants, codatatype now...
|
commit | commitdiff | tree |
| 2015-09-10 |
ajreynol | Fix bug 670. Minor.
|
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Fix bug in strings rewriter regarding lengths of substr...
|
commit | commitdiff | tree |
| 2015-09-09 |
ajreynol | Working towards a fair enumerator for codatatypes.
|
commit | commitdiff | tree |
| 2015-09-06 |
ajreynol | Improve quantifiers rewriter, minor refactoring.
|
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Working fix for bugs 610 and 643 regarding check-model...
|
commit | commitdiff | tree |
| 2015-09-05 |
ajreynol | Fix bugs related to fmf with incremental. Reinitialize...
|
commit | commitdiff | tree |
| 2015-09-04 |
ajreynol | Fix bugs 605 and 667.
|
commit | commitdiff | tree |
| 2015-08-30 |
ajreynol | Minor improvement to sygus sol reconstruction.
|
commit | commitdiff | tree |
| 2015-08-28 |
ajreynol | Improvements to sygus, register equivalent terms based...
|
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Do ITE term bookkeeping when solving Sygus inputs....
|
commit | commitdiff | tree |
| 2015-08-27 |
ajreynol | Modify slow regressions.
|
commit | commitdiff | tree |
| 2015-08-26 |
ajreynol | Minor improvements to cbqi, fix bug in solving with...
|
commit | commitdiff | tree |
| 2015-08-25 |
ajreynol | Use zero in cbqi when not using infinities.
|
commit | commitdiff | tree |
| 2015-08-24 |
ajreynol | Improvements to vts in cbqi, bug fix vts for non-atomic...
|
commit | commitdiff | tree |
| 2015-08-21 |
ajreynol | Minor changes related to codatatypes for 1.5 release.
|
commit | commitdiff | tree |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for...
|
commit | commitdiff | tree |
| 2015-08-19 |
ajreynol | Make cbqi robust to term ITE removal. Separate vts...
|
commit | commitdiff | tree |
| 2015-08-19 |
ajreynol | Implementation of model-based projection in cbqi, cleanup...
|
commit | commitdiff | tree |
| 2015-08-16 |
ajreynol | More optimizations to --macros-quant, add --macros...
|
commit | commitdiff | tree |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split...
|
commit | commitdiff | tree |
| 2015-08-01 |
ajreynol | Simplification/improvement to solving deltas in LRA...
|
commit | commitdiff | tree |
| 2015-08-01 |
ajreynol | Support for default grammar for datatypes in sygus...
|
commit | commitdiff | tree |
| 2015-07-31 |
ajreynol | Make --fmf-fun and --macros-quant work in incremental...
|
commit | commitdiff | tree |
| 2015-07-31 |
ajreynol | Sygus support for inductive datatypes.
|
commit | commitdiff | tree |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested...
|
commit | commitdiff | tree |
| 2015-07-25 |
ajreynol | Add option --sygus-inv-templ for synthesizing strengthening...
|
commit | commitdiff | tree |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch.
|
commit | commitdiff | tree |
| 2015-07-12 |
ajreynol | Add option --full-saturate-quant-rd. Fix option -...
|
commit | commitdiff | tree |
| 2015-07-05 |
ajreynol | Add options --partial-triggers, --elim-taut-quant,...
|
commit | commitdiff | tree |
| 2015-07-02 |
ajreynol | On-demand upper bound lemmas for deltas in quantified...
|
commit | commitdiff | tree |
| 2015-07-01 |
ajreynol | Add options --qcf-all-conflict, --ite-dtt-split-quant...
|
commit | commitdiff | tree |
| 2015-06-29 |
ajreynol | Module to infer alpha equivalence of quantified formulas...
|
commit | commitdiff | tree |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modules...
|
commit | commitdiff | tree |
| 2015-06-25 |
ajreynol | Do not assert fail for fmf empty domains. Fixes bug...
|
commit | commitdiff | tree |
| 2015-06-22 |
ajreynol | Add --user-pat=interleave. Remove unused lte inst strategy.
|
commit | commitdiff | tree |
| 2015-06-16 |
ajreynol | Avoid completion for large finite types. Fix bug for...
|
commit | commitdiff | tree |
| 2015-06-15 |
ajreynol | Make array basis term a skolem (avoids crashing in...
|
commit | commitdiff | tree |
| 2015-06-13 |
ajreynol | Robust check to avoid store all instantiations. Fix...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search