1

I am using th z3 C++ API. if I create this simple false expression:

z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);

and try to solve, I get an unknown outcome. I am not an expert of strategies and tactics, but I am sure that z3 can solve this, if I use the right tactic.

I also tried

z3::expr p = !z3::forall(x, x==0);

with, of course, the same runknown esult.

Cœur
  • 37,241
  • 25
  • 195
  • 267
Giacomo Tagliabue
  • 1,679
  • 2
  • 15
  • 31
  • 1
    See the related question: http://stackoverflow.com/questions/14988298/what-are-the-limits-of-reasoning-in-quantified-arithmetic-in-smt – Leonardo de Moura Apr 18 '13 at 22:39

1 Answers1

0

I'm not familiar with z3, but from a general C++ perspective, wouldn't x==0 evaluate first, i.e. wouldn't your call be equivalent to implies(x, 1)? From a quick search it seems you may have to construct each piece of the statement as a z3 object, for example:

Z3_ast consequent = Z3_mk_eq(ctx, x, 0);
Z3_ast theorem = Z3_mk_implies(ctx, x, consequent);

But the above is not correct, either. I believe the parameters x and 0 themselves have to be instances of Z3_ast that encapsulate the statement you mean (as opposed to their interpolated values or references).

Andrew Cheong
  • 29,362
  • 15
  • 90
  • 145
  • That's not true, it is a valid z3 construct. If I substitute the forall with an exists, it solves to true, as one expects. maybe you got confused because i wrote the expression badly, sorry. I updated it now. – Giacomo Tagliabue Apr 18 '13 at 22:14
  • Hm, it's probable that indeed I'm mistaken. But are you saying that z3 overloads C++'s `==` operator, then, produce a statement out of `x==0`, instead of evaluating it? – Andrew Cheong Apr 18 '13 at 23:52
  • exactly, the C++ apis do that ;) it overrides pretty much everything – Giacomo Tagliabue Apr 19 '13 at 01:46