如何使用 z3 c++ API 将常量声明为不同的

【问题标题】：How to declare constants as distinct using the z3 c++ API如何使用 z3 c++ API 将常量声明为不同的
【发布时间】：2015-01-27 00:18:10
【问题描述】：

例如：上下文 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(not(x==y or x==z or y==z)); ?

谢谢。

【问题讨论】：

标签： c++ api z3

【解决方案1】：

Z3 支持distinct 函数，该函数在C++ 中为expr expr::distinct(expr_vector const & args)。

【讨论】：

感谢您的回复。您能否举一个与我之前的示例相关的用法示例？
假设 v 是一个包含 x、y、z 的 ast_vector，则 expr c = distinct(v);创建一个描述 x、y、z 必须不同的约束。
好的。谢谢。例如：expr_vector v(ctx)； v.push_back(x); v.push_back(y); expr c=distinct(v);
与我之前的示例相关，如果我们希望以交互方式将函数 b1 给定的值赋给某个特殊常量（通过读取常量并通过 b1 搜索其值，例如：std: :cin >>constante; std::cout
它应该是一个 int，因为 b1 接受一个 int 并返回一个 bool。