나는 잠시 동안 (ML) Z3 바인딩을 사용하고 distinct`

Question

`에 대한 Z3/SMTLIB2 지원, API 함수

val mk_distinct : context -> ast array -> ast 

은 여러 해 동안 충실하게 봉사했다. 을 SMTLIB2 인터페이스로 전환하려고 시도했지만, distinct 명령 은 unsupported입니다. 예를 들어, 쿼리

unsupported 
; distinct 
sat 

웹 데모에 :

(declare-fun x() Int) 
(declare-fun y() Int) 
(distinct x y) 
(assert (= x y)) 
(check-sat) 

는 응답을 얻을 수 있습니다. 몇 가지 해결 방법이 있습니까?

감사합니다.

Ranjit.

Answer 1

(distinct x y) 대신 (assert (distinct x y))을 사용해야합니다. 다음은 업데이트 된 예에 대한 링크입니다. http://rise4fun.com/Z3/uVrX