1

所以我花了一些时间学习后才开始学习cvc4boolector。有了它，可以仅使用boolector_print_model打印模型。不幸的是，文档页面cvc4目前已关闭，我无法理解如何cvc4在 Java 中做同样的事情。

任何人都可以帮忙吗？

例如，你可以帮我看看这个例子的模型。

编辑：为了清楚起见，对于整个模型，我的意思是模型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)
  ...
)

非常感谢

4

1 回答 1

1

与 boolector 不同，CVC4 没有通过 API 一次调用访问整个模型的机制。这是因为 CVC4 允许更丰富的类型，包括数据类型、未解释函数等；这使得模型构建更加复杂。

相反，您getValue为您拥有的每个输入变量调用该方法，并自己打印它们。这是一个例子：

https://github.com/CVC4/CVC4/blob/e3cd4670a080554e4ae1f2f26ee4353d11f02f6b/examples/api/java/FloatingPointArith.java#L66-L68

于 2020-10-04T20:59:38.883 回答