Skolemization in Z3

Question

I am trying to remove existential quantifiers in my theory using Skolemization. This means that I replace existential quantifiers with functions that are parameterized by the universally quantified variables in the scope of the existential quantifiers.

Here I found an explanation how to do this in Z3, but I am still having troubles doing it. Suppose the following two functions:

(define-fun f1 ((t Int)) Bool (= t 3))
(define-fun f2 () Bool (exists ((t Int)) (f1 t)))

I believe that f2 should be true, because there exists an integer t such that (f1 t) is true, namely t=3. I apply Skolemization by introducing a constant for the existentially quantified formula:

(define-const c Int)

Then the formula with the existential quantifier is rewritten to:

(define-fun f2 () Bool (f1 c))

This does not work, that is, the constant c does not have the value 3. I suspect it is because we have not given an interpretation to the constant c, because if we add (assert (= c 3)) it works fine, but this takes away the whole idea of the existential quantifier. Is there a way in which I give a less explicit interpretation to c so that this will work?

Answer 1

So, I think you have it about right actually, here's the script I used with automatic (via Z3's SNF tactic) and manual (via adding the constant c) skolemization, which gave the value 3 in the model for the skolem constant as expected (smt-lib script: http://rise4fun.com/Z3/YJy2 ):

(define-fun f1 ((t Int)) Bool (= t 3))
(define-fun f2 () Bool (exists ((t Int)) (f1 t)))
(declare-const c Int)
(define-fun f2a () Bool (f1 c))

(push)
(assert f2)
(check-sat) ; sat
(get-model) ; model gives t!0 = 3 (automatic skolemization in Z3)
(pop)

(push)
(assert f2a)
(check-sat) ; sat
(get-model) ; model gives c = 3 after manual skolemization
(pop)

Also, note that Z3 has a Skolem normal form (SNF) conversion tactic built in, and here's an example in z3py (link to script: http://rise4fun.com/Z3Py/ZY2D ):

s = Solver()

f1 = Function('f1', IntSort(), BoolSort())
t = Int('t')
f2 = Exists(t, f1(t))
f1p = ForAll(t, f1(t) == (t == 3)) # expanded define-fun macro (define-fun f1 ((t Int)) Bool (= t 3))

s.add(f1p)
s.add(f2)

print f1p
print f2

print s.check()
print s.model() # model has skolem constant = 3

g = Goal()
g.add(f1p)
g.add(f2)
t = Tactic('snf') # use tactic to convert to SNF
res = t(g)
print res.as_expr()
s = Solver()
s.add( res.as_expr() )
print s.check()
print s.model() # model has skolem constant = 3