在 Z3py 中检索匹配的模型? [英] retrieve the matched model in Z3py?

问题描述

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

In the following working example , How to retrieve the matched model?

     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()

推荐答案

我假设你想要 Z3 生成的模型中 x1 和 x2 的值.如果是这种情况，您可以使用以下方法检索它们:

I'm assuming that you want the value of x1 and x2 in the model produced by Z3. If that is the case, you can retrieve them using:

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

这是完整的示例(也可以在此处在线获得).顺便说一句，请注意我们不需要 h1, h2 = Consts('h1 h2', S).

Here is the complete example (also available online here). BTW, note that we don't need 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]

这篇关于在 Z3py 中检索匹配的模型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！