Z3 Java API에서 지나치게 엄격한 타이핑이 필요합니까? Z3, 또한 및 기타 유사한 운영자를위한 자바 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한다. 예를 들어, mkITE은 Expr을 반환하지만 if-then-else의 결과가 정수인 경우에도 올바른 Java 클래스가 아니기 때문에 Java API에서 해당 연산을 허용하지 않습니다. (이것은 내 코드에서 실행중인 문제입니다.)

Java API의 무언가가 누락되었거나 (의도하지 않은) 제한입니까?

Answer 1

이것은 제한 사항이 아니며 완전히 의도 된 디자인입니다. 일부 함수는 임의의 Expr을 반환 할 수 있으며, 일부 함수는 더 전문화되어 있고 ArrExpress (Expr에서 파생 됨) 만 반환하고 일부 함수는 더욱 특수화되어 IntExpr을 반환합니다. 예를 들어 mkITE과 같은 함수에서 기대할 수있는 것을 알고 있다면 출력을 원하는 형식으로 캐스팅 할 수 있습니다. 이것이 바람직한 패러다임입니다.

내부적으로 Z3에서 나온 Expr은 API (Expr.create)에서 검사되므로 Java는 모든 Expr의 유형 계층 구조와 해당 요소를 형변환 할 수있는 항목을 알고 있습니다.