Z3의 문서화되지 않은 삼각 함수가 복구 가능합니까?

Question

공식적으로 Z3에는 trig가 지원되지 않습니다. 예를 들어 this question 또는 this one을 참조하십시오. 그러나 Z3에는 문서화되지 않은 삼각 함수 연산자가 있습니다. 예를 들어 regression tests에 사용됩니다. pi이라는 내장 기호가 있습니다.

sat 
((x (- 1.0))) 

이러한 연산자가 잘 작동하지 않습니다 Z3도

(declare-fun x() Real) 
(assert (= (cos pi) x)) 
(check-sat) 
(get-value (x)) 

함께 다시 온다 :, 이러한 연산자와 예컨대 일부 사소한 교정을 할 수 있습니다. 예를 들어,이 작은 입력 파일 Z3 4.4.1와 독방 감금 오류가 발생할 것입니다, 또는 (현재) this commit로 마스터 지점과 메모리 사용량의 급격한 폭발의 원인 :

(declare-fun x() Real) 
(assert (< (sin x) -1.0)) 
(check-sat) 

내가 놀라지 아니에요 팀이 존재하지 않는다고 말하는 문서화되지 않은 기능은 작동하지 않습니다. 내 질문은 : 그들이 수정할 수 있습니까? 어떤 수준의 성능이 Z3에 합리적인 추가가 될 것입니까? 나는 해석되지 않은 함수와 삼각 함수의 ID를 사용하여 Z3으로 여러 가지 삼각 함수 증명을 할 수 있다는 것을 알고 있습니다. Z3 팀 중에 이것에 관심이 있습니까?

Answer 1

감사합니다. 그런 경우 Z3이 충돌하지 않아야합니다. 이러한 작업을 처리하는 것이 더 우아해야합니다. 나는 지금 이것에 대한 수정을 조사했다, 9b91e6f..cb29c07. OTOH, 그러한 연산자에 대한 이론은 본질적으로 없다. 예를 들어, Z3은 죄 영역을 알지 못합니다. 당신은 그러한 성질을 당신 스스로 공리화해야 할 것입니다. Z3은 (부분) 결정 프로 시저 지원이없는 내장 함수를 사용할 때 "알 수 없음"(또는 "unsat"이지만 "sat"가 아님)을 반환합니다.