Есть ли способ передать предположения из (check-sat ...) утверждения формулы SMT2 в решатель?
Рассмотрим следующий пример формулы, хранящейся в ex.smt2:
# cat ex.smt2
(declare-fun p () Bool)
(assert (not p))
(check-sat p)
Как и ожидалось, запуск z3 дает unsat. Теперь я хотел бы решить с предположениями (p) через интерфейс z3py:
In [30]: ctx = z3.Context()
In [31]: s = z3.Solver(ctx=ctx)
In [32]: f = z3.parse_smt2_file("ex.smt2", ctx=ctx)
In [33]: s.add(f)
In [34]: s.check()
Out[34]: sat
Есть ли API для получения предположений (например, (p) в этом примере) от парсера? Или даже лучше, просто скажите решателю, чтобы он решил с предположениями, прочитанными из входного файла?
