Как упростить Or (Not (y), And (y, Not (x))) до Or (Not (y), Not (x)) с Z3?

Question

Я пытался использовать Z3 для упрощения ~y or (y, ~x) до ~y or ~x, но, похоже, не могу этого сделать, даже когда я использую tacti c ctx-solver-simplify. Ниже приведен код Python, демонстрирующий то, что я сделал. Есть идеи, как этого добиться? Спасибо,

sage: x,y = z3.Bools('x y')
sage: f = Or(Not(y), And(y, Not(x)))
sage: simpl = Tactic('ctx-solver-simplify')
sage: simpl = z3.TryFor(simpl, 300000)
sage: simpl(f).as_expr()
Or(Not(y), And(y, Not(x)))   # cannot simplify

Answer 1

Z3 обладает мощным механизмом для поиска решений, но все это находится под капотом.

Sympy , Python symboli c математическая библиотека больше подходит для такого рода упрощений. srepr() может использоваться для отображения внутреннего формата. По умолчанию логические операторы отображаются как &, | и ~. Вы также можете напрямую использовать эти символы для написания выражений.

from sympy import symbols, Or, Not, And, srepr

x, y = symbols('x y')
f = Or(Not(y), And(y, Not(x))) # or f = ~y | (y & ~x)

print(f) # ~y | (y & ~x)
print(f.simplify()) # ~x | ~y
print(srepr(f)) # Or(Not(Symbol('y')), And(Symbol('y'), Not(Symbol('x'))))
print(srepr(f.simplify())) # Or(Not(Symbol('x')), Not(Symbol('y')))

Answer 2

В общем, вы не можете ожидать, что z3 выполнит такие упрощения, поскольку то, что вы считаете «простым», и то, что оно считает «простым», может сильно различаться.

Сказав это, вы можете запустить help_simplify() и это покажу вам все варианты simplify поддерживает. Из того, что я вижу, нет правила, которое бы помогло в вашем случае.

Обратите внимание, что решатели SMT на самом деле не предназначены для такого рода упрощения на уровне пользователя. Более традиционным было бы спросить z3, является ли то, что вы считаете упрощенной формой, действительно эквивалентным. В вашем случае что-то вроде:

from z3 import *

x, y = Bools('x y')

f = Or(Not(y), And(y, Not(x)))
g = Or(Not(y), Not(x))

prove(f == g)

На что отвечает z3:

proved