z3 - 優秀な図書館

z3

1熱

1答えて

intの変数番号を持つ長いSumを作成するにはどうすればよいですか？ expr mk_add(expr_vector args) { vector<Z3_ast> arr; for (int i = 0; i < (int)args.size(); i++) arr.push_back(args[i]); return to_expr(args.ctx()

0熱

2答えて

未解決の用語を代表するものからz3の用語に進む方法はありますか？

私はC++ APIを使用しています。私はそのタイプの未解釈の用語x、y、zを作成します。モデルを印刷すると、次のようになります。これは基本的に、各用語の内部担当者を印刷しています。 x: USORT!val!0 y: USORT!val!0 z: USORT!val!1 私の質問は：私はすぐに代理人になることができますか？ repr_to_term(USORT!val!0) => [x,

1熱

1答えて

Z3のconst配列から値を抽出する

私の質問は、Z3 C/C++ APIでは、Z3によって生成されたモデルから（インデックス、値）のペアを取得する方法です。私はしかし、そのソリューションは、常に私のために動作しません Read func interp of a z3 array from the z3 model 、同じ問題が発生しました。 assert(Z3_get_decl_kind(c, some_array_1_eval_

0熱

1答えて

コールはZ3_astオブジェクトが削除されたときのために戻ってありますか？

私は、私は参照カウントやメモリ管理を心配する必要はありませんZ3のためのC++ APIを使用しています。しかし、私はstd::map<Z3_ast, some_struct>の線に沿ってのstd ::マップを使用してZ3のASTに対する情報を保存したいと思います。特定のZ3_astオブジェクトが削除された場合、このマップからそのエントリを削除します。 Z3_astオブジェクトの参照カウントが

0熱

1答えて

Z3 Java APIでの厳密な型指定ですか？ Z3、さらに、その他の類似の事業者のためのJava APIで

はArithExpr秒で行うことができます。 ArithExpr x = ctx.mkInt(0); ArithExpr y = ctx.mkInt(1); // Compiles: ctx.mkAdd(x, y); // Does not compile: ctx.mkAdd((Expr) x, (Expr) y); しかしArithExpr Javaクラスは、すべての可能な表現が

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

1熱

1答えて

アサーションがz3pyの場合

これはz3pyの新しいユーザーです。私は IF room.temp < 18 THEN room.fireplace = on IF room.temp > 24 THEN room.fireplace = off IF room.CO > 180 THEN room.fireplace = off IF room.temp > 28 THEN house.hvac = off IF ho

0熱

1答えて

不正な結果を与えるZ3 .NET APIでの最適化 - バグ？

私はZ3用の.NET APIを使用していますが、コードを使用して奇妙な動作（おそらくオプティマイザのバグ）を発見しました。最適化クラスで実行すると、解決策が誤って検出されますが、ソルバークラスで実行すると、実行不可能と正しくレポートされます。誰でも私の声明を検証するコードを実行してもらえますか？何が起こっているかについてのヒントは高く評価されます。種類がマレク using System; u