Когда вы объявляете datatype следующим образом:
(declare-datatype Barrier
((barrier (proc Int)
(rank Int)
(group Int)
(complete-time Int))))
, вы генерируете вселенную, которая генерируется «свободно». Это просто причудливое слово, означающее, что для каждого возможного элемента в декартовом произведении есть значение Barrier Int x Int x Int x Int.
Позже, когда вы скажете:
(assert
(forall ((b1 Barrier) (b2 Barrier))
(=> (= (group b1) (group b2))
(= (complete-time b1) (complete-time b2)))))
you утверждаете все возможные значения b1 и b2, и вы говорите, что если группы совпадают, то время завершения должно быть одинаковым. Но помните, что типы данных генерируются свободно, поэтому z3 сообщает вам unsat, что означает, что ваше утверждение явно нарушается при выборе правильных значений b1 и b2 из этого декартового произведения, в котором множество пар жителей, нарушающих это утверждение .
То, что вы пытались сказать, конечно, было: «Я просто хочу, чтобы вы обратили внимание на те элементы, которые удовлетворяют этому свойству. Меня не волнуют другие». Но это не то, что вы сказали. Для этого просто включите ваше утверждение в функцию:
(define-fun groupCompletesTogether ((b1 Barrier) (b2 Barrier)) Bool
(=> (= (group b1) (group b2))
(= (complete-time b1) (complete-time b2))))
, затем используйте ее в качестве гипотезы ваших последствий. Вот глупый пример:
(declare-const b00 Barrier)
(declare-const b01 Barrier)
(assert (=> (groupCompletesTogether b00 b01)
(> (rank b00) (rank b01))))
(check-sat)
(get-model)
Это печатает:
sat
(model
(define-fun b01 () Barrier
(barrier 3 0 2437 1797))
(define-fun b00 () Barrier
(barrier 2 1 1236 1796))
)
Это не особенно интересная модель, но, тем не менее, это правильно. Я надеюсь, что это объясняет проблему и устанавливает правильный путь к модели. Вы можете использовать этот предикат в сочетании с другими фактами, и я подозреваю, что в сценарии sat это действительно то, что вы хотите. Итак, вы можете сказать:
(assert (distinct b00 b01))
(assert (and (= (group b00) (group b01))
(groupCompletesTogether b00 b01)
(> (rank b00) (rank b01))))
, и вы получите следующую модель:
sat
(model
(define-fun b01 () Barrier
(barrier 3 2436 0 1236))
(define-fun b00 () Barrier
(barrier 2 2437 0 1236))
)
, которая сейчас становится более интересной!
В общем, пока SMTLib поддерживает квантификаторы, вы должны стараться держаться подальше от них настолько, насколько это возможно, так как логика c становится полуразрешимой. И вообще, вы хотите писать только количественные аксиомы, как вы делали для неинтерпретированных констант. (То есть, вводите новую функцию / константу, пусть она не интерпретируется go, но утверждается универсально выраженная аксиома, которой она должна удовлетворять.) Это может позволить вам смоделировать кучу интересных функций, хотя квантификаторы могут заставить решатель реагировать unknown, поэтому их лучше избегать, если вы можете.
[Примечание: Как правило, когда вы пишете количественную аксиому над свободно сгенерированным типом данных (например, вашим барьером), он либо быть тривиально верным или никогда не будет удовлетворен, потому что вселенная буквально будет содержать все, что может быть построено таким образом. Думайте об этом как о типе данных в Haskell / ML et c .; где это не что иное, как контейнер всех возможных значений.]