z3 - z3を使用した式で「not」を削除する方法は?

Question

コードを使用して、式に含まれていないものを削除しようとしています:

(declare-const t Int)

(assert (and (or (>= t 2) (>= t 1)) (not (= t 1))))

(apply ctx-solver-simplify)

次のような結果を取得したい: t >= 2 ただし、結果は次のとおりです。

(goals
(goal
  (>= t 1)
  (not (= t 1))
  :precision precise :depth 1)
)

誰かがそれを行う方法を教えてくれますか?

Answer 1

戦術simplifyにはオプションがあります:eq2ineq。有効にすると、等式が に変換t1 = t2されt1 <= t2 and t1 >= t2ます。この戦術を適用した後、戦術propagate-ineqsはより効果的になります。

トリックを実行するスクリプトは次のとおりです。 http://rise4fun.com/Z3/JWit

これは一般的な解決策ではないことに注意してください。組み込みの戦術はどれも、あなたが望むことを正確に行うものではありません。