как подавить упрощение формул до True или False?

можно ли отключить автоматическое упрощение логических выражений в Z3?

Например, выражение 2> 1 автоматически становится True, в то время как я хотел бы, чтобы оно оставалось 2> 1:

>>> t = 2 > 1
>>> t
True

Я нашел несколько вариантов, вызвав help_simplify () в Z3Py. Однако ни один из них, похоже, не имеет отношения к моей проблеме.

В другом руководстве (http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231) упоминалась опция «УПРОЩИТЕЛЬ КОНТЕКСТА»: «Этот параметр можно использовать для упрощения подформул до истинного или ложного. " Однако мне не удалось найти эту опцию в Z3Py.

Предпосылки: я хотел бы иметь возможность использовать такие выражения, как And (2> 1, 1! = 2), где 2> 1 и 1! = 2 автоматически генерируются раньше и иногда не содержат переменных (констант). Z3Py упрощает это до And (True, False), которое не принимается, потому что «По крайней мере, один из аргументов должен быть выражением Z3 или зондом». Поэтому я хотел бы исключить упрощение. Или есть способ сделать And (True, False) приемлемым выражением?

Заранее спасибо!


z3 z3py
person Carsten Rütz    schedule 28.05.2014    source источник
comment
ну, я только что заметил, что это упрощение уже сделано интерактивной оболочкой python: она оценивает простое сравнение 2 ›1 до того, как Z3Py действительно сможет это сделать. Однако у меня остается вопрос: как подавить это и передать Z3Py термин 2 ›1 и / или как разрешить выражения And (True, False)?   -  person Carsten Rütz    schedule 28.05.2014

Ответы (1)


arrow_upward
1
arrow_downward

В самом деле, это связано с тем, что простые выражения вроде 2> 1 упрощаются Python до True / False. Большинство операторов (например, Implies, Xor, ...) с этим справлялись, но операторы And и Or - нет. У них была другая реализация, потому что они могут использоваться как для зондов, так и для выражений. Я добавил немного больше кода, чтобы заставить их вести себя как другие логические операторы (для исправления см. здесь). Я надеюсь, что это решит эту проблему, не создавая при этом никаких новых проблем с датчиками. Я был бы признателен, если бы кто-нибудь еще мог это проверить.

person Christoph Wintersteiger    schedule 29.05.2014
comment
Я обошел проблему, используя IntVal (..) и BoolVal (..) вместо целочисленных литералов и логических констант: IntVal (2) ›IntVal (1) не упрощается интерактивной оболочкой python, поэтому And (BoolVal (True) , IntVal (2) ›IntVal (1)) также принимается - person Carsten Rütz; 11.06.2014