2

我使用以下策略来简化表达

(apply (then  (! simplify :eq2ineq true) ctx-solver-simplify propagate-values ctx-solver-simplify (par-then (repeat (or-else split-clause skip)) propagate-ineqs) tseitin-cnf))

原来的表达是：

( 0 > t_DS or 1 > t_FS or 1 > t_PS) And 
(true) And 
(( 0 > t_DS or 0 > t_FS or 0 > t_PS) or (t_DS <= 3)) And 
(( 0 > t_DS or 0 > t_FS or 0 > t_PS or t_FS <= 1) or ( t_DS+t_FS <= 3)) And
((0 > t_DS or 0 > t_PS or 1 > t_FS or t_PS > 1) or ( t_DS+t_PS <= 2)) And
(t_DS >=0) And (t_FS >= 0) And (t_PS >=0)

应用该策略后，简化结果为：

(goals
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_User 0.0)
  (>= t_PS 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (not (<= t_PS 1.0))
  (>= t_User 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (<= (+ t_DS t_PS) 2.0)
  (>= t_PS 0.0)
  (<= t_PS 2.0)
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (not (<= t_FS 1.0))
  (<= (+ t_DS t_PS) 2.0)
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (>= t_User 0.0))
(goal
  (>= t_PS 0.0)
  (not (>= t_PS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 2.0)
  (>= t_FS 0.0)
  (<= t_FS 3.0)
  (<= (+ t_DS t_PS) 2.0)
  (>= t_User 0.0))
)

但是，我认为第二个目标可以删除，因为它比第一个要强。那么如何使用 z3 来获得更简单的结果呢？

(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (>= t_User 0.0)
  (>= t_PS 0.0))
(goal
  (>= t_FS 0.0)
  (not (>= t_FS 1.0))
  (<= (+ t_DS t_FS) 3.0)
  (>= t_DS 0.0)
  (<= t_DS 3.0)
  (not (<= t_PS 1.0))
  (>= t_User 0.0))
4

1 回答 1

0

不幸的是，这在当前的实现中无法做到，因为不同目标之间没有通信。

于 2013-07-05T19:19:19.933 回答