0

問題は非常に単純です。C API インターフェイスを使用して、Z3 で次のステートメントをアサートします。

(assert(>= (xA 1) (- (yB 0) period))))

ここで、どのような種類のアサーションが供給され、SatSolver で結果が得られたかを確認する必要がある場合があります。これを行うには、ast_to_string() API を使用してテキスト ファイルを生成します。この API は、上記のステートメントを次のように返します -

(assert(>= (xA 1) (+ (yB 0) (* -1 period))))

このファイルを Sat Solver にフィードすると、次のエラーが表示されます -

(エラー「エラー: 行 150 列 56: ID -1 が見つかりませんでした。」)

そのため、コード内のすべての -1 を手動で修正し、sat ソルバーを実行する必要があります。これを回避できる他の方法はありますか？

4

1 に答える 1

1

設定することを忘れないでください：

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

ast_to_string()出力式が SMTLIB 2.0 形式に準拠するように、使用する前に確認してください。

于 2012-05-31T12:21:07.213 に答える