как упростить результат скрытия переменной с помощью z3?

Я хочу скрыть некоторые переменные и получить упрощенные результаты.

Я хочу скрыть c1, c2 и d следующим образом:

(declare-const v1 Real)
(declare-const v2 Real)
(elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real)) 
                          (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0) 
                               (= v1 (+ c1 d)) 
                               (= v2 (+ c2 d)))))

Однако результат кажется сложным, на самом деле результат должен быть v2>=5.0 & v1<= v2+5.0, я использовал (apply ctx-solver-simplify) код

(declare-const v1 Real)
(declare-const v2 Real)
(assert (elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real)) 
                                  (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
                                       (= v1 (+ c1 d)) 
                                       (= v2 (+ c2 d))))))
(apply ctx-solver-simplify)

Однако, когда я добавляю применить....Есть и ошибка,скрипт может не работать. может ли кто-нибудь помочь мне исправить это?


z3 smt
person Community    schedule 03.09.2012    source источник
comment
Насколько я могу судить, это не ошибка, просто результат получился в форме, которая вам не нравится, я прав?   -  person Christoph Wintersteiger    schedule 03.09.2012
comment
Я имею в виду, что когда я запускаю код, возникает ошибка. Не результат неправильный   -  person    schedule 03.09.2012
comment
Ах да, запрос уродлив; ответ панели ниже показывает, как применять исключение квантификатора в сочетании с последующим упрощением.   -  person Christoph Wintersteiger    schedule 03.09.2012

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете использовать тактику then, чтобы применить исключение квантификатора к формуле и применить упрощение контекста ко всем подчиненным -цели произведены:

(declare-const v1 Real)
(declare-const v2 Real)
(assert (exists ((c1 Real) (c2 Real)(d Real)) 
                                  (and (<= c1 10.0) (>= c2 5.0) (>= d 0.0)
                                       (= v1 (+ c1 d)) 
                                       (= v2 (+ c2 d)))))
(apply (then qe ctx-solver-simplify))

В результате получается v2 >= 5.0 and v1 - v2 <= 5.0, что довольно близко к тому, что вы хотите.

person pad    schedule 03.09.2012
comment
qe — тактика устранения квантификатора; это соответствует elim-quantifiers. - person pad; 03.09.2012