일반 목록의 길이 함수

This post은 Z3의 기본 제공 목록에 길이 함수를 공리화하는 방법을 보여줍니다. 그러나이 함수는 정렬 관련 (여기서는 Int)이며 bool 또는 사용자 지정 정렬 목록에는 적용되지 않습니다.일반 목록의 길이 함수

; declare len as an uninterpreted function 
(declare-fun len ((List Int)) Int) 

; assert defining equations for len as an axiom 
(assert (forall ((xs (List Int))) 
    (ite (= nil xs) 
    (= 0 (len xs)) 
    (= (+ 1 (len (tail xs))) (len xs)))))

정렬 - 제네릭 목록 기능을 가장 똑똑하게 인코딩하는 방법은 무엇입니까? (올바르게 기억한다면 함수 자체는 일반적인 것이 될 수 없다).

출처

2012-06-19 Malte Schwerhoff

SMT 2.0 스크립트의 매개 변수 적 공리를 지원하지 않습니다. 한 가지 대안은 프로그래밍 방식의 API를 사용하는 것입니다. 주어진 정렬에 대해 len 공리를 만드는 함수를 만들 수 있습니다. 다음은 Python API를 사용하여이를 수행하는 방법에 대한 예제입니다.

http://rise4fun.com/Z3Py/vNa

from z3 import * 
def MkList(sort): 
    List = Datatype('List') 
    List.declare('insert', ('head', sort), ('tail', List)) 
    List.declare('nil') 
    return List.create() 


def MkLen(sort): 
    List = MkList(sort) 
    Len = Function('len', List, IntSort()) 
    x = Const('x', List) 
    Ax = ForAll(x, If(x == List.nil, Len(x) == 0, Len(x) == 1 + Len(List.tail(x)))) 
    return (Len, [Ax]) 

IntList = MkList(IntSort()) 
IntLen, IntLenAxioms = MkLen(IntSort()) 
print IntLenAxioms 
s = Solver() 
l1 = Const('l1', IntList) 
s.add(IntLenAxioms) 
s.add(IntLen(l1) == 0) 
s.add(l1 == IntList.insert(10, IntList.nil)) 
print s.check()

출처

2012-06-19 15:15:11

stdio에서 프로그래밍 API로 전환해야하는 것처럼 보입니다 ... 감사합니다. –

그 밖의 것이 있습니다 : 그러한 정의 방정식을 패턴으로 보호해야합니까? 나는 보통 정량화 된 공리 (axioms)로 할 것입니다. 또한 가이드는 모 형 파인더가 가상 매크로를 정의하는 수량 기호를 자동으로 감지한다고 말합니다. 나는 이것이 : mbqi가 사실 일 것을 요구한다고 가정한다 (그것은 나의 경우에는 아니다). 이걸 조금 더 자세히 설명해 주시겠습니까? –

패턴을 제공하지 않으면 Z3에서 패턴을 제공합니다. 'Len' 공리는 "재귀적인"정의이기 때문에 의사 매크로가 아닙니다. 옵션 : mbqi는 기본적으로 true입니다. –

당신은 그것을위한 일종의을 사용할 수 있습니다. len 함수는 사용자 정의 정렬 T의 일반 목록을 통해 정의됩니다. 처음에만 define-sort은 에서 Int 유형으로 연결됩니다.

(define-sort T() Int) 
(define-sort MyList() (List T)) 

(declare-const listlen Int) 
(declare-const a MyList) 
(declare-const b MyList) 
(declare-const c MyList) 
(declare-const d MyList) 
(declare-const e MyList) 

(define-fun-rec len((l MyList)) Int 
    (ite 
     (= l nil) 
     0 
     (+ (len (tail l)) 1) 
    ) 
) 
(assert (= a nil)) 
(assert (= b (insert 2 a))) 
(assert (= c (insert 8 b))) 
(assert (= d (insert 6 c))) 
(assert (= e (insert 10 d))) 

(assert (= listlen (len e))) 

(check-sat) 
(get-model)

출처

2017-11-30 12:42:02 Julian

일반 목록의 길이 함수

답변

관련 문제