일치하는 모델을 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) 

: 의 I 당신이 Z3에 의해 생성 된 모델 x1 및 x2의 값을 원하는 있으리라 믿고있어

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

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

Answer 1

해결사 다음과 같이. 이런 경우, 당신은 사용하여 검색 할 수 있습니다 : 여기

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]