배열을 포함하는 구문 분석 및 저장

Question

파일에 배열과 관련된 두 개의 정수 계산식이 있습니다. 각 표현식을 메모리에 저장하는 가장 좋은 방법은 무엇입니까? 등식이 구문 상 동등해진다. 그 구조를 비교해 보면 동등성을 찾을 수 있습니다. 동등성을 먼저 확인하려면 구조가 동일하면 같고 그렇지 않으면 SMT 솔버를 사용하십시오.

Ex. a [i + 2] +5 및 a [i + 3-1] + 4 + 1은 동등하다.

현재 i는 a [i] = b [i] + z를 wr (a, i, rd (b, i) + z)로 나타냅니다. 여기서 Write (wr) 및 Read (rd)는 함수입니다.

Answer 1

당신이 묻는 것을 이해하기가 약간 어렵습니다. 그러나 배열 이론은 이미 읽기/쓰기 작업을 지원합니다. 당신은 예를 들어 아래로 넣어 평등은 다음과 같이 구분 될 수있다 : 이것은 평등은 모든 배열 a 마찬가지입니다 것을 증명 unsat가 발생합니다

(set-logic AUFLIA) 

(declare-const i Int) 
(declare-const a (Array Int Int)) 

(define-fun eq() Bool (= (+ (select a (+ i 2))  5) 
          (+ (select a (+ i (- 3 1))) (+ 4 1)))) 

; To prove equivalence, assert the negation and make sure the result is unsat: 
(assert (not eq)) 

(check-sat) 

. (우리는 평등의 부정을 주장하고 있습니다.)

이것은 당신이 쓴 것입니까?