5

私が持っていると言う

t1<x and x<t2

t1<t2 Z3のように変数xを非表示にすることは可能 ですか?

4

2 に答える 2

6

そのために量指定子の削除を使用できます。次に例を示します。

(declare-const t1 Int)
(declare-const t2 Int)

(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))

この例はオンラインで試すことができます: http://rise4fun.com/Z3/kp0X

于 2012-07-24T11:27:12.700 に答える
2

Reduce の Redlog を使用した可能な解決策:

ここに画像の説明を入力

于 2013-07-28T20:31:05.713 に答える