問題タブ [sat-solvers]

z3 SMT ソルバーは初めてです。関数の代わりにリレーションを定義する必要があります。複数の値を返すことができる関数を意味します。チュートリアルを調べましたが、何も見つかりませんでした。この点で私を助けていただければ幸いです。

どうもありがとう。

私は sat4j ソルバーがまったく初めてで、ブール値の満足可能な問題を研究しています。そして私は立ち往生しています。ブール式の整数変数を解くプログラムを作りたいです。

x1 < x2 + x3 ユーザーがその数式を入力すると、私のプログラムは x1 = 5 、 x2 = 3 、 x3 = 4 のようにこの数式を満たします (true を返します)。したがって、数式は true を返し、ユーザーは数式を満たすこの整数値を取得します。私はJavaでEclipseで作業しているため、sat4jで作成することは可能です。

stackoverflow-ers(?)、

私はz3で遊んでいて、次の制限を解決しようとしています:

これらの制約にはいくつかの問題があります: a) 最初の問題は、z3 が「制限 #2」を無視していることです。

、私が得る値は次のとおりです。

制限にもかかわらず、F*B = D です。

b）「制限＃1」のコメントを外した場合

私は次の結果を得ています：

それは椅子 - キーボード インターフェイスのバグですか? 私は何を間違っていますか？

これを Z3 オンラインで実行します。

前もって感謝します！

Z3 の Python バインディングを使用して、属性が関数である Z3 データ型を作成しようとしています。たとえば、次のように実行します。

これは、int から bool への関数を取得するために(が type の変数である場合)呼び出すことができる、Fooattributeを使用してデータ型を作成しようとする試みです。my_functionmy_function xxFoo

ただし、2 行目で次のエラーが発生します。

おそらく別の構文を使用して、関数を属性として Z3 データ型を宣言することは可能ですか?

それとも許されないものですか？z3の事後関数宣言は、Z3 では高階関数が許可されていないことを示唆しているため、これらのデータ型を使用した高階関数の作成を防ぐために、データ型に関数を追加することは許可されていない可能性があります。

http://amit.metodi.me/research/bee/から bumblebee sat-solver をコンパイルしようとしています。SWI-Prolog と MinGW を既にインストールしていますが、cmd に「make-minisat」と入力すると、次のようになります。

g++ がプロローグ ヘッダー ファイルに到達できないようです。何か案は？私はwin 10、64ビットで作業しています。