| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
--purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.
|
|
no macros-quant in incremental. Update casc TFN script.
|
|
--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.
|
|
|
|
|
|
|
|
|
|
|
|
improvements to robustness of sygus parsing.
|
|
Minor changes to sygus type registration. Print sygus let solutions assuming fixed variable names.
|
|
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
|
|
within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
|
|
|
|
for non-UF logics. Update SMT COMP scripts accordingly.
|
|
--cbqi-sat whether to disable sat for quantified arith.
|
|
|
|
|
|
|
|
|
|
for sygus.
|
|
|
|
|
|
tff script. Minor additions to sygus.
|
|
competition scripts (in progress).
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
delta lemmas.
|
|
|
|
and strings preprocessing. Minor fix for conjecture generation for finite types.
|
|
|
