Model-based Quantifier Instantiation and the St1 fragment of many-sorted logic

Question

This is a follow-up to my previous question on Z3's Model-based Quantifier Instantiation (MBQI) and the stratified sorts fragment (thanks again to Leonardo de Moura for the quick answer).

In their paper on decidable fragments of many-sorted logic [Abadi et al., Decidable fragments of many-sorted logic, LPAR 2007], the authors describe a fragment St1 of many-sorted logic that is decidable with a finite model property.

This fragment requires the sorts to be stratified and the formula F to be in (skolemized) prenex normal form as described in the Z3 documentation, but allows an additional atomic formula

y in Im[f]

to occur in F, which is a "shorthand" for

exists x1 : A1, ..., xn : An . y = f(x1,...,xn)

where f is a function with a signature f : A1 x ... x An -> B, and f must be the only function with range B. Thus, the St1 fragment allows (in a very restricted way) to violate the stratification, e.g., in order to assert that f is surjective.

I am not sure if this could be an open research question: Does someone know whether the MBQI decision procedure for Z3 is complete for the St1 fragment? Will Z3 produce (theoretically) either SAT or UNSAT for F after a finite time?

Answer 1

First, one clarification, in principle, MBQI can decide the stratified multi-sorted fragment. The justification is given in Section 4.1 of http://research.microsoft.com/en-us/um/people/leonardo/ci.pdf (*). However, Z3 4.0 does not support implement the additional rules suggested in Section 4.1. So, Z3 4.0, may fail (return unknown) on formulas that are in this fragment. I just want to make clear a distinction between the algorithm and the actual implementation using the current Z3.

Regarding your question, yes MBQI framework can decide the stratified formulas containing the expanded predicate y in Im[f]. I'm assuming this predicate occurs only positively. That is, we do not have not y in Im[f] which is equivalent to

forall x1:A1, ...,xn:An. y != f(x1, ... xn)

If y in Im[f] occurs only positively, then it can be expanded, and after skolemization we have a ground formula of the form y = f(k1, ..., kn). MBQI is still a decision procedure because the set F* defined in (*) will still be finite. F* may become infinite only if the stratification is broken inside of a universal formula.