Question about Skolem/Prenex normal form with SNF tactic

alebugariu commented 4 years ago

I would have a question about the SNF tactic. For the following formula:

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)

(declare-fun f (Int) Bool)
(declare-fun g (Int Int) Bool)

(assert (forall ((x Int))
    (! (=> (f x)
           (not (exists ((y Int)) (! (g x y) :pattern ( (g x y) )))))
       :pattern ( (f x) ))))
(apply (using-params snf :mode quantifiers))

I was expecting the get a formula in prenex normal form (with all the quantifiers at the beginning) and with only universal quantifiers. The output produced by the SNF tactic with mode quantifiers is:

(goals
(goal
  (forall ((x Int))
    (! (or (not (f x)) (forall ((y Int)) (! (not (g x y)) :pattern ((g x y)))))
       :pattern ((f x))))
  :precision precise :depth 1)
)

which is a formula in negation normal form.

Is this the expected output of the SNF tactic? Or are there any parameters that I should have set to obtain an output in prenex normal form?

Thank you very much for your help.

NikolajBjorner commented 4 years ago

we don't have a prenex normal form conversion exposed.

panda2134 commented 2 years ago

Sorry for commenting on this old discussion, but if we look at the definition of Skolem normal form, wouldn't it be a requirement that the output is in prenex normal form?

Z3Prover / z3

Question about Skolem/Prenex normal form with SNF tactic #4051