| 2016-02-23 |
ajreynol | Fix term database for non-equal, congruent terms in...
|
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Fixes and improvements for datatypes properties and...
|
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas...
|
commit | commitdiff | tree |
| 2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for...
|
commit | commitdiff | tree |
| 2016-02-17 |
ajreynol | Refactor quantifiers attributes. Make quantifier elimination...
|
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | Public interface for quantifier elimination. Minor...
|
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | More simplification to internal implementation of tuples...
|
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Minor change to last commit
|
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastructure...
|
commit | commitdiff | tree |
| 2016-02-11 |
ajreynol | More aggressive conditional rewriting for quantified...
|
commit | commitdiff | tree |
| 2016-02-10 |
ajreynol | Fix model postprocessor for tuples, add regression.
|
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Fix regression, minor change to output.
|
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Eager introduction of eqc, lemma cache for ground fmf...
|
commit | commitdiff | tree |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatypes...
|
commit | commitdiff | tree |
| 2016-02-05 |
ajreynol | Add two optimizations for datatypes, currently disabled...
|
commit | commitdiff | tree |
| 2016-02-01 |
ajreynol | Simplify fmc model construction, add regression. Improve...
|
commit | commitdiff | tree |
| 2016-01-20 |
ajreynol | Fix bug in fmc mbqi where modelscomputed for mbqi could...
|
commit | commitdiff | tree |
| 2016-01-19 |
ajreynol | Bug fixes for model construction with codatatypes,...
|
commit | commitdiff | tree |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs.
|
commit | commitdiff | tree |
| 2016-01-15 |
ajreynol | Type enumerators take optional argument indicating...
|
commit | commitdiff | tree |
| 2016-01-14 |
ajreynol | Ensure model construction for parametric sorts involving...
|
commit | commitdiff | tree |
| 2016-01-13 |
ajreynol | Lemma cache datatypes. Do not send true lemma in quantifiers...
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix uf-ss-totality.
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involving...
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix for cbqi, do not use model values for terms...
|
commit | commitdiff | tree |
| 2015-12-17 |
ajreynol | Minor
|
commit | commitdiff | tree |
| 2015-12-16 |
ajreynol | Work on purification for quantifiers, minor updates.
|
commit | commitdiff | tree |
| 2015-12-15 |
ajreynol | Add option uf-ss-fair-monotone. Minor cleanup and improvemen...
|
commit | commitdiff | tree |
| 2015-12-10 |
ajreynol | Add option fmf-empty-sorts.
|
commit | commitdiff | tree |
| 2015-12-02 |
ajreynol | Minor fixes for cegqi-si-partial.
|
commit | commitdiff | tree |
| 2015-12-01 |
ajreynol | More work on --cegqi-si-partial, incomplete.
|
commit | commitdiff | tree |
| 2015-11-28 |
ajreynol | Initial work on --cegqi-si-partial, refactoring.
|
commit | commitdiff | tree |
| 2015-11-26 |
ajreynol | Update to new implementation of single invocation partition...
|
commit | commitdiff | tree |
| 2015-11-26 |
ajreynol | Front-end support for get-value of sort cardinality...
|
commit | commitdiff | tree |
| 2015-11-25 |
ajreynol | Infrastructure for partially single invocation properties...
|
commit | commitdiff | tree |
| 2015-11-18 |
ajreynol | Option for midpoints in cbqi.
|
commit | commitdiff | tree |
| 2015-11-17 |
ajreynol | Improve relevant domain computation for arithmetic...
|
commit | commitdiff | tree |
| 2015-11-12 |
ajreynol | Minor fixes and improvements to purify quant, relational...
|
commit | commitdiff | tree |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checking...
|
commit | commitdiff | tree |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes...
|
commit | commitdiff | tree |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifiers...
|
commit | commitdiff | tree |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers.
|
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Promote InstStrategyCbqi to quantifier module. Cleanup...
|
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended...
|
commit | commitdiff | tree |
| 2015-10-24 |
ajreynol | Fixes related to string contains.
|
commit | commitdiff | tree |
| 2015-10-22 |
ajreynol | Enable counterexample-guided quantifier instantiation...
|
commit | commitdiff | tree |
| 2015-10-21 |
ajreynol | Minor refactoring in strings related to length.
|
commit | commitdiff | tree |
| 2015-10-20 |
ajreynol | Refactor strings, remove old cycle checks in normalize...
|
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Clean up explanations involving string length. Add...
|
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Improve stratification of strings extended function...
|
commit | commitdiff | tree |
| 2015-10-19 |
ajreynol | Improve regexp rewriter, simplify regexp preprocess...
|
commit | commitdiff | tree |
| 2015-10-18 |
ajreynol | Fix for no condense func values.
|
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Add option to interleave enumerative instantiation...
|
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Throw error for recursively defined types involving...
|
commit | commitdiff | tree |
| 2015-10-16 |
ajreynol | Fix for codatatype constant rewrite, add regression.
|
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Fix congruence check in strings, fixes bug 686.
|
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Change semantics of str.substr to allow endpoint out...
|
commit | commitdiff | tree |
| 2015-10-15 |
ajreynol | Decompose string contains, minor refactoring.
|
commit | commitdiff | tree |
| 2015-10-11 |
ajreynol | Fix strings preprocessing + incremental, fixes bug...
|
commit | commitdiff | tree |
| 2015-10-08 |
ajreynol | Minor improvements to strings. Refactor rewriter. Enable...
|
commit | commitdiff | tree |
| 2015-10-07 |
ajreynol | Minor improvements, add endpoint eq inference to strings.
|
commit | commitdiff | tree |
| 2015-10-06 |
ajreynol | More improvements to strings rewriter for regexps,...
|
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Fixes related to explanations for cycles, sym inferences...
|
commit | commitdiff | tree |
| 2015-10-02 |
ajreynol | Improvements to rewriter for regexp, contains, indexof...
|
commit | commitdiff | tree |
| 2015-10-01 |
ajreynol | Evaluate extended operators on partially concrete arguments...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search