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

Question

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

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

Answer 1

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

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