| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
report. Other minor cleanup.
|
|
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.
|
|
|
|
for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
|
|
soundness bug in strings related to explaining length terms.
|
|
pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.
|
|
|
|
|
|
--ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence. Update casc 25 FOF script.
|
|
options.
|
|
default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
|
|
|
|
|
|
|
|
for non-UF logics. Update SMT COMP scripts accordingly.
|
|
|
|
|
|
|
|
for sygus.
|
|
tff script. Minor additions to sygus.
|
|
|
|
fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
|
|
|
|
fun-def. Add skolemization options.
|
|
|
|
|
|
syntax for single inv properties.
|
|
quantifiers module. Refactor QuantifiersEngine registration and check.
|
|
refactor of previous commit.
|
|
quantifiers check for sat.
|
|
inside splitting lemmas for sygus.
|
|
|
