smt - smtlib を使用して cvc4 でモデル全体を印刷する方法

Question

そのため、学習に時間を費やした後、 cvc4の学習を開始したところboolectorです。これにより、 boolector_print_modelを使用するだけでモデルを印刷できます。残念ながら のドキュメント ページは現在ダウンしており、Java でcvc4同じことを行う方法がわかりません。cvc4

誰でもそれを手伝ってもらえますか？

たとえば、この例のモデルを見るのを手伝ってくれませんか。

編集：明確にするために、モデル全体BVで、モデル内に存在する各変数または一般的な変数の有効な値を意味します。

モデルの例は次のとおりです。

(model
  ...
  (define-fun number_6_0_7 () (_ BitVec 8) #x00)
  (define-fun number_6_1_7 () (_ BitVec 8) #x00)
  (define-fun number_6_2_7 () (_ BitVec 8) #x00)
  (define-fun number_6_3_7 () (_ BitVec 8) #x78)
  ...
)

どうもありがとう