1

I am trying to solve constraints in an if or while statement by using Z3py. As Z3py expects expressions like True, False or Z3py-Boolean expression, I had to work out how I can convert the constraints which are just strings into the correct form.
I found this topic, z3python: converting string to expression, which says you should use "eval".
Now, simplified, what I am doing is the following:

a = Real("a")
constr = "a < 1000"
ds = eval(constr)
print(ds)
solve(ds)

This nicely prints out:

real_a < 1000

[real_a = 0]

Now I also want to solve the negation of this constraint, which is:

constr = "not(a < 1000)"

The result of this is:

False

no solution

I honestly do not understand why this result shows up. I expected that the whole expression inside "not" is inverted and therefore the solution would be something like "a = 1000". But this is obviously not the case.
Now my question is: What exactly happens there that this result occurs? And, even more important: How can I fix this? Is there a workaround?
I am aware I could just change every < in >=, ever > in <=, every and in or and the other way round, remove every not and so on. But this looks like a lot of work and I first want to make sure there is no other way.

Community
  • 1
  • 1
M0rgenstern
  • 411
  • 1
  • 6
  • 18
  • what is the value of `a`? – Padraic Cunningham Aug 02 '14 at 18:01
  • Well, a has no value at all. That would also make no sense. Because then eval would just replace the variable with its value and return True or False. But what I need is a string which can be used as a constraint which Z3py should solve. And therefore the variable for which I want to know the value has to stay in the constraint as it is. – M0rgenstern Aug 02 '14 at 18:18

0 Answers0