Есть ли общий способ добавления гипотетических предположений в Z3?

Question

Я только начинаю, и мне любопытно, есть ли способ добавить гипотезы. Использование (assert ...) не то, что я хочу, так как для моего приложения иногда предположениям разрешено быть ложными, и поэтому все должно стать выполнимым. Я знаю, что могу просто использовать такие последствия, как (assert (подразумевает вывод о допущении)), но, если есть много предположений, кажется неуклюжим преобразовать все мои утверждения в значения. Грубо я хотел бы иметь модель взаимодействия, как

(предположим ...)

...

(предположим ...)

(утверждать ...)

...

(утверждают ...)

(чек-сат)

Answer 1

Использование assert с последствиями - путь, нет assume (см. Руководство SMT-LIB, раздел 3.9, http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf).

Если у вас есть много утверждений, которые вы хотите использовать в качестве предположения, вы можете использовать один из программных интерфейсов API, чтобы помочь автоматизировать это преобразование для вас: http://z3.codeplex.com/documentation

В качестве альтернативы, если утверждения достаточно просты, вы можете просто написать сценарий, работающий над строковыми представлениями утверждений для печати формул SMT-LIB с последствиями.

Вас также может заинтересовать: Soft/Hard constraints in Z3