z3py останавливается при выполнении исключения квантификатора в цикле - PullRequest
Новая
       5

z3py останавливается при выполнении исключения квантификатора в цикле

0 голосов
/ 10 февраля 2020

Я пытаюсь применить следующее исключение квантификатора в Python. На третьей итерации z3 не возвращается и застревает. Я использую Python 2.7.17 и Ubuntu 18.04.4. 

from  z3 import *

for i in range(0,10) :
      n,X_0_, X_1_= Ints('n X_0_ X_1_')
      R_0_0, R__0, R_1_0, R__1= Ints('R_0_0 R__0 R_1_0 R__1')
      all=[n >= 3, X_0_ + X_1_ == n,X_0_ >= 0,R_0_0 <= X_0_, R_0_0 >= 0]
      all.extend([R_0_0 <= R__0, X_1_ >= 0, R_1_0 <= X_1_, R_1_0 >= 0, R_1_0 <= R__0, R_0_0 + R_1_0 == R__0])
      all.extend([3*R__0 > 2*n, R_1_0 > R_0_0, 3*R_1_0 <= 2*n, 3*R__1 <= 2*n])
      expr = And(*all)
      expr = Exists([R_0_0, R__0, R_1_0, R__1],expr)
      print "before:",expr
      tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))     
      expr=tactic(expr).as_expr()
      print "after:",expr
      print i

Чего мне не хватает? Должен ли я, например, освободить память, и т.д. c?

Обновление. Я заметил, что когда я меняю порядок переменных в Exists, иногда он не застревает! Я не знаю почему ...

Ответы [ 2 ]

0 голосов
/ 11 февраля 2020

Очевидно, что tacti c qe не подходит для этого небольшого выражения. Вместо этого следует использовать tacti c qe2, который делает проверки осуществимости меньшего веса. Кроме того, упрощение должно быть сделано до устранения квантификатора.

Таким образом, эту строку кода 

tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))

следует заменить следующей строкой 

tactic = Then(Tactic('simplify'),Tactic('qe2'),Tactic('solve-eqs'))
0 голосов
/ 10 февраля 2020

Этот вопрос отличается от того, который вы задавали раньше? Здесь: z3py умирает, пытаясь устранить квантификатор

Совет точно такой же! Если это другой вопрос, пожалуйста, поясните, чего вы пытаетесь достичь по-другому на этот раз.

...