z3py

2熱

1答えて

私はBoolsの束を持っている： a=Bool('a') ... z=Bool('z') タプルにこれらのboolsの一部をパックした後、その非平等についての制約を追加する方法は？私が試した： tuple1=(a,b,c,d) tuple2=(e,f,g,h) # so far so good s=Solver() s.add(tuple1 != tuple2) しかし、それ

2熱

1答えて

z3pyでcrackmeを解く

Z3でcrackmeを解いてみたい。 crackmeはかなり大きいですが、次のように単純化することができます:: #! /usr/bin/python import sys T='Fguad2x-GP5_QqNi' key=sys.argv[1] if len(key) != 3: print "Bad key length" exit(1) out=[] f

0熱

1答えて

z3py：私はZ3のPythonのAPIを使用しています具体的な値

でネストされた店舗を簡素化し、[バージョン4.4.2 - 64ビット]と私はZ3が、この場合には式を簡素化する理由を理解しようとしています： >>> a = Array('a', IntSort(), IntSort()) >>> a = Store(a, 0, 1) >>> a = Store(a, 0, 3) >>> simplify(a) Store(a, 0, 3) それがこの

0熱

1答えて

z3.z3types.Z3Exception：モデルが利用できません

私は最新のビルドリリース（x64）をWin10 x64、python 2.7 x64で使用しています。私はこの制約にmodelを呼び出そう： (i2 % 59) == (i2 * i10) , (i10 % 43) == ((i2 + i12) % 3) , 4 != (i14 % 28) , 5 != (i14 % 28) , 6 != (i14 % 28) , 7 != (i14 % 28

0熱

1答えて

Z3py - 配列変数の制約を解く際に生成される関数k！0

研究活動中、z3pyの配列（Python API for Z3 v4.4.2）を調べています。なぜz3が結果としてより多くの配列関数を提供するのか疑問に思っていました。！Z3はKを使用していますように思え >>> A = Array('A', IntSort(), IntSort()) >>> solve(A[0] == 0) [A = [0 -> 0, else -> 0], k!0 =

0熱

1答えて

Z3ソルバのランタイムを計算するには

私はz3pyを使って一連の方程式を解いています。どのように私はそれのランタイム順序を計算するでしょうか？これは、線形方程式のセットで満たされる必要があるbitvecs変数を持ちます。マニュアルとガイドでは、ランタイムを計算する方法はありません。

0熱

1答えて

問題Z3 CC_NUM_THREADSを使用して並列Z3を設定しながら、= 3

号Z3 CC_NUM_THREADSを使用して並列Z3の設定中= 3 私は= 3私のSMT2ファイル次のエラーのためには、popingさCC_NUM_THREADSとZ3の並列バージョンを実行しようとしていますアップ。 ERROR: unknown parameter 'cc_num_threads' Legal parameters are: auto_config (bool) (def

1熱

1答えて

バインドされた変数の種類がfinite_domain_sortにならないのはなぜですか？

私は有限ドメインソート困惑の束縛された変数の振る舞いを見つけます。次のコードは、それらが is_finite_domain_sort述語を満たさないことを示しています。どんな考え？ Mac上 from z3 import * U=FiniteDomainSort('U', 3) V=FiniteDomainSort('V', 2) u=Const('u', U) x=Const('x

0熱

1答えて

Z3のシンボリック表現全体をどのように表示するのですか？

私はZ3Pyをいくつかの分析作業に使用していますが、何度も象徴的な表現をプリントアウトしたいと思います。例えば、 a = BitVecVal("test", 32) + 13 print a はしかし、私はZ3表現が非常に大きくなると、それだけで完全にプリントアウトすることができないことがわかります。代わりに、「省略記号は、」どのように私は完全にZ3表現をプリントアウトすることができ、だから