代入 z3 公式中的函数符号 [英] Substituting function symbols in z3 formulas

问题描述

在公式中替换函数符号(用另一个函数)的最佳方法是什么?Z3py 的 substitute 似乎只适用于表达式，我现在要做的是尝试猜测可以应用该函数的 consts/vars 的所有可能组合，然后用另一个函数的应用程序替换它们.有没有更好的方法来做到这一点?

What is the best way to substitute a function symbol (with another function) in a formula? Z3py's substitute seems to only work with expressions, and what I do now is I try to guess all possible combinations of consts/vars to which the function could be applied and then substitute those with an application of another function. Is there a better way to do that?

推荐答案

我们可以实现一个简单的自底向上重写器，给定一个术语 s、一个函数 f 和term t 会将 s 中的每个 f-application f(r_1, ..., r_n) 替换为 <代码>t[r_1, ..., r_n].我使用符号 t[r_1, ..., r_n] 来表示通过用术语 r_1 替换 t 中的自由变量而获得的术语, ..., r_n.

We can implement a simple bottom-up rewriter that given a term s, a function f and term t will replace every f-application f(r_1, ..., r_n) in s with t[r_1, ..., r_n]. I'm using the notation t[r_1, ..., r_n] to denote the term obtained by replacing the free-variables in t with the terms r_1, ..., r_n.

重写器可以实现 Z3 API.我使用 AstMap 缓存结果，使用 todo 列表存储仍需处理的表达式.

The rewriter can be implemented the Z3 API. I use an AstMap to cache results, and a todo list to store expressions that still have to be processed.

这是一个简单的例子，它用 g(t+1) 替换 f(t) 形式的 f-applications in <代码>s.

Here is a simple example that replaces f-applications of the form f(t) with g(t+1) in s.

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

这是代码和更多示例.请注意，我仅在一小部分示例中测试了代码.

Here is the code and more examples. Beware, I only tested the code in a small set of examples.

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

这篇关于代入 z3 公式中的函数符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！