Age | Commit message (Collapse) | Author |
|
incomplete for fmc.
|
|
|
|
|
|
enumerator and codatatype rewriter, further simplify fmc.
|
|
|
|
|
|
values. Add regression.
|
|
|
|
|
|
respect cardinality bounds on when finite model finding is enabled.
|
|
|
|
sorts when finite model finding is enabled, add regressions.
|
|
sorts.
|
|
unconstrained functions in sygus solver.
|
|
|
|
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
|
|
|
|
|
|
restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
|
|
|
|
|
|
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
|
|
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
|
|
|
|
regressions. Eliminate preprocess for regexp.
|
|
|
|
|
|
|
|
infrastructure for str.contains inferences.
|
|
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.
|
|
fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.
|
|
regressions.
|
|
|
|
|
|
|
|
in strings. Other improvements.
|
|
eagerly, only process contains/memberships that have non-constant arguments. Cleanup.
|
|
bug 613.
|
|
of term database, other refactoring. Bug fixes for cbqi+datatypes.
|
|
liberal.
|
|
quantified formulas with non-constant polarity.
|
|
report. Other minor cleanup.
|
|
|
|
|
|
bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
|
|
|
|
|
|
|
|
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.
|
|
Enable redundant ITE branch elimination in quantifiers rewriter.
|