Упрощение интерпретации функций в модели

Question

В SMT: check uniqueness and totality of function Я дал функцию аксиоматизации и спросил Z3 для модели. Однако, поскольку решение чего-то с квантификаторами в нем неразрешимо вообще, Z3 раз лишается.

Вот модифицированная версия, в которой в случае «ИНТ» моделируется как одно значение:

(declare-datatypes() ((ABC int error none))) 
(declare-fun f (ABC ABC) ABC) 
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f none x) none)))) 
(assert (forall ((x ABC)) (=> (or (= x int) (= x error) (= x none)) (= (f x none) none)))) 
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f error x) error)))) 
(assert (forall ((x ABC)) (=> (or (= x int) (= x error)) (= (f x error) error)))) 
(assert (forall ((x ABC) (y ABC)) (=> (and (= x int) (= y int)) (= (f x y) int)))) 
(check-sat) 
(get-model) 

Потому что теперь конечное число случаев, Z3 дает ответ быстро:

sat 
(model 
    (define-fun k!26 ((x!0 ABC)) ABC 
    (ite (= x!0 error) error 
    (ite (= x!0 int) int 
     none))) 
    (define-fun f!28 ((x!0 ABC) (x!1 ABC)) ABC 
    (ite (and (= x!0 error) (= x!1 int)) error 
    (ite (and (= x!0 int) (= x!1 error)) error 
    (ite (and (= x!0 error) (= x!1 error)) error 
    (ite (and (= x!0 int) (= x!1 int)) int 
     none))))) 
    (define-fun k!27 ((x!0 ABC)) ABC 
    (ite (= x!0 error) error 
    (ite (= x!0 int) int 
     none))) 
    (define-fun f ((x!0 ABC) (x!1 ABC)) ABC 
    (f!28 (k!27 x!0) (k!26 x!1))) 
) 

Оба k!26 и k!27 фактически просто возвращают свой вход (это легко увидеть, проверив все три случая). Можно ли упростить модель, устранив эти две функции автоматически?

Оптимально я хотел бы иметь что-то вроде следующего, хотя я вижу, что не может быть возможным:

(define-fun f ((x!0 ABC) (x!1 ABC)) ABC 
    (ite (or (= x!0 none) (= x!1 none)) none 
    (ite (or (= x!0 error) (= x!1 error)) error 
    int))) 

Я использую Z3Py, но как общие Z3-специфические и Z3Py специфические ответы приветствуются ,

Answer 1

Я не думаю, что вы можете сделать так, чтобы руководство Z3 обеспечивало «более простой» ответ здесь; поскольку создаваемая модель зависит от того, как было сделано доказательство, и даже простые изменения проблемы могут иметь непредсказуемые результаты. В частности, модель, которую вы получите, может измениться со следующей версией Z3.

Сказав это, общий трюк составляет eval терминов в модели. Поскольку ваша текущая проблема связана только с конечным доменом, вы можете ее перечислить. Если добавить следующие строки в конце сценария:

(eval (f int int)) 
(eval (f int error)) 
(eval (f int none)) 
(eval (f error int)) 
(eval (f error error)) 
(eval (f error none)) 
(eval (f none int)) 
(eval (f none error)) 
(eval (f none none)) 

Тогда Z3 напечатает:

int 
error 
none 
error 
error 
none 
none 
none 
none 

Может быть, вы можете использовать этот вывод для построения «проще» модель самостоятельно. Конечно, это работает только в том случае, если домен конечен; но вы можете использовать тот же трюк, чтобы оценить «интересные» части входного домена, в зависимости от вашей проблемы.