Z3 python이 x * 2를 x * x와 다르게 취급합니까?

Question

그것은 Z3 파이썬 인터페이스는 ** 연산자를 좋아하지 않는 것 같다, 그것을 해결할 수있는 X * X가 아닌 X ** 2 당신은 아마 버전 4.3을 사용하는

>>> x,y = x,y=Reals('x y') 
>>> z3.prove(Implies(x -6 == 0,x**2 -36 == 0)) 
failed to prove 
[x = 6] 
>>> z3.prove(Implies(x -6 == 0,x*x -36 == 0)) 
proved 

Answer 1

아래의 예와 같이. Linux 또는 OSX에서는 0입니다. 버전 4.3.0은 이러한 플랫폼에서 구성 문제점이 있습니다. 그렇다면 버전 4.3.1을 다운로드하시기 바랍니다. 버전 4.3.1은 Linux와 OSX 모두에 대한 쿼리를 증명합니다. 버전 4.3.0에서 자동 구성은 Linux 및 OSX에서 기본적으로 활성화되어 있지 않습니다. 따라서 Z3은 항상 비선형 산술 연산을 위해 완전하지 않은 일반 목적의 솔버를 사용하지 않으며 동력 연산자를 지원하지도 않습니다. 자동 구성을 사용하면 Z3에서 이러한 두 가지 문제가 비선형 실수 산술 조각에 있음을 감지하고 nlsat solver으로 전환합니다.

현재 버전 4.3.0에서 수동으로 자동 구성을 사용하려면 z3.set_option(auto_config=True) 명령을 사용할 수 있습니다.