Z3 Java API의 심볼 생성

Question

저는 Z3을 처음 사용합니다. 질문이 너무 쉽다면 실례합니다. 나는 Z3 Java API에서 상수를 회피하는 두 가지 질문을 가지고있다.

1. 내부적으로 상수 생성이 어떻게 발생합니까? 나는 결국`INTERNALmkStringSymbol가 '나는 소스를 볼 수 없습니다 기본이기 때문에 지금이 라인 long var3 = INTERNALmkStringSymbol(var0, var2);

에 var3에서 변수를 생성 Native.mkStringSymbol(var1.nCtx(), var2)를 호출 public StringSymbol mkSymbol(String) 아래로 public BitVecExpr mkBVConst(String, int)를 추적하여 시작 것을 이해합니다. 나는 그것이 어떻게 작동하는지 궁금해. 아무도 그것이 어떻게 작동 하는지를 압니까? 어디에서 소스를 볼 수 있습니까?

2. 또 다른 혼란스러운 점은 API를 사용하는 상수의 범위 지정입니다. 대화식 Z3에서는 일치하는 푸시 및 팝을 통해 유지되지만 API를 통해 범위 지정이 정의되고 관리되는 방법을 잘 모르겠습니다.

모든 통찰력이나 지도력을 바랍니다.

Answer 1

1. Z3은 오픈 소스이므로 https://github.com/z3prover/z3.git에서 소스를보고 다운로드 할 수 있습니다. Z3의 기호는 src/util/symbol.h에 정의되어 있습니다. 기호가 LISP 아톰과 비슷하다는 것을 알 수 있습니다. 즉, dll의 수명을 통해 지속되며 고유합니다. 그래서 같은 이름의 두 심볼은 포인터가 같을 것입니다. Java API는 src/api/z3_api.h에 선언 된 C API를 호출합니다. 디렉토리 src/api는 기호를 작성하는 API 함수를 포함하여 API 함수를 포함합니다. mkBVConst와 같은 표현식 상수를 만들면 포인터 고유의 표현식이됩니다 (동일한 mkBVConst를 두 번 작성하면 관리되지 않는 포인터가 동일하게됩니다.) Java 포인터는 동일하지 않지만 평등성 테스트는 모두를 악용합니다 이의).
2. Solver 객체에는 push 및 pop 메서드가 있습니다. 솔버 객체에 제약 조건을 추가 할 수 있습니다. 제약 조건의 수명은 푸시/팝 네 스팅 (pop/pop nesting)에 따릅니다. 제약 조건은 제약 조건이 추가 된 범위를 제거하는 팝이있을 때까지 활성화됩니다.