| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
solution reconstruction.
|
|
unconstrained functions in sygus solver.
|
|
|
|
|
|
strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.
|
|
|
|
|
|
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.
|
|
|
|
module. Add heuristics for cbqi LIA instantiation with coefficients.
|
|
of term database, other refactoring. Bug fixes for cbqi+datatypes.
|
|
liberal.
|
|
|
|
quantified formulas with non-constant polarity.
|
|
|
|
report. Other minor cleanup.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
Enable redundant ITE branch elimination in quantifiers rewriter.
|
|
|
|
|
|
Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
|
|
for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
|
|
datatypes.
|
|
|
|
|
|
|
