저는 z3을 C++ 라이브러리로 사용하고 있습니다. 내 현재 프로그래밍 프로젝트에서 부울 수식을 가지고 있는데 z3을 사용하여 단순화했습니다.z3 C++ API : expr 연산하기
내 프로젝트에서 단순화 된 방정식을 사용하려면 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
"수식 가져 오기"란 무엇을 의미합니까? A (수학) 방정식에는 항상'=='이 있습니다. – user463035818
무슨 뜻인지 명확히하기 위해 질문을 업데이트했습니다! – toebs