| Age | Commit message (Collapse) | Author |
|---|
|
--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.
|
|
|
|
|
|
|
|
|
|
|
|
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
|
|
|
|
for non-UF logics. Update SMT COMP scripts accordingly.
|
|
|
|
|
|
|
|
testing purposes
|
|
|
|
|
|
|
|
|
|
--cbqi-sat whether to disable sat for quantified arith.
|
|
|
|
|
|
|
|
towards parsing non-flattened sygus grammars.
|
|
|
|
|
|
|
|
tff script. Minor additions to sygus.
|
|
|
|
competition scripts (in progress).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
present.
|
|
|
|
|
|
Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
StarExec infrastructure for testing.
|
