You should use (assert (distinct x y))
instead of (distinct x y)
.
Here is a link to the updated example: http://rise4fun.com/Z3/uVrX
Z3 / SMTLIB2 support for `distinct`
Domanda
I've been using the (ML) z3 bindings for a while, and the API function
val mk_distinct : context -> ast array -> ast
has served faithfully for many years. Am now trying to switch
to the SMTLIB2 interface, but I find that the distinct
command
is unsupported
. For example, the query:
(declare-fun x () Int)
(declare-fun y () Int)
(distinct x y)
(assert (= x y))
(check-sat)
yields the response:
unsupported
; distinct
sat
on the web-demo. Is there some workaround?
Thanks!
Ranjit.
Soluzione
Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow