1
전 집합을 보편적으로 정량화 된 의미로 설정 한 관계 및 연산으로 인코딩 집합입니다. 단항 조건 자 p (예 : v < 4, v> 4, ..)를 만족하는 요소를 선택하여 새 세트를 생성하는 세트에 대해 선택 연산자를 사용합니다. 이 연산자로 인해, 내 수식에 간단한 산술 술어가 있습니다. 이러한 식의 예 Z3 부호화 아래 주어진 - 예상대로평등 및 부등식이있는 EPR 수식
(set-option :mbqi true)
(set-option :model-compact true)
;; Rmem and Rmem1 are sets of Int
(declare-fun Rmem (Int) Bool)
(declare-fun Rmem1 (Int) Bool)
(declare-const v Int)
(declare-const v1 Int)
(declare-const x Int)
;; Rmem = Rmem1 U {x}
(assert (forall ((n Int)) (= (Rmem n)(or (Rmem1 n) (= n x)))))
;; Select(m<v1) from Rmem1 = {}
(assert (forall ((m Int)) (= false (and (Rmem1 m) (< m v1)))))
(assert (or (< v x) (= v x)))
(assert (or (< v v) (= v v1)))
(assert (exists ((q Int)) (and (Rmem q) (< q v))))
(check-sat)
(get-model)
, Z3는 UNSAT은 상기 화학식에 대해 반환한다. 그러나 제 질문은 -
- 내 prenex 정규 형식으로 수식을 쓸 수 있다고 가정하면, 여전히 EPR 클래스에 있습니까?
- 그러한 공식은 결정 가능한가? z3은 그러한 공식에 대한 의사 결정 절차입니까? 수식을 결정할 수 있도록 내 조건을 어떻게 제한해야합니까?
업데이트 - 위 공식 집합은 관계형 대수의 결합 쿼리로 표현할 수 있지만 부등식이 있습니다.