How to print the entire model in cvc4 using smtlib

Question

so I have just started to learn cvc4 after I have spent some time learning boolector. With it, it is possible to print the model just using boolector_print_model. Unfortunately the doc page for cvc4 is down at the moment and I cannot understand how to do the same with cvc4 in Java.

Can anyone help to do it please?

For instance, you could help me to see the model for this example.

EDIT: Just to be clear, with the entire model I mean a valid value for each BV or in general variable present within my model.

An example model could be:

(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)
  ...
)

Thanks a lot

Answer 1

Unlike boolector, CVC4 does not have a mechanism of accessing the entire model in once call via the API. This is because CVC4 allows for much richer types, including data-types, uninterpreted-functions, etc.; which makes model construction more complicated.

Instead, you call the getValue method for each of the input variables you have, and print them yourself. Here's an example:

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