z3의 기호 변수

Question

z3 솔버가 "기호화 된"솔루션을 생성 할 수있는 방법이 있습니까? 예를 들어, 방정식 :

1 + X = C

용액 X = C-1이지만, Z3 [c = 0, x = -1] 항상 같은 특정 모델을 방출한다. c를 기호 변수로 "정의"하는 방법?

Answer 1

불행히도 Z3은 이러한 종류의 기능을 드러내지 않습니다. 내부적으로는 솔버를 사용하지만 API에서는 노출되지 않습니다. 향후 버전에서는 솔버, Grobner베이스 프로 시저 등의 내부 구성 요소를 공개하려고합니다. 현재 버전에서는 solve-eqs이라는 전략이 있습니다 (http://rise4fun.com/Z3Py/tutorial/strategies 참조). 가우스 제거의 일반화를 사용하여 변수를 제거합니다. 그러나 이것은 전처리 단계이므로 제거 할 변수를 제어 할 수 없습니다.