Z3 Model Merging

[walnutwaldo]

Hi, apologies if there is already a builtin way to do this. I at least could not find a way to do it using the Python SDK. I would just like to know if there is a better way to do this that addresses some of the issues I'm facing.

Basically, given two ModelRef objects, I want to be able to merge their definitions into a new ModelRef object (assuming there are no conflicting definitions). The current way I do this is using a very weird workaround that involves creating a new solver object to generate the combined model for me. The code is below:

def combine_models(m1: z3.ModelRef, m2: z3.ModelRef) -> z3.ModelRef:
    s = z3.Solver()

    def add_decls(m):
        for d in m.decls():
            if z3.is_const(d):
                s.add(d == m.eval(d))
            elif z3.is_func_decl(d) and d.arity() == 0:
                s.add(d() == m.eval(d()))

    add_decls(m1)
    add_decls(m2)
    cr = s.check()
    assert cr == z3.sat, "Got check result: {}".format(cr)
    return s.model()

‼️ However, even this does not work all the time. For example, there are often functions that don't have arity() == 0. In my exploration, I also have found that there are also often other kinds of things found from model.decls() that don't necessarily correspond directly to variable assignments.

Does anyone know of a builtin/better way of doing this sort of model merging?

[NikolajBjorner]

this wasnt well supported.
I added a way to do this.

from z3 import *

f = Function('f', IntSort(), IntSort())
x, y = Ints('x y')
s1 = Solver()
s1.add(f(x) > 0)
s1.check()
m1 = s1.model()
print(m1)
s2 = Solver()
s2.add(y < 0)
s2.check()
m2 = s2.model()
print(m2)
def merge(m1, m2):
    m = Model()
    for d in m1.decls():
        m.update_value(d, m1[d])
    for d in m2.decls():
        m.update_value(d, m2[d])
    return m

m = merge(m1, m2)
print(m1, m2, m)

[NikolajBjorner]

8e70112

[walnutwaldo]

Much appreciated! Thank you for the quick response + commit