0

いくつかの変数を非表示にして、簡略化された結果を取得したいと思います。

私は隠したい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)

ただし、applyを追加すると、エラーが発生し、スクリプトが機能しなくなります。誰かが私がそれを修正するのを手伝ってもらえますか？

4

1 に答える 1

2

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あなたが望むものに非常に近いものです。

于 2012-09-03T11:08:50.490 に答える