Z3は、仮定が命題変数ではなく、実際には

Question

でもJava APIを使用しています。これは、この警告のための最小限の作業例です：

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の配列をとります。なぜ命題変数が必要ですか？

私の質問：この警告を無視していいですか？

Answer 1

いいえ、andは命題変数ではありませんが、命題項（言い換えればBoolExpr）です。 solver.check(...)の仮定リテラルは変数または変数の否定、すなわちaまたはnot aである必要がありますが、a and bではなく、変数の否定である必要があります。

この警告は無視しても意味がありません.Z3がこれらの前提を無視する、つまり予期しない結果が生じる可能性があるためです。

ただ、混乱を避けるために：solver.check(...)への引数は仮定リテラルで、彼らはアサーションはない、つまり、我々はandが充足可能かどうかを確認したい場合は、まずそれを主張して、チェックするためにソルバーを依頼する必要がありますさらなる仮定なしに、例えば、

... 
solver.assert(and); 
solver.check();