1

I want to get the solution from Z3 C API for the constraint followed:

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

expression for 2^x is :

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

    2^(x+1) is similar,

"a" is a int const ,which value is 10:

   a=Z3_mk_int(ctx,10);

the constraints are:

   c1=Z3_mk_lt(ctx,t_x,a);

   c2=Z3_mk_lt(ctx,a,t_x_plus_one);

then I get the model is "unknown", Z3 C API cannot get a model like this?

user2940648
  • 72
  • 8

1 Answers1

0

From the description it's not clear which solving method Z3 employs in the end, but in general non-linear integer arithmetic is undecidable and Z3 can only handle simple cases of exponentials. See also Leo's answers to similar questions:

How does Z3 handle non-linear integer arithmetic?

Z3 supports for nonlinear arithmetics

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • I wrote the constraint wrong the last time, and I edited again , this one is clear. I read Leo's answer first. thanks. – user2940648 Apr 16 '14 at 10:13