Как распечатать всю модель в cvc4 с помощью smtlib

поэтому я только начал изучать cvc4 после того, как потратил некоторое время на изучение boolector. С его помощью можно распечатать модель, просто используя 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)
  ...
)

Большое спасибо


smt cvc4
person Alberto    schedule 04.10.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

В отличие от boolector, CVC4 не имеет механизма доступа ко всей модели за один вызов через API. Это связано с тем, что CVC4 допускает гораздо более богатые типы, включая типы данных, неинтерпретируемые функции и т. д.; что усложняет построение модели.

Вместо этого вы вызываете метод getValue для каждой из имеющихся у вас входных переменных и печатаете их самостоятельно. Вот пример:

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

person alias    schedule 04.10.2020
comment
Спасибо, @alias, по крайней мере, я должен иметь возможность использовать dump, верно? Я пытаюсь, но ничего. Я думал, что если установлено значение true, это позволит мне печатать модель после каждого chdckSat. Любое предложение? Спасибо - person Alberto; 05.10.2020
comment
Если вы имеете в виду параметр командной строки --dump-models для CVC4: он доступен только при использовании CVC4 из командной строки с вводом SMTLib. Нет эквивалента, когда вы используете его из API. - person alias; 05.10.2020
comment
С помощью ML я обнаружил, что существует метод printModel(), github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h#L3169, есть даже примеры того, как его использовать с помощью C++, но не Java. Я все еще пытаюсь понять это. Помните, что я использую 1.8, а не последнюю версию, потому что новый API Java недоступен для этой версии. Спасибо - person Alberto; 06.10.2020