でもJava APIを使用しています。これは、この警告のための最小限の作業例です:Z3は、仮定が命題変数ではなく、実際には
の 否定でなければならない。この小さなプログラムのためにWARNING::仮定が命題変数または1
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
Solver solver = ctx.mkSolver();
BoolExpr a = ctx.mkBoolConst("a");
BoolExpr b = ctx.mkBoolConst("b");
BoolExpr and = ctx.mkAnd(a,b);
solver.check(and);
、Z3はそれを訴え
私が何かを誤解しない限り、and
は命題変数です。なぜこの警告があるのか理解できません。さらに、check
メソッドはパラメータとしてBoolExpr
の配列をとります。なぜ命題変数が必要ですか?
私の質問:この警告を無視していいですか?