z3 C++ API : expr 연산하기

Question

저는 z3을 C++ 라이브러리로 사용하고 있습니다. 내 현재 프로그래밍 프로젝트에서 부울 수식을 가지고 있는데 z3을 사용하여 단순화했습니다.

내 프로젝트에서 단순화 된 방정식을 사용하려면 lhs, rhs 및 단순화 된 방정식의 연산이 필요합니다.

예를 들면 : -> X

expression.arg(0) 

식 (엑스 == 3) & & (X < 5) (X == 3) Z3

(= x 3) 

좌 인수로 간략화 rhs 인수 -> 3

expression.arg(1) 

작업 (=)을 어떻게 얻을 수 있습니까?

1 개 이상의 인수가있는 모든 expr에 조작 권한이 있어야합니다.

3 시간 내로 API를보고 있는데 그 사실을 알 수 없습니다.

바라건대, 누구나 올바른 방향으로 나를 가리킬 수 있습니다! Z3의

감사 Toebs

Answer 1

는 "정상"수준의 연산자를 얻으려면 즉, 원래의 "and"에 대해 문자열을 사용하면 다음과 같이 사용할 수 있습니다.

expression.decl().name().str() 

Answer 2

기능 응용 프로그램은 인수의 벡터와 함수 선언으로 표시됩니다. 예를 들어, f 함수가 x 및 y 인수에 적용된다고 가정하십시오. C++ API에서 이것은 e.num_args() 인수를 가진 expr 객체 e의 모양을 취하고 x, y은 e.arg(0), e.arg(1) 및 이 이러한 인수에 적용됩니다.

(그들은 일정 기능의 응용 프로그램이기 때문에 분명히 이것은 또한, 자주 API의 다양한 부분에서 const라고 0 인수에 적용됩니다.)