CODEWITHSUNDEEP
z3
Andreas
Andreas

Reputation: 283

Why does Z3 not solve this simple script with arrays and quantifiers?

Here is a small Z3 problem that returns unknown (timeout), both in a locally built Z3 4.6.0 and on https://rise4fun.com/z3/tutorial:

(declare-const m1 (Array String Int))
(declare-const m2 (Array String Int))
(declare-const c Int)
(assert (or (= c 11) (= c 12)))
(assert (forall ((x String)) (= (select m1 x) 0)))
(assert (= (select m2 "0") 42))
(assert (forall ((x String)) (or (= x "0") (= (select m2 x) 0))))
(assert (= m2 (ite (= c 11) (store m1 "1" 100) (store m1 "0" 42))))
(check-sat)

I'm curious why z3 is not able to prove it. How is Z3 processing this problem and is there a way I can determine what Z3 is trying to do? When I run with -v:15, I see output like this:

(smt.restarting :propagations 0 :decisions 903 :conflicts 1 :restart 100 :agility 0.00)
(smt.mbqi)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 84)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!8)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 82)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!10)
(smt.restarting :propagations 0 :decisions 946 :conflicts 1 :restart 100 :agility 0.00)
^C(tactic-exception "canceled")

I'm not entirely sure what to make of that output. Is there a way to see more info on Z3's state at each of these points?

When I change the problem slightly to the following, it finishes immediately:

(declare-const m1 (Array String Int))
(declare-const m2 (Array String Int))
(declare-const c Int)
(assert (= c 12)) ; or (= c 11)
(assert (forall ((x String)) (= (select m1 x) 0)))
(assert (= (select m2 "0") 42))
(assert (forall ((x String)) (or (= x "0") (= (select m2 x) 0))))
(assert (= m2 (ite (= c 11) (store m1 "1" 100) (store m1 "0" 42))))
(check-sat)

Can the first problem be fixed (while letting c be indeterminate to solve for), while still requiring that m1 is 0 for all values and m2 is 0 on all values other than "0", e.g. by applying appropriate tactics or quantifier patterns?

Upvotes: 1

Views: 366

Answers (1)

alias
alias

Reputation: 30485

For declaring constant arrays, you should prefer the const struct, instead of going through quantifiers. That is, replace:

(assert (forall ((x String)) (= (select m1 x) 0)))

with:

(assert (= m1 ((as const (Array String Int)) 0)))

You'll notice that z3 can now handle your query with ease.

Constant arrays are explained in the Z3 guide: https://rise4fun.com/z3/tutorialcontent/guide#h26

Upvotes: 1

Related Questions