| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
|
|
sort inference and monotonicity. Minor cleanup.
|
|
|
|
especially for disequalities
|
|
|
|
|
|
|
|
|
|
|
|
sorts. Working on monotonicity inference.
|
|
|
|
|
|
|
|
to bounded integer quantifier instantiation.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some new functionality in substitutions.h/cpp
|
|
|
|
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
|
|
for faster compilation
|
|
|
|
|
|
|
|
|
|
some debug messages.
|
|
|
|
|
|
|
|
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
|
|
|
|
|
|
|
|
|
|
Brain for reporting this.
|
|
|
|
|
|
|
|
|
