Dreal4 Forall() SMT

Question

I would like to use the Dreal4 SMT solver to check the following condition of a control lyapunov function:

there exists a u contained with in the set U for all x contained within the set X for which V(x,u) is negative. (I am calling V(x,u) the lie derivative of the V(x) for those familiar with CLFs).

I believe I should be able to solve this problem using the forall() function call (although I cant seem to find an exists() in the documentation), but I am not understanding the syntax of the forall function.

Simple example:

we will say x is bounded by the interval : [-5,5]and u [-25,25]

def V(x,u):
    return (x**2) - 1 + u
problem = forall([x], And(V(x,u) < 0, x < 5, x > -5, u > -25, u < 25)
result = CheckSatisfiablitity(problem,0.01)

This should be verified correct based on the above condition since for every x you can chose a u that will make the function negative. Regardless of the u boundrys I set (even when I set to values that would result in the function not being able to be made negative everywhere) I just get a None return.

It seems I dont understand the forall() function syntax, How should I use the forall() function to verify this condition?

Answer 1

dReal uses the notion of delta-satisfiability; which isn't quite what you want here. Also, it models real values by machine floats; which is sufficient for many practical applications but isn't mathematically sound to use when you want to prove theorems like this.

I'm not sure how one would go about proving this in dReal, but in z3, you'd code it as follows:

from z3 import *

def V(x, u):
    return (x**2) - 1 + u

x = Real('x')
u = Real('u')

prove(ForAll([x], Implies(And(x < 5, x > -5),
                          Exists([u], And(u > -25, u < 25, V(x, u) < 0)))))

Note the use of nested quantifiers, which matches your problem definition. This prints:

proved

If you do have to use dReal for some other reason, I recommend asking at https://github.com/dreal/dreal4/issues where they might have better advice for you. Please post back here what you find out!

Getting a model

Note that z3 (and SMT solvers in general) do not display values of quantified variables in models. To get the value, you need to make it a top-level declared variable instead. To do this, we declare a solver and assert the negation of what we want to "prove." So, you'd code it as follows:

from z3 import *

def V(x, u):
    return (x**2) - 1 + u

x = Real('x')
u = Real('u')

s = Solver()
s.add(x < 5)
s.add(x > -5)

# Add the negation of what we want to prove
s.add(Not(Exists([u], And(u > -20, u < 25, V(x, u) < 0))))

r = s.check()
if r == sat:
    print("Counter-example:")
    print(s.model())
else:
    print("Solver said: ", r)

This prints:

Counter-example:
[x = 19/4]