z3py умирает, пытаясь устранить квантификатор - PullRequest
Новая
       66

z3py умирает, пытаясь устранить квантификатор

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

У меня есть программа Python, в которой я генерирую различные формулы z3, а затем выполняю экзистенциальное количественное определение некоторых из них. Раньше моя программа работала нормально, но внезапно она начала d ie пытаться исключить квантификатор для некоторых выражений. Код не возвращается и висит на этих примерах. Это один из входов, для которых возникает проблема. Все переменные являются целыми числами. Я пытаюсь напечатать expr, но он никогда не печатается. В проблемных случаях c процесс также не может быть легко завершен. Я должен заставить его закрыть терминал (ubuntu). 

Exists([R_1_0, R__0, R_0_1, R__1, R_0_0, R_1_1],
       And(n >= 3,
           X == n,
           X_0_ + X_1_ == X,
           X_0_ >= 0,
           R_0_0 <= X_0_,
           R_0_0 >= 0,
           R_0_0 <= R__0,
           R_0_1 <= X_0_,
           R_0_1 >= 0,
           R_0_1 <= R__1,
           X_1_ >= 0,
           R_1_0 <= X_1_,
           R_1_0 >= 0,
           R_1_0 <= R__0,
           R_1_1 <= X_1_,
           R_1_1 >= 0,
           R_1_1 <= R__1,
           R__0 <= X,
           R__1 <= X,
           R_1_0 + R_0_0 == R__0,
           R_1_1 + R_0_1 == R__1,
           And(True,
               And(And(3*R__0 > 2*n, R_0_0 >= R_1_0),
                   3*R_0_0 <= 2*n),
               And(And(3*R__1 <= 2*n, 3*R_0_1 <= 2*n),
                   3*R_1_1 <= 2*n))))

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

z3_expr = And(*conjuncts)// a list of small expressions like R_0_0 >= 0 produced by the program
z3_expr = Exists(some_variables,z3_expr)
tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))      
expr=tactic(z3_expr).as_expr()//this line doesn't return in some cases

Меня удивляет то, что если я заново сгенерирую это выражение, объявив переменные и выражения с нуля, он будет работать нормально. Что мне не хватает? Можно ли дать Tactic тайм-аут?

1 Ответ

1 голос
/ 07 февраля 2020

Вы можете связать тайм-аут с решателем, который вы получаете от tacti c: 

from z3 import *

s = Tactic('qe_rec').solver()
s.set("timeout", 500)

К сожалению, в моем опыте это не так надежно: во-первых, не все тактики поддерживают тайм-аут, и во-вторых, реализация кажется ненадежной; время ожидания не всегда соблюдается. К сожалению, нет достаточной документации о том, как сделать это должным образом.

Относительно того, почему устранение квантификатора может задыхаться: Невозможно сказать без добавления операторов трассировки в код и запуска его в режиме отладки. Очевидно, что это будет непросто, и будет нелегко определить причину root.

Я бы порекомендовал подать здесь проблему с людьми из z3: https://github.com/Z3Prover/z3/issues Было бы лучше дать им что-нибудь, что они могли бы хотя бы запустить и воспроизвести проблему, вместо того, чтобы задавать общий вопрос c, подобный этому. Пожалуйста, сообщите, что вы узнали!

...