반복적으로 다른 변수 선언

Question

이 질문은 this 및 this 질문과 관련이 있습니다.

Z3

의 distinct 함수

(declare-const a S) 
(declare-const b S) 
(assert (distinct a b)) 

세트 내의 모든 변수가 서로 다른 값을 취해야한다는 (여기 a 및 b) 등을 변수 집합을 구속 할 수 있습니다.

내 질문은입니다. 변수가 고유해야하는 변수 집합을 명시 적으로 참조하지 않고도 변수가 고유 한 값을 갖도록 설정할 수 있습니까? 예 :

(declare-unique-const a S) 
(declare-unique-const b S) 
(declare-unique-const c S) 

이는 프로그램 검증과 같이 반복적 인 프로세스에서 새로운 변수를 선언 할 때 유용합니다.

가능하지 않은 경우 모든 고유 변수를 추적하고 해당 집합을 사용하여 적절한 distinct (newvar, oldvar1, ..., oldvarn)) 제약 조건을 방출해야합니다.

Answer 1

우리는 Int에 S에서 보조 신선한 기능 f을 정의하고

f(a_1) = 1 
f(a_1) = 2 
f(a_3) = 3 
... 
f(a_n) = n 

그런 다음, a_1이, ..., a_n이 서로 달라야합니다 주장 할 수 있습니다. b도 모두 a_i과 다릅니다. 우리는 단지 주장한다

f(b) = n+1 

이 접근법에서는 카운터를 추적하면된다.