Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?

Question

Suppose I have the following CHC system (I(x) is an unkown predicate):

(x = 0) -> I(x) 

(x < 5) /\ I(x) /\ (x' = x + 1) -> I(x') 

I(x) /\ (x >= 5) -> x = 5

Now suppose I guess a solution for I(x) as x < 2 (actually an incorrect guess). Can I write code for Z3Py to (i) check if it is a valid solution and (ii) if it's incorrect find a counterexample, i.e. a value which satisfies x < 2 but does not satisfy atleast one of the above 3 equations? (For eg: x = 1, is a counterexample as it does not satisfy the 2nd equation?)

Answer 1

Sure. The way to do this sort of reasoning is to assert the negation of the conjunction of all your constraints, and ask z3 if it can satisfy it. If the negation comes back satisfiable, then you have a counter-example. If it is unsat, then you know that your invariant is good.

Here's one way to code this idea, in a generic way, parameterized by the constraint generator and the guessed invariant:

from z3 import *

def Check(mkConstraints, I):
    s = Solver()

    # Add the negation of the conjunction of constraints
    s.add(Not(mkConstraints(I)))

    r = s.check()
    if r == sat:
        print("Not a valid invariant. Counter-example:")
        print(s.model())
    elif r == unsat:
        print("Invariant is valid")
    else:
        print("Solver said: %s" % r)

Given this, we can code up your particular case in a function:

def System(I):
    x, xp = Ints('x xp')

    # (x = 0) -> I(x)
    c1 = Implies(x == 0, I(x))

    # (x < 5) /\ I(x) /\ (x' = x + 1) -> I(x')
    c2 = Implies(And(x < 5, I(x), xp == x+1), I(xp))

    # I(x) /\ (x >= 5) -> x = 5
    c3 = Implies(And(I(x), x >= 5), x == 5)

    return And(c1, c2, c3)

Now we can query it:

Check(System, lambda x: x < 2)

The above prints:

Not a valid invariant. Counter-example:
[xp = 2, x = 1]

showing that x=1 violates the constraints. (You can code so that it tells you exactly which constraint is violated as well, but I digress.)

What happens if you provide a valid solution? Let's see:

Check(System, lambda x: x <= 5)

and this prints:

Invariant is valid

Note that we didn't need any quantifiers, as top-level variables act as existentials in z3 and all we needed to do was to find if there's an assignment that violated the constraints.