Z3 подвесной для универсального количественного определения - PullRequest
Новая
       14

Z3 подвесной для универсального количественного определения

0 голосов
/ 03 декабря 2018

Я новичок в z3 и пытаюсь использовать z3 для решения следующей проблемы:

formula

Мой код z3 следующий: 

(declare-sort A)
(declare-sort O)
(declare-const o1 O)
(declare-const o2 O)

(declare-fun x () A)
(declare-fun g (A O) A)
(declare-fun f (A) Int)

(assert (= (f x) 0))
(assert (forall ((a A))
        (forall ((o O))
            (= (f (g a o)) (+ (f a) 1))
        )
    )
)

(assert (= (f (g x o1)) 1))
(assert (= (f (g (g x o2) o1)) 2))

(check-sat)
(get-model)

Когда я запускаю это (используя z3 без флагов), кажется, что оно зависает (я позволил ему работать в течение часа, прежде чем его остановить).Я знаю, что z3 не является процедурой принятия решений для универсально количественных формул в целом.Эта проблема выходит за пределы z3 или мне нужно что-то еще, чтобы z3 решил эту проблему?

1 Ответ

0 голосов
/ 03 декабря 2018

Скорее всего, это за пределами возможностей типичного решения SMT и z3.Вы можете поэкспериментировать с шаблонами, как описано здесь: https://rise4fun.com/z3/tutorialcontent/guide#h28 Однако я попробовал несколько наиболее очевидных родителей, но это не помогло.Даже если вы нашли правильный «образец», они, как правило, довольно хрупкие.Так да;Я бы сказал, что это за пределы того, с чем может справиться типичный решатель SMT.

...