z3py

0熱

1答えて

Pythonでz3でいくつかのCプログラムを分析しようとしていて、ポインタに問題がありました。 float * buffer = (float*)malloc(5*sizeof(float)) 私はそう*bufferはReal()あるべきBitVec(32)値としてバッファ解釈：私のような条件で働いています。それは大丈夫でなければなりませんが、私はプログラムヒープをエンコードするために *

2熱

2答えて

z3pyデータ型/列挙型を文字列と比較する

この例の後に（ここでは：z3py）、私はcを次のように比較できます。 Color.green。私のpython-文字列に cを比較する必要が自分のアプリケーションで Color = Datatype('Color') Color.declare('red') Color.declare('green') Color.declare('blue') Color = Color.create(

3熱

2答えて

Z3 QBFの式をpcnfに直接変換する

私はQ3定理証明（Z3Pyを使う：PythonのZ3 API）を使ってQBF（Quantified Boolean formula）を作成しています。 q3の形式でqbfの式を直接Prenex normal formに変換する方法はありますか？

3熱

2答えて

Z3 Proverが間違った解を返します

私はPythonでZ3 Thoerem Proverを使って方程式を解こうとしています。しかし、私が得る解決策は間違っています。 from z3 import * solv = Solver() x = Int("x") y = Int("y") z = Int("z") s = Solver() s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>

0熱

1答えて

z3py：存在記号の使用法

このスクリプト from z3 import * solver = z3.Solver() x = Int('x') def f(y): return y+y solver.add(x >= 0, x < 10, Exists(x, f(x) == 4)) print solver.check() print solver.model() は私の答えとして sat [x

1熱

1答えて

式に条件式（=>）が含まれているかどうかをチェックする方法

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

1熱

1答えて

z3pyでZ3 EnumSortの値を抽出できません

現在、問題をZ3にエンコードしようとしています。「tristate」ブール型（つまり、true,falseおよびunknownのブール値）をモデル化したいと考えています。ここでが、私はそれをモデル化してきた方法です。 #!/usr/bin/env python import z3 from collections import OrderedDict TristateValues =

4熱

1答えて

Z3の量子トラバースの理解

z3の定量化された数式をトラバースすることを理解しようとしています（私はz3pyを使用しています）。定量化された変数をどのようにピックアップするか分かりません。たとえば、以下のコードでは、私はと同じ式とエラーを表示しようとしています。私はZ3はド・ブラン・インデックスを使用し、私はヴァール（1、BoolSort（））のようなものを取得する必要があることを知るようになった少し検索して from z3

2熱

1答えて

Z3定量化された式の変数の数を数えて

私は数式（Z3pyの定量化された式）ですべての変数を収集しようとしています。小さな例 w, x, y, z = Bools('w x y z') fml = And(ForAll(x, ForAll(y, And(x, y))), ForAll(z, ForAll(w, And(z, w)))) varSet = traverse(fml) iが横断するために使用するコードは def t