Как я могу написать длинное выражение smt-lib с квантором существования?

У меня есть следующее выражение

(declare-fun x00 () Real)
(declare-fun x01 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)
(declare-fun t0init () Real)
(declare-fun z0init0 () Real)
(declare-fun z0init1 () Real)
(assert (>= t0init 0))
(assert (= (+ x00 z0init0) x10))
(assert (= (+ x01 z0init1) x11))
(assert (< (+ (* 1 x00)(* 0 x01)) 0.0))
(assert (= (+ (* 0 x00)(* 1 x01)) 0.0))
(assert (< (+ (* 1 x10)(* 0 x11)) 0.0))
(assert (= (+ (* 0 x10)(* 1 x11)) 0.0))
...
(assert (< (+ (* 1 x40)(* 0 x41)) 0.0))
(assert (= (+ (* 0 x40)(* 1 x41)) 0.0))
(assert (= (+ (* 1 z4end0)(* 0 z4end1)) (* t4end 1)))
(assert (= (+ (* 0 z4end0)(* 1 z4end1)) (* t4end -2)))

и я хотел бы выразить в виде простой формулы, чтобы выразить следующее:

(assert exists (x00 x01) ("the above expression"))

а затем выполните исключение квантификатора.

Есть ли кто-нибудь, кто знает, как действовать? Я знаю, как это сделать с помощью z3py, но мне нужно более быстрое решение.

Большое спасибо за любую подсказку.


z3 smt
person Mairim    schedule 09.04.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Одно из возможных решений заключается в следующем

(declare-fun x00 () Real)
(declare-fun x01 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)
(declare-fun t0init () Real)
(declare-fun z0init0 () Real)
(declare-fun z0init1 () Real)
(define-fun conjecture () Bool
   (and (>= t0init 0) (= (+ x00 z0init0) x10) (= (+ x01 z0init1) x11)))
(assert (exists ((x00 Real) (x01 Real)) conjecture))
(check-sat)

и соответствующий вывод

sat

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

person Juan Ospina    schedule 09.04.2014