Z3 4,0 Extra Выход в модели

Question

Когда я пытаюсь получить модель строки, наряду с переменными, которые я определяю, я получаю дополнительный выход в модели как -

z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0 

Я хочу знать, что это ошибочный результат? Или это некоторые промежуточные переменные, которые используются Z3?

Поскольку значения для переменных, которые я определил, для меня все в порядке. Я раньше не видел такого выхода, поэтому у меня возникло это сомнение.

Answer 1

Z3 имеет несколько этапов предварительной обработки. Некоторые из них вводят новые переменные. Новые переменные обычно удаляются из полученной модели. Если это не так, это ошибка. Однако эта ошибка не влияет на правильность. Это просто неудобство.

Было бы здорово, если бы вы могли опубликовать свои проблемы. Мы могли бы определить, какой шаг предварительной обработки не устраняет введенные вспомогательные переменные.

Answer 2

Я понимаю, что это старая тема, но я обнаружил, что у меня такая же «ошибка», как ее называл Леонардо. Поскольку ОП не размещал его код, я думал, что мой может помочь его исправить (хотя этот дополнительный вывод для меня не является проблемой, пока правильность действительно сохраняется).

Похоже, что если я изменю «/» в последнем утверждении, скажем, на оператор «+», проблема исчезнет.

(declare-fun fun0!0() Int) 
(declare-fun fun0!-1() Int) 
(declare-fun var0() Int) 

(assert (and 
    (and 
     (or (= fun0!0 0) (= fun0!0 1) (= fun0!0 2)) 
     (or (= fun0!-1 0) (= fun0!-1 1) (= fun0!-1 2)) 
     (or (= var0 1) (= var0 -1)) 
    ) 
    (and (or (= var0 0) (= var0 -1))) 
)) 

(define-fun fun0 ((i! Int)) Int 
    (ite 
     (= i! 0) 
     fun0!0 
     (ite 
      (= i! -1) 
      fun0!-1 
      (- 0 1) 
     ) 
    ) 
) 

(assert (= 
    (fun0 var0) 
    (/ var0 var0) 
)) 
(check-sat)