在z3公式中替換函數符號

Question

在公式中用函數符號替代函數符號的最佳方法是什麼？ Z3py的substitute似乎只適用於表達式，我現在所做的是嘗試猜測可以應用該函數的const/vars的所有可能組合，然後用另一個函數的應用替換那些組合。有沒有更好的方法來做到這一點？

Answer 1

我們可以實現一個簡單的自下而上的重寫，鑑於術語s，功能f和期限t將t[r_1, ..., r_n]取代每f -application f(r_1, ..., r_n)在s。我使用t[r_1, ..., r_n]表示通過將t中的自由變量替換爲術語r_1，...，r_n而獲得的術語。

重寫器可以實現Z3 API。我使用AstMap來緩存結果，並使用todo列表來存儲仍然需要處理的表達式。

下面是一個簡單的例子，它代替f-表示f(t)的應用g(t+1)在s中的應用。

x = Var(0, IntSort()) 
print rewrite(s, f, g(x + 1)) 

這裏是代碼和更多的例子。當心，我只在一小組示例中測試代碼。

from z3 import * 

def update_term(t, args): 
    # Update the children of term t with args. 
    # len(args) must be equal to the number of children in t. 
    # If t is an application, then len(args) == t.num_args() 
    # If t is a quantifier, then len(args) == 1 
    n = len(args) 
    _args = (Ast * n)() 
    for i in range(n): 
     _args[i] = args[i].as_ast() 
    return z3._to_expr_ref(Z3_update_term(t.ctx_ref(), t.as_ast(), n, _args), t.ctx) 

def rewrite(s, f, t): 
    """ 
    Replace f-applications f(r_1, ..., r_n) with t[r_1, ..., r_n] in s. 
    """ 
    todo = [] # to do list 
    todo.append(s) 
    cache = AstMap(ctx=s.ctx) 
    while todo: 
     n = todo[len(todo) - 1] 
     if is_var(n): 
      todo.pop() 
      cache[n] = n 
     elif is_app(n): 
      visited = True 
      new_args = [] 
      for i in range(n.num_args()): 
       arg = n.arg(i) 
       if not arg in cache: 
        todo.append(arg) 
        visited = False 
       else: 
        new_args.append(cache[arg]) 
      if visited: 
       todo.pop() 
       g = n.decl() 
       if eq(g, f): 
        new_n = substitute_vars(t, *new_args) 
       else: 
        new_n = update_term(n, new_args) 
       cache[n] = new_n 
     else: 
      assert(is_quantifier(n)) 
      b = n.body() 
      if b in cache: 
       todo.pop() 
       new_n = update_term(n, [ cache[b] ]) 
       cache[n] = new_n 
      else: 
       todo.append(b) 
    return cache[s] 

f = Function('f', IntSort(), IntSort()) 
a, b = Ints('a b') 
s = Or(f(a) == 0, f(a) == 1, f(a+a) == 2) 
# Example 1: replace all f-applications with b 
print rewrite(s, f, b) 

# Example 2: replace all f-applications f(t) with g(t+1) 
g = Function('g', IntSort(), IntSort()) 
x = Var(0, IntSort()) 
print rewrite(s, f, g(x + 1)) 

# Now, f and g are binary functions. 
f = Function('f', IntSort(), IntSort(), IntSort()) 
g = Function('g', IntSort(), IntSort(), IntSort()) 

# Example 3: replace all f-applications f(t1, t2) with g(t2, t1) 
s = Or(f(a, f(a, b)) == 0, f(b, a) == 1, f(f(1,0), 0) == 2) 
# The first argument is variable 0, and the second is variable 1. 
y = Var(1, IntSort()) 
print rewrite(s, f, g(y, x)) 

# Example 4: quantifiers 
s = ForAll([a], f(a, b) >= 0) 
print rewrite(s, f, g(y, x + 1))