Можем ли мы определить отношения в Z3?

Question

Я новичок в решении z3 SMT. Мне нужно определить отношение, а не функцию. Я имею в виду функцию, которая может возвращать более одного значения. Я посмотрел учебник и ничего не нашел. Я ценю, если вы можете мне помочь в этом отношении.

Спасибо.

Answer 1

Используйте один из логик, поддерживает ArrayEx теорию, которая обеспечивает массива рода и связанные с ними функции для манипулирования массивами. Затем вы можете вернуть свои функции значениям массива, которые могут содержать произвольно много Ints или Bools или что-то еще.

This SMT tutorial - хороший ресурс, который собирает множество деталей SMT в одном месте.

Answer 2

В некотором смысле SMT «естественно» поддерживает реляционное программирование. Вы можете просто отключить возможные значения аргумента и, таким образом, достичь желаемого результата. Что-то вроде:

(declare-fun foo ((Int)) Int) 
(assert (or (= (foo 3) 4) (= (foo 3) 5))) 
(check-sat) 
(eval (foo 3)) ; might produce 4 of 5 
(assert (distinct (foo 3) 4)) 
(check-sat) 
(eval (foo 3)) ; will produce 5 
(assert (distinct (foo 3) 5)) 
(check-sat)  ; will declare unsat 

Here're вы говорите foo применительно к 3, может производить 4 или 5. И тогда вы можете утверждать «дальнейшие» факты, чтобы ограничить пространство по мере необходимости; или оставить его свободным. Вы можете использовать этот трюк, чтобы по существу моделировать foo как отношение; заставляя SMT-решателя вести себя как язык реляционного программирования.

Конечно, как вы действительно хотите заниматься модельными отношениями, действительно зависит от проблемы. Вышеупомянутое может быть не лучшим выбором для вашей проблемы.