Fortress

Предлагается реализовать следующие статические методы работы с логическими формулами (условиями):

1. boolean isCondition(Node expr) - проверка того, что формула является логической формулой;
2. boolean isAtomicCondition(Node expr) - проверка того, что формула является атомарной логической формулой (в ней нет логических связок: !, &&, || и др.);
3. Node getConjunction(Node ... expr) = (expr[1] && ... && expr[n]) - получение конъюнкции системы условий;
4. Node getDisjunction(Node ... expr) = (expr[1] || ... || expr[n]) - получение дизъюнкции системы условий;
5. Node getNegation(Node ... expr) = !getConjunction(expr[1], ..., expr[n]) - получение отрицания системы условий;
6. Node getComplement(Node ... expr) = getNegation(getDisjunction(expr[1], ..., expr[n]) - получение дополнения к системе условий;
7. boolean areComplete(Node ... expr) = !(getComplement(expr[1], ..., expr[n]) is SAT) - проверка системы условий на полноту;
8. boolean areCompatible(Node ... expr) = (getConjunction(expr[1], ..., expr[n]) is SAT) - проверка системы условий на совместимость.