Z3Py - 표현식이 포함 된 모든 수식을 가져옵니다.

Question

Z3Py에서 일부 변수/표현식이 발생하는 모든 수식의 목록을 가져올 수 있습니까? 예 :

s.add(x < 0) 
s.add(x > y) 
print s[y] 
>>> x > y 

Answer 1

Z3 API에는이 기능이 포함되어 있지 않습니다. 그러나 Z3 API 위에 구현 될 수 있습니다. 다음은 간단한 구현입니다.

from z3 import * 

# Wrapper for allowing Z3 ASTs to be stored into Python Hashtables. 
class AstRefKey: 
    def __init__(self, n): 
     self.n = n 
    def __hash__(self): 
     return self.n.hash() 
    def __eq__(self, other): 
     return self.n.eq(other.n) 
    def __repr__(self): 
     return str(self.n) 

def askey(n): 
    assert isinstance(n, AstRef) 
    return AstRefKey(n) 

# Return True iff f contains t. 
def contains(f, a): 
    visited = set() # Set of already visited formulas 
    # We need to track the set of visited formulas because Z3 represents them as DAGs. 
    def loop(f): 
     if askey(f) in visited: 
      return False # already visited 
     visited.add(askey(f)) 
     if f.eq(a): 
      return True 
     else: 
      for c in f.children(): 
       if loop(c): 
        return True 
      return False 
    return loop(f) 

# Return the set of assertions in s that contains x 
def assertions_containing(s, x): 
    r = [] 
    for f in s.assertions(): 
     if contains(f, x): 
      r.append(f) 
    return r 

x = Real('x') 
y = Real('y') 
s = Solver() 
s.add(x < 0) 
s.add(x > y) 
print assertions_containing(s, y) 
print assertions_containing(s, x)