I'm trying to learn how to write code for giving a counterexample to a horn clause and it's guessed interpretation. In the below code, let I be the uninterpreted function (it's a trivial loop invariant). The first 3 s.add() add the condition requirements for I(x), and the fourth one is a guess candidate for I. I try to use the s.prove directive to get a counterexample to my guessed candidate for I. I seem to be getting a huge error log on running this code, could anyone tell me what's wrong?
s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort())
x, x2 = Ints('x x2')
s.set("produce-proofs", True)
s.add( ForAll( [x] ,Implies( x == 0 , I(x))) )
s.add( ForAll( [x, x2] , Implies ( And( I(x), x2 == x + 1 , x < 5) , I(x2) ) ) )
s.add( ForAll( [x] ,Implies( And( I(x), Not(x < 5) ) , x == 5 ) ) )
s.add( ForAll( [x], And( Implies( I(x) , (x == 2) ), Implies( (x == 2) , I(x) ) ) ) ) #Adding guessed invariant here!
assert unsat == s.check()
print(s.proof())
You've a couple of mistakes in the script; perhaps this dates back from a while ago with a different version of z3? In any case, the following goes through with z3 version 4.8.14:
from z3 import *
s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort())
x, x2 = Ints('x x2')
s.set("proof", True)
s.add( ForAll( [x] ,Implies( x == 0 , I(x))) )
s.add( ForAll( [x, x2] , Implies ( And( I(x), x2 == x + 1 , x < 5) , I(x2) ) ) )
s.add( ForAll( [x] ,Implies( And( I(x), Not(x < 5) ) , x == 5 ) ) )
s.add( ForAll( [x], And( Implies( I(x) , (x == 2) ), Implies( (x == 2) , I(x) ) ) ) ) #Adding guessed invariant here!
print(s.check())
Unfortunately it prints:
unknown
This means the solver wasn't able to determine if the input is satisfiable or not; it gave up and said unknown. An earlier version of the solver might've been able to solve this successfully, providing an unsatisfiability proof, or a model should it be satisfiable.
I recommend tracking down where you got this example from and find out which version of z3 they were using. Going back to that version might help you make progress. Or, if you think the problem should be solvable as is, you can file a bug report at https://github.com/Z3Prover/z3/issues