Форма запроса валидации, решатель SMT, Z3, STP

Question

У меня есть булевая формула f(a, b, x, y). Где a и b являются булевыми выражениями и x и y являются битовыми векторными выражениями. a и b являются булевыми выражениями, возможно, с использованием выражений a, b, x и y.

Я хочу, чтобы определить следующий запрос для действия:

f(a, b, x, y)* such that *a = false && b = false 

f(a, b, x, y)* such that *a = true && b = false 

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

Просьба сообщить, как создать такой запрос.

Answer 1

Почему бы не создать свежую переменную для? вы можете утверждать следующее: (утверждать (не)) (утверждать (не б)) (утверждают (fabxy)) (утверждают, а2) (утверждать (не (е а2 Ъху))) (чек-СБ)

ваш запрос является действительным, если и только если выше запрос невыполнима, так как переплеты представлены как утверждения и вывод был отрицается (и уплощенная в двух утверждений)