Z3 MBQI different behavior between API and SMT-LIB for the same model

Question

I'm using Z3 to check some quantified formulas. If I assert the formula via Z3's Java API the MBQI engine might not converge if the formula is unsat. I know that my formulas are not in a fragment of FOL that is known to be decidable, however if I input the same formula via Z3's smt-lib interface it produces an answer quite quickly. I suspect that some option is not being set via the API that is normally active with the normal SMTLIB input or that I'm not adding important meta information to the formulas via the API.

The assertion in the following SMTLIB session was taken directly from the toString of the BoolExpr I'm asserting via the API:

(set-option :smt.mbqi true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi.trace true)
(declare-fun R (Int Int) Bool)
(declare-const |'x| Int)
(declare-const |'y| Int)
(assert 
  (let ((a!1 (forall ((|'x0| Int) (|'y0| Int))
         (= (R |'x0| |'y0|)
            (and (forall ((|'y1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'y0| 0) (= |'y1| 1))
                                       (and (= |'y0| 1) (= |'y1| 3))
                                       (and (= |'y0| 2) (= |'y1| 3))
                                       (and (= |'y0| 0) (= |'y1| 2)))))
                         (a!2 (exists ((|'x1| Int))
                                (and (or (and (= |'x0| 3) (= |'x1| 0))
                                         (and (= |'x0| 1) (= |'x1| 3))
                                         (and (= |'x0| 1) (= |'x1| 2))
                                         (and (= |'x0| 2) (= |'x1| 0))
                                         (and (= |'x0| 0) (= |'x1| 1)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2)))
                 (forall ((|'x1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'x0| 3) (= |'x1| 0))
                                       (and (= |'x0| 1) (= |'x1| 3))
                                       (and (= |'x0| 1) (= |'x1| 2))
                                       (and (= |'x0| 2) (= |'x1| 0))
                                       (and (= |'x0| 0) (= |'x1| 1)))))
                         (a!2 (exists ((|'y1| Int))
                                (and (or (and (= |'y0| 0) (= |'y1| 1))
                                         (and (= |'y0| 1) (= |'y1| 3))
                                         (and (= |'y0| 2) (= |'y1| 3))
                                         (and (= |'y0| 0) (= |'y1| 2)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2))))))))
 (and (= |'x| 0) (= |'y| 0) (R |'x| |'y|) a!1)))
(check-sat)

Interestingly, when I run the above through Z3's SMTLIB interface the MBQI trace is short and looks like this:

(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
...
(smt.mbqi "started")
(smt.mbqi :checking k!37)
(smt.mbqi :failed k!37)
(smt.mbqi :num-failures 1)
unsat

However, the trace when run via the API (and the same solver options) looks like:

(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)
(smt.mbqi "started")
(smt.mbqi :failed null)
(smt.mbqi :num-failures 1)

Is the "null" reference indicative of something I'm doing wrong on the API side?

The null reference is because I was not providing a quantifier ID when I constructed the quantifier. Unfortunately, even when a quantifier ID is set the MBQI refinement process does not converge using the API — j58

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2015-05-19T17:01:27

I am having some trouble reproducing the failure behavior. Here is how I emulate the API behavior:

from z3 import *

spec = """
(declare-fun R (Int Int) Bool)
(declare-const |'x| Int)
(declare-const |'y| Int)
(assert 
  (let ((a!1 (forall ((|'x0| Int) (|'y0| Int))
         (= (R |'x0| |'y0|)
            (and (forall ((|'y1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'y0| 0) (= |'y1| 1))
                                       (and (= |'y0| 1) (= |'y1| 3))
                                       (and (= |'y0| 2) (= |'y1| 3))
                                       (and (= |'y0| 0) (= |'y1| 2)))))
                         (a!2 (exists ((|'x1| Int))
                                (and (or (and (= |'x0| 3) (= |'x1| 0))
                                         (and (= |'x0| 1) (= |'x1| 3))
                                         (and (= |'x0| 1) (= |'x1| 2))
                                         (and (= |'x0| 2) (= |'x1| 0))
                                         (and (= |'x0| 0) (= |'x1| 1)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2)))
                 (forall ((|'x1| Int) (a Int))
                   (let ((a!1 (not (or (and (= |'x0| 3) (= |'x1| 0))
                                       (and (= |'x0| 1) (= |'x1| 3))
                                       (and (= |'x0| 1) (= |'x1| 2))
                                       (and (= |'x0| 2) (= |'x1| 0))
                                       (and (= |'x0| 0) (= |'x1| 1)))))
                         (a!2 (exists ((|'y1| Int))
                                (and (or (and (= |'y0| 0) (= |'y1| 1))
                                         (and (= |'y0| 1) (= |'y1| 3))
                                         (and (= |'y0| 2) (= |'y1| 3))
                                         (and (= |'y0| 0) (= |'y1| 2)))
                                     (R |'x1| |'y1|)))))
                     (or a!1 a!2))))))))
 (and (= |'x| 0) (= |'y| 0) (R |'x| |'y|) a!1)))
"""


spec = parse_smt2_string(spec)

#set_option(verbose=10)
set_option('smt.mbqi', True)
set_option('smt.pull_nested_quantifiers', True)
set_option('smt.mbqi.trace', True)

s = Solver()
s.add(spec)
print s.check()

In my case, Z3 quickly returns with the answer unsat. The main approaches for investigating with goes on with behaviors is by using verbose tracing. The verbose trace will show which tactics are invoked. You can use verbose tracing both from SMT-LIB (from the command line pass the option -v:10 or similar number).

Z3 MBQI different behavior between API and SMT-LIB for the same model

1 Answers