回顧Z3py中的匹配模型？

Question

在下面的工作示例中，如何檢索匹配的模型？

 S, (cl_3,cl_39,cl_11, me_32,m_59,m_81) = 
    EnumSort('S', ['cl_3','cl_39','cl_11','me_32','me_59','me_81']) 

     h1, h2 = Consts('h1 h2', S) 
     def fun(h1 , h2): 

     conds = [ 
     (cl_3, me_32), 
     (cl_39, me_59), 
     (cl_11, me_81), 
     # ... 
      ] 

    and_conds = (And(h1==a, h2==b) for a,b in conds) 
    return Or(*and_conds) 

例如： 如下面的求解器

s = Solver() 
    x1 = Const('x1', S) 
    x2 = Const('x2', S) 
    s.add(fun(x1,x2)) 

    print s.check() 
    print s.model() 

Answer 1

我假設你想要的x1和x2由Z3產生的模型中的價值。如果是這樣的話，你可以使用檢索它們：

m = s.model() 
    print m[x1] 
    print m[x2] 

下面是完整的例子（也可在網上here）。順便說一句，請注意，我們不需要h1, h2 = Consts('h1 h2', S)。

S, (cl_3, cl_39, cl_11, me_32, me_59, me_81) = 
     EnumSort('S', ['cl_3','cl_39','cl_11','me_32','me_59','me_81']) 
def fun(h1 , h2): 
    conds = [ 
    (cl_3, me_32), 
    (cl_39, me_59), 
    (cl_11, me_81), 
    ] 
    and_conds = (And(h1==a, h2==b) for a,b in conds) 
    return Or(*and_conds) 

s = Solver() 
x1 = Const('x1', S) 
x2 = Const('x2', S) 
s.add(fun(x1,x2)) 
print s.check() 
m = s.model() 
print m 
print m[x1] 
print m[x2]