| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
|
|
default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
|
|
Start grammar. Add regression.
|
|
Add regression.
|
|
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
|
|
within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
fmf mbqi=gen-ev for interpreted operators.
|
|
--fmf-fun.
|
|
|
|
(mostly whitespace differences).
|
|
Morgan's proof branch).
|
|
Parser dont tokenize
|
|
|
|
|
|
|
|
|
|
https://www.starexec.org/starexec/secure/details/job.jsp?id=6972
The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.
|
|
|
|
|
|
simplification.
|
|
|
|
|
|
signature. Add regressions.
|
|
regressions.
|
|
|
|
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
|
|
|
