(Semi-decidable) combination of first-order theories is possible in Z3, but what about an actual semantic/signature-wise combination?

Question

Disclaimer: This is a rather theoretical question, but think it fits here; in case not, let me know an alternative :)

Z3 seems expressive

Recently, I realized I can specify this type of formulae in Z3:

Exists x,y::Integer s.t. [Exists i::Integer s.t. (0<=i<|seq|) & (avg(seq)+t<seq[i])] & (y<Length(seq)) & (y<x)

Here is the code (in Python):

from z3 import *

#Average function

IntSeqSort = SeqSort(IntSort())

sumArray    = RecFunction('sumArray', IntSeqSort, IntSort())
sumArrayArg = FreshConst(IntSeqSort)

RecAddDefinition( sumArray
                , [sumArrayArg]
                , If(Length(sumArrayArg) == 0
                    , 0
                    , sumArrayArg[0] + sumArray(SubSeq(sumArrayArg, 1, Length(sumArrayArg) - 1))
                    )
                )

def avgArray(arr):
    return ToReal(sumArray(arr)) / ToReal(Length(arr))

###The specification

t = Int('t')
y = Int('y')
x = Int('x')
i = Int('i') #Has to be declared, even if it is only used in the Existential

seq = Const('seq', SeqSort(IntSort()))

avg_seq = avgArray(seq)

phi_0 = And(2<t, t<10)
phi_1 = And(0 <= i, i< Length(seq))
phi_2 = (t+avg_seq<seq[i])

big_vee = And([phi_0, phi_1, phi_2])

phi = Exists(i, big_vee)


phi_3 = (y<Length(seq))
phi_4 = (y>x)

union = And([big_vee, phi_3, phi_4])

phiTotal = Exists([x,y], union)

s = Solver()
s.add(phiTotal)
print(s.check())
#s.model()
solve(phiTotal) #prettier display

We can see how it outputs sat and outputs models.

But...

However, even if this expressivity is useful (at least for me), there is something I am missing: formalization.

I mean, I am combining first-order theories that have different signature and semantics: a sequence-like theory, an integer arithmetic theory and also a (uninterpreted?) function avg. Thus, I would like to combine these theories with a Nelson-Oppen-like procedure, but this procedure only works with quantifier-free fragments.

I mean, I guess this combined theory is semi-decidable (because of quantifiers and because of sequences), but can we formalize it? In case yes, I would like to (in a correct way) combine these theories, but I have no idea how.

An exercise (as an orientation)

Thus, in order to understand this, I proposed a simpler exercise to myself: take the decidable array property fragment (What's decidable about arrays?http://theory.stanford.edu/~arbrad/papers/arrays.pdf), which has a particular set of formulae and signature.

Now, suppose I want to add an avg function to it. How can I do it?

• Do I have to somehow combine the array property fragment with some kind of recursive function theory and an integer theory? How would I do this? Note that these theories involve quantifiers.
• Do I have to first combine these theories and then create a decision procedure for the combined theory? How?
• Maybe it suffices with creating a decision procedure within the array property fragment?
• Or maybe it suffices with a syntactic adding to the signature?

Also, is the theory array property fragment with an avg function still decidable?

Answer 1

A non-answer answer: Start by reading Chapter 10 of https://www.decision-procedures.org/toc/

A short answer: Unless your theory supports quantifier-elimination, SMT solvers won't have a decision-procedure. Assuming they all admit quantifier-elimitation, then you can use Nelson-Oppen. Adding functions like avg etc. do not add significantly to expressive power: They are definitions that are "unfolded" as needed, and so long as you don't need induction, they're more or less conveniences. (This is a very simplified account, of course. In practice, you'll most likely need induction for any interesting property.)

If these are your concerns, it's probably best to move to more expressive systems than push-button solvers. Start looking at Lean: Sure, it's not push-button, but it provides a very nice framework for general purpose theorem proving: https://leanprover.github.io

Even longer answer is possible, but stack-overflow isn't the right forum for it. You're now looking into the the theory of decision procedures and theorem-proving, something that won't fit into any answer in any internet-based forum. (Though https://cstheory.stackexchange.com might be better, if you want to give it a try.)