| Age | Commit message (Collapse) | Author |
|---|
|
appears to be source of crashes on mac
|
|
|
|
infrastructure for str.contains inferences.
|
|
multiple sorts in UF finite model finding by default.
|
|
|
|
|
|
replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.
|
|
improvements.
|
|
fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.
|
|
rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms.
|
|
reductions based on congruence, precheck for cycles.
|
|
|
|
regressions.
|
|
|
|
|
|
|
|
in strings. Other improvements.
|
|
eagerly, only process contains/memberships that have non-constant arguments. Cleanup.
|
|
bug 613.
|
|
module. Add heuristics for cbqi LIA instantiation with coefficients.
|
|
of term database, other refactoring. Bug fixes for cbqi+datatypes.
|
|
liberal.
|
|
|
|
fix involves sets getModelValue handling the case when element theory
doesn't have model
|
|
|
|
|
|
quantified formulas with non-constant polarity.
|
|
|
|
report. Other minor cleanup.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
quantified formulas.
|
|
bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
|
|
|
|
|
|
|
|
|
|
original conjecture, set default invariant template mode to post-condition.
|
|
Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
|
|
for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.
|
|
|
|
|
|
|
|
|
|
symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
|
