Вот один из способов:
(declare-sort Person 0)
(declare-fun parentOf (Person Person) Bool)
(declare-fun loves (Person Person) Bool)
(assert
(forall ((x Person) (y Person))
(=> (parentOf x y)
(loves x y))))
(check-sat)
(get-model)
z3 говорит:
sat
(model
;; universe for Person:
;; Person!val!0
;; -----------
;; definitions for universe elements:
(declare-fun Person!val!0 () Person)
;; cardinality constraint:
(forall ((x Person)) (= x Person!val!0))
;; -----------
(define-fun loves ((x!0 Person) (x!1 Person)) Bool
false)
(define-fun parentOf ((x!0 Person) (x!1 Person)) Bool
false)
)
По сути, z3 говорит нам, что наши ограничения выполнимы (в этом смысл вывода sat) и a (примечание: не ) с удовлетворительным заданием - это вселенная, в которой есть:
- Именно один человек по имени
Person!val!0 - Никто никого не любит
- Никто не является родителем кого-либо еще
, который явно удовлетворяет всем ограничениям, но, возможно, не самая интересная модель там. Если вы утверждаете дальнейшие факты, вы можете получить более богатые модели. (Например, вы можете сказать, что есть по крайней мере 5 человек, что никто не является их собственным родителем, родительские отношения не симметричны c, все любят себя и т.д. c. В зависимости от того, что именно вы пытаетесь смоделировать .)
Имейте в виду, что решатели SMT не годятся для работы с квантификаторами. В то время как подобные заявления будут работать просто отлично, широкое использование квантификаторов и логик первого порядка c приведет к тому, что теории окажутся на полуразрешимой территории, т. Е. Z3 может в итоге сказать unknown. Решатели SMT лучше всего подходят для комбинаций теорий без количественных показателей, таких как арифметика c, массивы, типы данных и т. Д. c. Для таких проблем Prolog, вероятно, является лучшим выбором для целей моделирования.