2017-12-05 27 views
1

私はブール式をトラバースするのにZ3pyを使用しています。数式に条件付きが含まれているかどうかを確認する方法。私はz3.pyのソースコードをチェックして、is_and()、is_or()、is_not()、などがありますが、is_implies()には何も関係ありません。何か案が ?ありがとう。式に条件式(=>)が含まれているかどうかをチェックする方法

+0

私は 'z3'の専門家ではないんだけど、' - !> C 'は 'AVC基本的に'...' 'a'と' c'は何でもかまいません。 **!bvcは '!b - > c'で、'!c - > b'、 '!av!bvc'は' a - >(!bvc) 'で、' b - >(! avc) 'と'!c - >(!av!b) 'と '(a&b) - > c'と '...'だから 'is_or()'は十分なはずですか? –

+0

ああ、私は暗示的な排除のためのコードを書いています。だから最初に、コードに含意(厳密な条件)が含まれていることを何らかの形で解析しなければなりません。それから、a => bを!aまたはbに変換します。ありがとう。 – Pushpa

+1

私はあなたの意見が関係していないので、あなたはそれらのすべてではなく、明示的な意味のみを捉えるのに十分満足していると思います。 :) –

答えて

2

関数 "is_app_of"を使用して、式の組み込み関数を判別できます。したがって、

def is_and(a): 
    return is_app_of(a, Z3_OP_AND) 

は、すでにz3.pyファイルに実装し、同様に

def is_implies(a): 
    return is_app_of(a, Z3_OP_IMPLIES) 
+0

ありがとう。素晴らしいことを知っている。 – Pushpa

関連する問題