Guidelines to tuning Z3 quantifier instantiation (with SMT-LIB interface)

0
votes

I am trying to tune z3 on machine-generated problems that

  • are unsatisfiable,
  • contain assertions that are irrelevant for the proof
  • irrelevant assertions contain quantifiers
  • where z3 is unable to find the unsatisfiability proof because of these irrelevant assertions (removing them manually shows this).

Are there any general guidelines to handle this situation?

Going through the command line options, I thought I could try:

mbqi.id (string) Only use model-based instantiation for quantifiers with id's beginning with string (default: )

Yet I do not see how I can attach an id to a quantifier using the SMT-LIB syntax. Could anyone with a clue share it with me?

1
z3smt

1 Answers

2
votes

The id mentioned here is simply the name of the quantified variable. If you have:

(declare-sort S 0)
(declare-fun gt (S S) bool)

(assert (forall ((inst_a S) (inst_b S))
          (or (gt inst_a inst_b) (gt inst_b inst_a))))

(check-sat)

Then you can say:

z3 smt.mbqi=true smt.mbqi.id=inst a.smt2

Don't forget to use smt.mbqi=true to turn MBQI on. If you use this call, then z3 will only instantiate a pattern if the quantified variable starts with inst in the above example.