Создание нескольких моделей для запросов CVC4 SMT

Могу ли я получить несколько моделей для запроса, подобного следующему?

(set-logic LIA)
(set-option :produce-models true)

(declare-const x Int)
(assert (< x 20))
(check-sat)
(get-model)

Вместо того, чтобы просто

sat
(
(define-fun x () Int 0)
)

Я хотел бы получить 0, 1, -1, 2,...


smt formal-methods satisfiability cvc4
person Alex Coleman    schedule 01.05.2021    source источник
comment
Если вы хотите изучить литературу по этой теме, эта проблема называется All-SAT для пропозициональной выполнимости или All-SMT при расширении до SMT. Вы можете найти множество статей по этим темам, например: sites.cs.ucsb. edu/~nestan/pdf/VLSID14.pdf и ieeexplore.ieee.org/document/7299903 .   -  person Tim    schedule 03.05.2021
comment
@ Тим, это действительно интересно. Спасибо за комментарий.   -  person Alex Coleman    schedule 05.05.2021

Ответы (1)


arrow_upward
1
arrow_downward

В языке SMTLib нет механизма получения всех моделей. Итак, если вы обязаны использовать только SMTLib, вы не можете этого сделать; по крайней мере не легко.

Однако большинство решателей (определенно включая cvc4 и z3) могут быть написаны на языках более высокого уровня. Идея состоит в том, чтобы сделать вызов check-sat, и если вы получите решение, вы добавите дополнительное утверждение, которое запрещает эту модель, и запросите новую. Посмотрите этот ответ, чтобы узнать, как это сделать в z3, как написано в сценарии Python: Попытка найти все решения логической формулы с использованием Z3 в python. Вы можете сделать то же самое из C/Java и т.д.; или используйте привязку более высокого уровня, которая предоставляет такую ​​команду из коробки.

person alias    schedule 01.05.2021