[YICES-HELP] "distinct" predicate
erkokl at gmail.com
Wed May 16 13:16:47 PDT 2007
Is there a "distinct" predicate supported by Yices's own input
language, similar to that of SMT-Lib? Or is this predicate "compiled
away" when Yices reads SMT-Lib inputs?
Since compiling "distinct" away causes the generation of a quadratic
number of inequations, we were thinking Yices might have a custom
predicate for this purpose. If that is the case, is it possible to
access it from Yices's own input language?
More information about the YICES-HELP