Как объявить или проверить функцию «один к одному»?
В C ++ API z3 функция описывается следующим образом:
func_decl f = function("f", I, I, I);
что означает, что функция принимает данные (int, int) и возвращается int,
Могу ли я объявить функцию «один к одному» (биективная) или я могу заставить функцию быть «один к одному» (биективную)?
Решение
Насколько я знаю, не существует встроенного способа объявления функции биекцией. Вы можете сделать аксиоматизацию самостоятельно, однако:
(declare-sort X)
(declare-sort Y)
(declare-fun f (X) Y)
(assert (forall ((y Y))
(exists ((x X))
(and
(= (f x) y)
(forall ((z X))
(implies
(not (= x z))
(not (= (f z) y))))))))
И используйте его следующим образом:
(declare-const x1 X)
(declare-const x2 X)
(declare-const y1 Y)
(declare-const y2 Y)
(assert (= (f x1) y1))
(check-sat) ; sat
(push)
(assert (= (f x2) y1))
(check-sat) ; sat
(pop)
(assert (not (= x1 x2)))
(check-sat) ; sat
(push)
(assert (= (f x2) y1))
(check-sat) ; unsat
(pop)
Попытайся онлайн здесь.
Я не уверен, как производительность этой кодировки. Чередующиеся квантификаторы часто вызывают проблемы при автоматическом доказательстве теорем, а приведенная выше аксиома даже не имеет паттернов / триггеров. Я догадываюсь, что аксиома в порядке, если вы предоставляете «достаточно» информации, например, x1, x2, (= (f x1) y1) а также (not (= x1 x2)), Я не уверен, насколько хорошо поиск моделей будет работать здесь, хотя.
Другие решения
Других решений пока нет …