Запрос Python Z3 API: можем ли мы получить частичную модель, используя z3 python API, когда решатель возвращает неизвестный статус

Question

Я почти уверен, что это как-то связано с API Python. Есть ли способ вернуть частичную модель из z3, даже если статусunknown?

Пытаюсь вытащить модель из z3 даже когда статус возвращается unknownрезультат. Не удается поднятьexception за model not available. Есть предложения, что можно сделать?

Я преобразовал утверждения в формат smt-lib, используя sexpr() метод из z3 Solver интерфейс, и он возвращает частичную модель, даже если статус unknown. Я приложил пример ниже.

# -*- coding: utf-8 -*-
​
from z3 import *
​
x, y, z = Reals('x y z')
m, n, l = Reals('m n l')
u, v = Ints('u v')
​
S = SolverFor("NRA")
​
S.add(x >= 0)
S.add(y >= 30, z <= 50)
S.add(m >= 5, n >= 5)
S.add(m * x + n * y + l > 300)
​
S.add(ForAll([u, v], Implies(m * u + n * v + l > 300, u + v + z <= 50)))
​
print(S.check())
print(S.sexpr())

В формате SMMT-LIB

(set-option :print-success true) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun l () Real)
(assert (>= x 0.0))
(assert (>= y 30.0))
(assert (<= z 50.0))
(assert (>= m 5.0))
(assert (>= n 5.0))
(assert (not (<= (+ (* m x) (* n y) l) 300.0)))
(assert (forall ((u Int) (v Int))
  (let ((a!1 (<= (+ (* m (to_real u)) (* n (to_real v)) l) 300.0)))
    (or (<= (+ (to_real u) (to_real v) z) 50.0) a!1))))
(check-sat)
(get-model)

Я запускаю этот файл из командной строки (терминала)

$ z3 example.py

Выход:

success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
unknown
(model 
  (define-fun z () Real
    20.0)
  (define-fun y () Real
    30.0)
  (define-fun l () Real
    145.0)
  (define-fun x () Real
    0.0)
  (define-fun n () Real
    5.0)
  (define-fun m () Real
    5.0)
)

Есть предложения о том, как получить эту модель напрямую через интерфейс Python?

Исключение, которое z3 вызывает после model() позвонить unknown статус.

unknown
Traceback (most recent call last):

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6696, in model
    return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 3759, in Z3_solver_get_model
    _elems.Check(a0)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 1385, in Check
    raise self.Exception(self.get_error_message(ctx, err))

Z3Exception: b'there is no current model'


During handling of the above exception, another exception occurred:

Traceback (most recent call last):

  File "C:\Users\lahir\Documents\GitHub\codersguild\Research\tangram-solve\z3_tryouts.py", line 19, in <module>
    print(S.model())

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6698, in model
    raise Z3Exception("model is not available")

Z3Exception: model is not available

Спасибо

Answer 1

Вы не можете полагаться на модель, если решатель вернул unknown. То есть модель, которую вы получаете, ни в коем случае не является "частичной": она может удовлетворять или не удовлетворять некоторым ограничениям, но в остальном вы мало что можете с ней сделать. В лучшем случае это представление внутреннего состояния решателя. Но в целом не гарантируется, что это будет изображение чего-либо.

Кроме того, когда я запускаю ваш сценарий SMTLib с z3, я получаю:

unknown
(error "line 21 column 10: model is not available")

и я построил z3 на их мастере github около недели назад. Я так понимаю, у вас старая версия, я настоятельно рекомендую вам обновить ее.

Для справки: когда вы получаете ответ "неизвестно", единственное, что можно сделать, - это спросить решающую программу, почему результат неизвестен. Обычно это делается с помощью такого кода:

r = S.check()
if r == sat:
    print(S.model())
elif r == unknown:
    print("Unknown, reason: %s" % S.reason_unknown())
else:
    print("Solver said: %s" % r)

Для вашей программы Python я получаю:

smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)

и это действительно единственная информация, которая у вас есть на данный момент: любое "извлечение" значений модели было бы просто неправильным, если состояние решателя unknown.

(Связанный с этим вопрос также касается "прерывания" вычислений во время вызова оптимизирующего решателя z3. "Модель", которую вы получите, если вы прервете решатель, ни в коем случае не будет "лучшей" до сих пор, она может удовлетворять или не удовлетворять существующие ограничения. Короче говоря, если решатель не сообщаетsat, не рассчитывайте на полученную модель: z3 поступает правильно и сообщает вам, что жизнеспособной модели нет.)

Answer 2

Я еще не нашел альтернативу, кроме той, которую я упомянул выше.