| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
--full-saturate-quant.
|
|
inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
|
|
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
|
|
|
|
|
|
improvement to performance of E-matching.
|
|
assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
|
|
|
|
|
|
strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.
|
|
|
|
for cegqi.
|
|
mkRep for multi triggers.
|
|
|
