2

SMT で Int から Bit Vector を使用するように切り替えました。ただし、ロジック QF_BV では、スクリプトで量指定子を使用できないため、FOL ルールを定義する必要があります。存在量指定子を削除する方法は知っていますが、普遍的な量指定子は? どうやってするか？

次のようなコードを想像してください。

(set-logic QF_AUFBV)

(define-sort Index () (_ BitVec 3))

(declare-fun P (Index) Bool)

(assert (forall ((i Index)) (= (P (bvadd i #b001)) (not (P i)) ) ) )
4

1 に答える 1

2

厳密に言えば、あなたは不運です。http://smtlib.cs.uiowa.edu/logics.shtmlによると、量指定子とビットベクトルを同時に含むロジックはありません。

そうは言っても、ほとんどのソルバーは非標準の組み合わせを許可します。コマンドを省略するだけset-logicで、幸運に恵まれるかもしれません。たとえば、Z3 はこのset-logic部分がなくても問題なくクエリを処理します。私はちょうど試してみました..

于 2015-07-14T20:58:00.750 に答える