| 2015-10-01 |
ajreynol | More improvements to strings. More aggressive inference...
|
commit | commitdiff | tree |
| 2015-09-30 |
ajreynol | Refactor strings, bug fix inferences vs lemmas.
|
commit | commitdiff | tree |
| 2015-09-29 |
ajreynol | Fix for fmf+incremental. Restrict cbqi to literals...
|
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Improve quantifiers engine wrt incremental presolve...
|
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fix
|
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Minor fixes to strings, add regressions.
|
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Add missing regression
|
commit | commitdiff | tree |
| 2015-09-28 |
ajreynol | Fix bug for trivial extf inferences in strings. Improve...
|
commit | commitdiff | tree |
| 2015-09-27 |
ajreynol | Improved handling of extended operators. Do preprocess...
|
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Lazy preprocessing of extended operators in strings...
|
commit | commitdiff | tree |
| 2015-09-26 |
ajreynol | Better organization of quantifiers modules, promote...
|
commit | commitdiff | tree |
| 2015-09-25 |
ajreynol | Clear term caches for quantifiers + incremental, fixes...
|
commit | commitdiff | tree |
| 2015-09-24 |
ajreynol | Counterexample-guided instantiation for datatypes....
|
commit | commitdiff | tree |
| 2015-09-22 |
ajreynol | Improve ITE redundant branch elimination in quantifiers.
|
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | Fix bug in quantifiers engine where model construction...
|
commit | commitdiff | tree |
| 2015-09-18 |
ajreynol | More work mixing UF and sygus.
|
commit | commitdiff | tree |
| 2015-09-17 |
ajreynol | Allow most smt2 commands as sygus commands. Fix bug...
|
commit | commitdiff | tree |
| 2015-09-16 |
ajreynol | Add option --fmf-fun-rlv, remove deprecated option...
|
commit | commitdiff | tree |
| 2015-09-15 |
ajreynol | Fix bug related to quantifiers + incremental, thanks...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search