Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
fix getModelValue(<non-preregistered term>)
|
|
|
|
|
|
|
|
|
|
|
|
Sticksel for the report.
|
|
Christoph Sticksel for reporting these.
|
|
ground terms).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
disabling codatatype reasoning. Minor cleanup.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
minimal instantiation level.
|
|
based on ground equalities. Add filtering options to options file.
|
|
|
|
quantifiers check. Minor fix for conjecture generation.
|
|
|
|
|
|
Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
|
|
changes for relevant term filtering.
|
|
values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation. Print --dump-instantiations on sat/unknown.
|
|
inst-level attribute to quant-inst-max-level
|