Как я могу определить функцию в z3 Python API после появления нового стандарта SMT-LIB?

Question

Новый стандарт SMT-LIB допускает команду определения функции в форме:

      (define-fun f ((x1 σ1) · · · (xn σn)) σ t) 

В спецификации уточняется, что это семантически эквивалентно

      (declare-fun f (σ1 · · · σn) σ)
(assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

На данный момент я бы определил функцию с использованием Python z3 API следующим образом:

      s = z3.Solver()
f = z3.Function("f", [σ1 ... σn, σ])
s.add(z3.ForAll([x1, ...,xn], t == f(x1, ..., xn)))

Это канонический способ сделать это или есть более простой или эффективный способ справиться с этим?

Answer 1

Обычно вместо этого просто используют функцию Python. Эта функция возвращает результат в терминах своих символических входных данных, таким образом разворачивая определение еще до того, как z3 его увидит.

Единственным исключением является случай, когда вы хотите определить рекурсивную функцию, завершение которой зависит от символического аргумента. Обратите внимание, что вы можете использовать ту же возможность, даже если ваша функция не является рекурсивной, что может решить вашу проблему с определениями, полученными из других источников. Для получения дополнительной информации см . RecAddDefinition.