Z3Py：evalやz3.parse_smt2_stringを使って式を解析する

Question

私はpythonプログラムを書いていますが、その中には大きな命題式をz3インスタンスに変換する必要があります。例えば

a = my_atomic_proposition("a") # Bool 
b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42 
c = my_atomic_proposition("c") # Bool 
f = my_and(a, my_or(b, my_not(c))) 

を経由して私のプログラムによって作成することができます式fは、私はほとんど以上含む式について話していますのでご注意ください

a = z3.Bool("a") 
b = z3.Real("b") 
c = z3.Bool("c") 
g = z3.And(a, z3.Or(b >= 42, z3.Not(c))) 

ですZ3インスタンスgに変換する必要があります100語。

ポスト Z3 with string expressions後、私は最初、単に私の式のオペランドのすべてを再帰的に行って、途中でZ3のインスタンスを構築し、私自身のパーサー（ポストにLeornardo・デ・モウラによって提案されたオプション1）を構築しようとしました。このオプションはかなり遅かったので、代わりに再帰的に文字列を作成して、はるかに高速で、その後evalを呼び出しました（上のポストで説明したオプション3）。しかし、このソリューションははるかに高速でしたが、私の公式が大きくなりすぎると（MemoryErrorが投げられたとき）はうまくいきませんでした。

だから私はで上記で使用したものではなく、z3.parse_smt2_stringを使用して文字列からz3インスタンスを作成すると、別の構文を持たなければなりません。私はそれがZ3_parse_smtlib_string usage issuesで行われているように何とか似たように進むでしょう。しかし、evalのようにz3.parse_smt2_stringを使用して同様のメモリ問題に遭遇する可能性がありますか？それ以来、私はおそらくこれに多大な努力を払う前に別の方法を模索するでしょう。

また、誰かが私の目標をどのように達成できるかについて他にも（うまくいえばさらに賢いアイデアがある）、私はどんなコメントにも喜んでいます。ご協力ありがとうございます！

EDIT - MemoryErrorの例：のは、私は文字列として、以下の式を有すると仮定しましょう：：

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,z3.Or(a___40,z3.And(True,z3.Or(a___41,z3.And(True,z3.Or(a___42,z3.And(True,z3.Or(a___43,z3.And(True,z3.Or(a___44,z3.And(True,z3.Or(a___45,z3.And(True,z3.Or(a___46,z3.And(True,z3.Or(a___47,z3.And(True,z3.Or(a___48,z3.And(True,z3.Or(a___49,z3.And(True,a___50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))' 

との以下のリスト

私はMemoryErrorがスローされた1例を説明しますfの変数を表す文字列：

variables = ['a___2', 'a___31', 'a___34', 'a___46', 'a___29', 'a___12', 'a___9', 'a___32', 'a___41', 'a___24', 'a___38', 'a___23', 'a___19', 'a___50', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___45', 'a___10', 'a___39', 'a___43', 'a___22', 'a___27', 'a___7', 'a___49', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___44', 'a___11', 'a___14', 'a___30', 'a___42', 'a___47', 'a___8', 'a___26', 'a___48', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18'] 

次のように電子eval：

# Declare z3 variables for all strings in my list 'variables' 
for x in variables: 
    globals()[x] = z3.Bool(x) 
# Create z3 object from string 'f' 
z3f = eval(f) 

とエラーが表示されます。

--------------------------------------------------------------------------- 
MemoryError        Traceback (most recent call last) 
<ipython-input-71-b7421db475e5> in <module>() 
     3  globals()[x] = z3.Bool(x) 
     4 # Create z3 object from string 'f' 
----> 5 z3f = eval(f) 

MemoryError: 

同様のために

より短いfは、上記のコードは正常に動作します。用例：

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,a___40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))' 
variables = ['a___2', 'a___31', 'a___34', 'a___29', 'a___12', 'a___9', 'a___32', 'a___24', 'a___38', 'a___23', 'a___19', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___10', 'a___39', 'a___22', 'a___27', 'a___7', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___11', 'a___14', 'a___30', 'a___8', 'a___26', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18'] 

私が受け取る：例えば、EC-Mを追加するための

z3f = Or(a___0, 
And(True, 
    Or(a___1, 
     And(True, 
      Or(a___2, 
      And(True, 
       Or(a___3, 
        And(True, 
         Or(a___4, 
          And(True, 
           Or(a___5, 
            And(True, 
            Or(a___6, 
            And(True, 
            Or(a___7, 
            And(True, 
            Or(a___8, 
            And(True, 
            Or(a___9, 
            And(True, 
            Or(..., ...))))))))))))))))))))) 

Answer 1

感謝を！

これは事実、Python側の問題です。Pythonはeval(...)のスタックを非常に控えめに制限しています。明らかに、一部のバージョンでは（3536）は35スコープしか扱えません（Parser crashes for deeply nested list displaysで請求されています）。深く入れ子になったラムダでも同様の問題が発生します（Python: nested lambdas — s_push: parser stack overflow Memory Error参照）。

Z3のparse_smt2_stringに切り替えることで、この種の問題を回避することは可能です。これにより、より大きなスタックが可能になります。