2

给定一个表达式 f ，我想用（是一个数字）之类v的f东西替换所有变量。目前我必须通过以下步骤来实现这一点v_dd

  1. 获取所有变量f
  2. 对于 中的每个变量v，f确定其排序，然后生成适当的v_dvar。
  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_
4

0 回答 0