python - Z3 で既存の式から新しい式を生成する

Question

v式 f が与えられた場合、すべての変数を( is a number) のfようなものに置き換えたいと思います。現在、これを達成するには、次の手順を実行する必要がありますv_dd

1. のすべての変数を取得します。f
2. の各変数について、その並べ替えを決定し、適切な var を生成しvます。 fv_d
3. 代用をする

私はまだZ3 pythonを学ぼうとしているので、おそらく上記を行うためのはるかに良い方法がありますか?

ありがとう。

私の完全なコードを以下に示します。

def get_vars(f,rs=[]):
    """obtain variables from f"""

    if is_const(f):
        try:
            f.as_string()   #to differentiate btw Int('x') and IntVal('3')
            return rs
        except AttributeError:
            return vset(rs + [f],str)

    else:
        for f_ in f.children():
            rs = get_vars(f_,rs)

        return vset(rs,str)

def gen_vars(vs,i):
    """
    Generates a new set of variables
    E.g.   v =>  v_i   ,  v_next =>  v_(i+1)

    """

    assert i>=0

    def mk_name(i,v):
        next_kw = '_next'
        if str(v).endswith(next_kw):
            astr = str(v)[:-len(next_kw)] + '_' + str(i+1)
        else:
            astr = str(v) + '_' + str(i)
        return astr

    def mk_var(name,vsort):
        if vsort.kind() == Z3_INT_SORT:
            v = Int(name)
        elif vsort.kind() == Z3_REAL_SORT:
            v = Real(name)
        elif vsort.kind() == Z3_BOOL_SORT:
            v = Bool(name)
        elif vsort.kind() == Z3_DATATYPE_SORT:
            v = Const(name,vsort)

        else:
            assert False, 'Cannot handle this sort yet (id: %d)'%vsort.kind()

        return v

    #so that the longest one is replaced first
    vs = sorted(vs,key=str,reverse=True) 

    names = [mk_name(i,v) for v in vs] 
    vs_ = [mk_var(ns,v.sort()) for ns,v in zip(names,vs)]


    vss = zip(vs,vs_)

    return vss

def substitute_f(f,i,vs=None):
    """
    Replaces all variables v in f with v_(i*_)
    vs: variables in f (could be automatically obtained from f)
    """

    assert is_expr(f)
    assert isinstance(vs,list) or vs is None

    if vs is None:
        vs = get_vars(f)

    vss = gen_vars(vs,i)

    f_ = f
    for pvs in vss:
        f_ = substitute(f_,pvs)

    return f_