Функция длины для общих списков

This post показывает, как аксиоматизировать функцию длины для встроенных списков Z3. Однако функция специфична для сортировки (здесь Int) и не относится к спискам bools или пользовательских сортов.Функция длины для общих списков

; 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 или Z3 do не поддержка параметрических аксиом в скриптах SMT 2.0. Один из вариантов - использовать программные API. Вы можете создавать функции, которые создают аксиому len для данного сорта. Вот пример того, как это сделать, используя API Python.

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 раньше, чем я думал ... спасибо! –

Что-то еще: нужно ли охранять такие определяющие уравнения с узорами? Как я обычно делал с количественными аксиомами. Кроме того, в руководстве говорится, что кванторы, определяющие псевдомакросы, автоматически обнаруживаются с помощью Finder модели. Я предполагаю, что для этого требуется: mbqi быть истинным (что не в моем случае). Не могли бы вы немного рассказать об этом? –

Если мы не предоставим шаблоны, Z3 вычислит их для нас. Аксиома «Лен» не является псевдомакро, потому что это «рекурсивное» определение. Опция: mbqi по умолчанию является true. –

Вы можете использовать то для этого. Функция len определена в общем списке пользовательского типа T. Только первые define-sort ссылки T на тип 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

Функция длины для общих списков

ответ

Смежные вопросы