Z3Py：创建模型对象

Question

我想创建一个 Z3 模型对象，例如由 (get-model)/s.model() 和 s = Solver() 返回的模型对象。我从一个元组列表开始(name, value)，其中name 是一个字符串，表示模型中使用的 Z3 变量，value 是分配给变量的值（实数或布尔值）。所以像

def myZ3Model(tuples):
    """ Returns a Z3 model based on the values of the given tuples. """
    <magic>
    return model

t = [('a', True), ('b', 42), ('c', False)]
myZ3Model(t) --> [a = True, b = 42, c = False]

我已经想出了一个非常“hacky”的方法来做到这一点：初始化一个公式，它是所有变量的联合等于它们的分配值，并让求解器返回这个公式的模型。但是，我想知道是否有更优雅的方式来实现我的目标......

Answer 1

这是一件相当奇怪的事情。模型是调用求解器的结果。您似乎希望能够无中生有地创建一个模型，而无需解决任何约束？

话虽如此，这毕竟只是编程，你肯定可以从你的列表中创建这样的约束，让 Z3 解决它们。这将满足您的要求：

from z3 import *

def myZ3Model(tuples):
    s = Solver()

    for (n, v) in tuples:
        if isinstance(v, bool):
            s.add(Bool(n) == v)
        else:
            s.add(Real(n) == v)

    s.check()
    return s.model() 

有了这个定义，你现在可以说：

t = [('a', True), ('b', 42), ('c', False)]
print myZ3Model(t)

它会做你想做的事。一些警告：

• 该构造仅支持您指定的Bool 和Real， 如果您想要其他类型，显然需要扩展。

• 请注意，代码确实涉及解决指定的约束：这应该没有性能损失，因为 约束总是很容易满足。但是你最终还是调用了求解器。