在 Z3-Python 中，我在执行模型搜索时得到 "builtin_function_or_method' object is not iterable"

Question

我正在探索在 Z3 中执行 SAT 求解的快速方法 (Python)。为此，我试图模仿 https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations.

第 5.1 章的结果

我使用的代码如下：

def block_modelT(s, terms): #I used the name 'block_modelT' so as not to use 'block_model'
    m = s.model()
    s.add(Or([t != m.eval(t) for t in terms]))

def all_smt(s, terms):
    while sat == s.check():
       print(s.model())
       block_modelT(s, terms)

因此，我执行它：

pip install z3-solver
from z3 import *

x, y, z = Bools('x y z')
vars = [x,y,z]

phi_0 = x #ignore that I call them phi: it is because I am used to do it like that for predicates (i.e. literals) of other theories: e.g., if x is Int, then phi_0 = (x>0)
phi_1 = y
phi_2 = z

phi = And(phi_0, Or(phi_1, phi_2))

all_smt(s, vars)

并得到以下错误：

      1 def block_modelT(s, terms):
      2     m = s.model()
----> 3     s.add(Or([t != m.eval(t) for t in terms]))

TypeError: 'builtin_function_or_method' object is not iterable

有什么帮助吗？

编辑：

问题已经解决，终于尝试了下一段代码：

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t))
    def fix_term(s, m, t):
        s.add(t == m.eval(t))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               for m in all_smt_rec(terms[i:]):
                   yield m
               s.pop()   
    for m in all_smt_rec(list(initial_terms)):
        yield m

我执行它：all_smt(s, varss) #has the same name。并获得生成器 <generator object all_smt at 0x7... 而不是有效的分配（即模型）。如何才能得到正确答案[z = False, y = True, x = True], [z = True, x = True]？ print 和 return.

我都试过了

Answer 1

您的程序没有定义 s；而且您还没有向其中添加公式。以下对我有用：

from z3 import *

def block_modelT(s, terms): #I used the name 'block_modelT' so as not to use 'block_model'
    m = s.model()
    s.add(Or([t != m.eval(t) for t in terms]))

def all_smt(s, terms):
    while sat == s.check():
       print(s.model())
       block_modelT(s, terms)

x, y, z = Bools('x y z')
vars = [x,y,z]

phi_0 = x #ignore that I call them phi: it is because I am used to do it like that for predicates (i.e. literals) of other theories: e.g., if x is Int, then phi_0 = (x>0)
phi_1 = y
phi_2 = z

phi = And(phi_0, Or(phi_1, phi_2))

s = Solver()
s.add(phi)

all_smt(s, vars)

这会打印：

[z = False, y = True, x = True]
[z = True, x = True]

在 Z3-Python 中，我在执行模型搜索时得到 "builtin_function_or_method' object is not iterable"

In Z3-Python, I get "builtin_function_or_method' object is not iterable" when performing model search

python

theorem-proving

z3

z3py

sat