Configure a quantifier so it cannot be instantiated by e-matching

[utaal]

I am interested in configuring a quantifier so it cannot be instantiated by e-matching (but it can be instantiated by mbqi), in the context of program verification. Here's a synthetic example:

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-sort Foo)
(declare-fun one (Foo) Bool)
(declare-fun two (Foo) Bool)

(declare-fun dummy_pattern (Foo) Bool)

(assert
  (forall ((f Foo)) (!
    (=>
      (one f)
      (two f)
    )
    :pattern (dummy_pattern f)
    :qid forall_f_one_two
  ))
)

(declare-const f1 Foo)
(assert (not
  (=>
    (one f1)
    (two f1)
  )
))

(check-sat)

This results in unknown ((:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)")), as expected.

• commenting out the line :pattern (dummy_pattern f) results in unsat, as expected;
• setting smt.mbqi to true results in unsat, as expected.

I'm looking for a way to accomplish the same (preventing e-matching instantiation) without having to provide a dummy pattern. Removing all the patterns lets z3 pick a pattern for the quantifier, and something like :pattern () is just ignored.

[NikolajBjorner]

there isn't a way at present to disable pattern inference (by setting parameters). Is this a feature request?

[utaal]

there isn't a way at present to disable pattern inference (by setting parameters). Is this a feature request?

Now that I know that there is in fact no way to disable pattern inference, I think it's indeed a feature request. Though it would only be enabling some experimentation for research work at this stage (in the context of program verification within EPR), so it's not critical for us at this stage.

Would you be open to adding this feature? We may be able to contribute the implementation. If so, should this be an additional attribute on the quantifier? (:no-pattern-qi? other suggestions?)

[NikolajBjorner]

I don't see what value :no-pattern-qi has over using a :pattern (dummy_pattern f). They seem to achieve the same. The parameter addition would disable pattern inference across all quantifiers. Maybe that isn't desired either?

[utaal]

I don't see what value :no-pattern-qi has over using a :pattern (dummy_pattern f).

This requires declaring a dummy_pattern function for each type that may appear in a quantifier (in the context where z3 smtlib input is emitted by a separate tool), while an attribute could explicitly mark the quantifier to disable pattern inference. But the dummy pattern approach is definitely workable for experimentation.

The parameter addition would disable pattern inference across all quantifiers. Maybe that isn't desired either?

I had misunderstood this the first time. And indeed having a (set-option :_) parameter for that would be desirable. It would be useful for these experiments and we would set it in the Verus rust verification tool we develop, where we try to never rely on pattern inference, as we try and choose triggers more relevant to our specific task.

I'll try and take a look to see if I can implement it. (Should it be named something like smt.qi.pattern-inference and default to true?)