2016-12-07 17 views
0

ArithExpr秒で行うことができます。Z3 Java APIでの厳密な型指定ですか? Z3、さらに、その他の類似の事業者のためのJava APIで

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クラスは、すべての可能な表現が含まれていないよう。たとえば、mkITEExprを返しますが、if-then-elseの結果が整数であっても、正しいJavaクラスではないため、Java APIはその操作を許可しません。

Java APIの何かが不足していますか、これは(おそらく意図しない)制限ですか?これは、私のコードで実行されている問題です。

+0

ctx.mkITEの結果を(ArithExpr)にキャストできます。 –

答えて

0

これは制限ではなく、完全に意図された設計の選択です。いくつかの関数は任意のExprを返すことができ、いくつかはより特殊化され、(Exprから派生した)ArithExprを返すだけで、さらに特殊化されてIntExprを返すものもあります。 mkITEのような関数(あなたの例のような)から何を期待するのか分かっていれば、出力を望ましい型にキャストすることができます。これが好ましいパラダイムです。

内部的には、Z3から出てくるExprがAPI(Expr.create)でチェックされているので、JavaはすべてのExprの型階層とキャスト可能なものを知っています。

関連する問題