如何使用z3 C++ API將常量聲明爲獨特

Question

舉例： context ctx;

sort type1 = ctx.int_sort(); 
sort type2 = ctx.bool_sort(); 

func_decl b1 = function("b1", type1, type2); 

expr x = ctx.int_const("x"); 
expr y = ctx.int_const("y"); 
expr z = ctx.int_const("z"); 

solver s(ctx); 
s.add(b1(x)); 
s.add(b1(y)); 
s.add(b1(z)); 

一個如何聲明的x，y和z比使用作爲不同的其他： s.add（未（X == y或x ==ž或y == Z））; ？

謝謝。

Answer 1

Z3支持distinct函數，該函數在C++中的版本爲。