Search code examples
z3z3pyquantifiersforall

Bounding universally quantified variable

I would like to know if it is possible to bound the range of values of a universally quantified variable in Z3.

For example, let's assume that I have a variable of type Real called "time" which is used to model the time in the system. Let's say that I have an assertion which says that the value of some unary function "func1" shall always be between 1 and 100. The function takes the input the time variable. Expressed in Z3, I have encoded the property as following:

  1. ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

    Please note that I explicitly need the time variable to be universally quantified, because I want the Z3 go give me unsat if I inject property of following type:

  2. Exists(time, func1(time) == 101)

    As far as my understanding goes for Z3, all the constants have mathematical (theoretical) and not computer (practical) implementation i.e. their values are not bound (unfortunately I cannot point to the resource where I have read this at the moment). Assume that with time I model time in my systems, and according to the system constrains it cannot run for more than x hours, which I can use and say that value of time is between 0 and x*60'*60 to give the maximum execution time in seconds. I know that I can assert the allowed values for time with the following assertion:

  3. And(time >= 0, time <= x*60*60)

    but will it affect the universal quantification given in 1?

Consequently, this should lead to a situation where if property 2 is injected and for value of time I specify x*60*60 + 1, it should not be unset since the ForAll is valid only for the values of time.

Solution

  • but will it affect the universal quantification given in 1)?

    Note that 

    ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

    treats the variable "time" as bound. The formula has the same meaning as:

    ForAll(xx, And(func1(xx) >= 1, func1(xx) <= 100))

    When you assert the above, the meaning is that any instantiation of xx holds (is asserted). In particular, you can instantiate the quantified variable with the free variable "time" and in particular, you can instantiate with x*60*60+1 producing the assertion:

     And(func1(x*60*60+1) >= 1, func1(x*60*60+1) <= 100)

    Suppose you wanted to say that 

     And(func1(xx) >= 1, func1(xx) <= 100))

    holds for every value xx between 0 and x*60*60, then you can write:

    ForAll(xx, Implies(And(xx >= 0, xx <= x*60*60), And(func1(xx) >= 1, func1(xx) <= 100)))

    (unfortunately I cannot point to the resource where I have read this at the moment).

    Reasonable logic text books or foundations of computer science books should explain this in depth. Z3 supports a standard first-order many-sorted logic (with background theories).