Z3 C API 中的指数约束未知？

Question

我想从 Z3 C API 中获取以下约束的解决方案：

   2^x < a < 2^(x+1)

2^x 的表达式是：

    t_x=Z3_mk_power(ctx,two,x), two is the expression of "2";

    2^(x+1) is similar,

"a" 是一个 int const ，其值为 10：

   a=Z3_mk_int(ctx,10);

约束是：

   c1=Z3_mk_lt(ctx,t_x,a);

   c2=Z3_mk_lt(ctx,a,t_x_plus_one);

然后我得到模型是“未知的”，Z3 C API 不能得到这样的模型？

Answer 1

从描述中并不清楚Z3最终采用哪种求解方法，但一般非线性整数运算是不可判定的，Z3只能处理简单的指数情况。另请参阅 Leo 对类似问题的回答：

How does Z3 handle non-linear integer arithmetic?

Z3 supports for nonlinear arithmetics