1

Z3Py では、何かが標準文法を使用する用語であるかどうかを確認する必要がありますterm := const | var | f(t1,...,tn))。それを判断するために次の関数を作成しましたが、n 項関数をチェックする方法はあまり最適ではないようです。

そうするより良い方法はありますか？これらのユーティリティ関数is_term、is_atom、is_literalなどは、Z3 に含めると便利です。私はそれらを投稿セクションに入れます

CONNECTIVE_OPS = [Z3_OP_NOT,Z3_OP_AND,Z3_OP_OR,Z3_OP_IMPLIES,Z3_OP_IFF,Z3_OP_ITE]
REL_OPS = [Z3_OP_EQ,Z3_OP_LE,Z3_OP_LT,Z3_OP_GE,Z3_OP_GT]

def is_term(a):
    """
    term := const | var | f(t1,...,tn)
    """
    if is_const(a):
        return True
    else:
        r = (is_app(a) and \
                 a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \
                 all(is_term(c) for c in a.children()))
        return r
4

2 に答える 2

1

一次論理で使用される用語、アトム、およびリテラルの「教科書」定義は、Z3 式に直接適用することはできません。Z3 では、f(And(a, b)) > 0やなどの式を使用できますf(ForAll([x], g(x) == 0))。ここで、fはブール値から整数への関数です。この拡張機能は表現力を向上させるものではありませんが、問題を作成するときに非常に便利です。SMT 2.0 標準では、「用語」if-then-else表現も使用できます。これは、「項」内に「数式」をネストできるもう 1 つの機能です。例: g(If(And(a, b), 1, 0)).

Z3 式を操作するプロシージャを実装する場合、ブール式と非ブール式を区別する必要がある場合があります。この場合、「用語」はブールソートを持たない単なる式です。

def is_term(a):
   return not is_bool(a)

And他の例では、ブール結合子 ( 、Or、...) を特別な方法で処理したいと考えています。たとえば、CNF トランスレータを定義しています。この場合、「アトム」を量化子ではないブール式、(自由な) 変数、またはブール結合子の 1 つではないアプリケーションとして定義します。

def is_atom(a):
   return is_bool(a) and (is_var(a) or (is_app(a) and a.decl().kind() not in CONNECTIVE_OPS))

アトムを定義した後、リテラルは次のように定義できます。

def is_literal(a):
   return is_atom(a) or (is_not(a) and is_atom(a.arg(0)))

これらの関数を示す例を次に示します ( rise4funでオンラインでも入手できます)。

x = Int('x')
p, q = Bools('p q')   
f = Function('f', IntSort(), BoolSort())   
g = Function('g', IntSort(), IntSort())
print is_literal(Not(x > 0))    
print is_literal(f(x))
print is_atom(Not(x > 0))
print is_atom(f(x))
print is_atom(x)
print is_term(f(x))
print is_term(g(x))
print is_term(x)
print is_term(Var(1, IntSort()))
于 2013-01-03T16:22:23.300 に答える
1

関数は合理的です。いくつかのコメントがあります。

  1. 仕様で「var」が何を意味するかによって異なります。Z3 には de-Brujin インデックスとして変数があります。z3py には「is_var(a)」という関数があり、「a」が変数インデックスかどうかをチェックします。

  2. 別のブール結合子 Z3_OP_XOR があります。

  3. ビットベクトルを比較する演算など、追加の関係演算があります。コードの意図と使用法によって異なりますが、代わりに、式の種類がブール値であるかどうか、および head 関数シンボルが解釈されていないことが保証されているかどうかを確認することもできます。

  4. is_const(a) は return is_app(a) および a.num_args() == 0 として定義されています。つまり、is_const は実際にはデフォルトのケースで処理されます。

  5. 単純化、解析、またはその他の変換の結果として Z3 が作成する式には、多くの共有サブ式が含まれる場合があります。したがって、単純な再帰的下降は、式の DAG サイズで指数関数的な時間を要する可能性があります。これは、訪問したノードのハッシュ テーブルを維持することで対処できます。Python から Z3_get_ast_id を使用して式の一意の番号を取得し、これをセットで維持できます。用語がガベージ コレクションされない限り、識別子は一意であるため、そのようなセットをローカル変数として維持する必要があります。

したがって、次のようなものです。

 def get_expr_id(e):
     return Z3_get_ast_id(e.ctx.ref(), e.ast)

 def is_term_aux(a, seen):
    if get_expr_id(a) in seen:
        return True
    else:
        seen[get_expr_id(a)] = True
        r = (is_app(a) and \
             a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \
             all(is_term_aux(c, seen) for c in a.children()))
        return r

 def is_term(a):
     return is_term_aux(a, {})
于 2013-01-03T16:10:47.113 に答える