Определение функции в Z3 ее реализацией Java?

Question

Вот что я пытаюсь сделать.

Допустим, я хочу найти значение op используя Z3 (и его Java-привязку) в выражении, похожем на это:

((exists (op Int)) (= (foo op) 2)

Поэтому я хочу вызвать функцию foo на op переменная и проверьте, для каких значений op будет возвращена функция 2. Я хочу определить функцию foo в Java и подумал, что для Z3 существует способ доступа к этим определениям функций. Я хочу сделать это так, потому что функции на самом деле являются поисками в HashMap, который легко реализовать в Java.

Так как я новичок в SMT-решениях в целом, возможно, я захочу сделать что-то, что невозможно сделать. Так что я открыт для всех предложений по теме.

Заранее спасибо за ваше время и ответы!

Answer 1

Это было бы очень хорошо иметь, но в настоящее время Z3 не может использовать определения функций из других языков /API. Для случая таблиц поиска это должно быть легко, потому что они могут быть легко закодированы как каскадные операции типа if-then-else, например, следующим образом:

;; define foo
(define-fun foo ((x Int)) Int
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply skip)

производит

(goal
  (exists ((op Int)) (= (ite (= op 1) 42 (ite (= op 2) 43 78)) 43))
  :precision precise :depth 0)
)

(и это решается быстро тоже.)

Самый простой способ сделать это через API - это установить проблему с объявлением функции, а затем предоставить определение макроса через универсальный квантификатор, который распознается macro-finder тактика:

;; declare foo
(declare-fun foo ((Int)) Int)

;; define foo
(assert (forall ((x Int)) (= (foo x)
    (ite (= x 1) 42
    (ite (= x 2) 43
    ;; ...
                 78)))))

;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply macro-finder) ;; replaces foo with it's definition

Чтобы макро-искатель мог выбрать определение функции, квантификатор должен иметь вид

(forall ((x ...)) (= (foo x) (... definition ...))