search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.17k stars 1.47k forks source link

qe, qe2, and qe_rec incomplete for QBF solving #3674

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(declare-const v3 Bool)
(assert (not (forall ((q10 Bool) (q11 Bool) (q12 Bool)) v3)))
(check-sat-using (then simplify qe_rec))

The final (check-sat-using ...) returns "unknown".

After adding (get-info :reason-unknown), z3 b686bb61 returns (:reason-unknown "incomplete")

rainoftime commented 4 years ago

qe, qe2 also do not work

rainoftime commented 4 years ago

(check-sat) works. But by adding -v:15 or -v:100, I did not see information like "mbqi".

NikolajBjorner commented 4 years ago

the purpose of the "qe" tactics is to eliminate quantifiers and produce an equivalent quantifier-free formula. They are not decision procedures. The check-sat-using ends up with a goal that isn't "true" or "false", but which is "v3". It takes a sat solver or something else to determine whether the trivial assertion v3 is satisfiable.

It is more appropriate to apply these tactics wen used as end-solvers.

C:\zzz\build>type 3674.smt2
(declare-const v3 Bool)
(assert (not (forall ((q10 Bool) (q11 Bool) (q12 Bool)) v3)))
(apply (then simplify qe_rec))
C:\zzz\build>z3 3674.smt2
(goals
(goal
  (not v3)
  :precision precise :depth 2)
)