BooleanUtils.java

//==============================================================================
//	
//	Copyright (c) 2015-
//	Authors:
//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package parser;

import java.io.ByteArrayInputStream;
import java.util.ArrayList;
import java.util.List;

import parser.ast.Expression;
import parser.ast.ExpressionBinaryOp;
import parser.ast.ExpressionLiteral;
import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.type.TypeBool;
import parser.visitor.ASTTraverseModify;
import prism.PrismException;
import prism.PrismLangException;

public class BooleanUtils
{
	/**
	 * Extract the conjuncts from a conjunction in the form of zero or more nested
	 * binary conjunctions represented by ExpressionBinaryOp objects.
	 * 
	 * @param expr The conjunction to extract from 
	 * @param conjuncts The list to insert conjuncts into
	 */
	public static void extractConjuncts(Expression expr, List<Expression> conjuncts)
	{
		// Traverse depth-first, and add any non-ands to the list
		if (Expression.isAnd(expr)) {
			extractConjuncts(((ExpressionBinaryOp) expr).getOperand1(), conjuncts);
			extractConjuncts(((ExpressionBinaryOp) expr).getOperand2(), conjuncts);
		} else {
			conjuncts.add(expr);
		}
	}

	/**
	 * Extract the disjuncts from a disjunction in the form of zero or more nested
	 * binary disjunctions represented by ExpressionBinaryOp objects.
	 * 
	 * @param expr The disjunction to extract from 
	 * @param disjuncts The list to insert disjuncts into
	 */
	public static void extractDisjuncts(Expression expr, List<Expression> disjuncts)
	{
		// Traverse depth-first, and add any non-ors to the list
		if (Expression.isAnd(expr)) {
			extractDisjuncts(((ExpressionBinaryOp) expr).getOperand1(), disjuncts);
			extractDisjuncts(((ExpressionBinaryOp) expr).getOperand2(), disjuncts);
		} else {
			disjuncts.add(expr);
		}
	}

	/**
	 * Convert a Boolean expression to positive normal form,
	 * i.e., remove any instances of =>, <=> or () and then push
	 * all negation inwards so that it only occurs on "propositions".
	 * A "proposition" is any Expression object that
	 * is not an operator used to define a Boolean expression (!, &, |, =>, <=>, ()).
	 * The passed in expression is modified, and the result is returned. 
	 */
	public static Expression convertToPositiveNormalForm(Expression expr)
	{
		// First expand implies/iff/parentheses
		// Then do conversion to +ve normal form
		return doConversionToPositiveNormalForm(removeImpliesIffAndParentheses(expr), false);
	}
	
	/**
	 * Convert an LTL formula to positive normal form,
	 * i.e., remove any instances of =>, <=> or () and then push
	 * all negation inwards so that it only occurs on "propositions".
	 * A "proposition" is any Expression object that
	 * is not an operator used to define a Boolean expression (!, &, |, =>, <=>, ())
	 * or a temporal operator (X, U, F, G, R, W).
	 * The passed in expression is modified, and the result is returned. 
	 */
	public static Expression convertLTLToPositiveNormalForm(Expression expr)
	{
		// First expand implies/iff/parentheses
		// Then do conversion to +ve normal form
		return doConversionToPositiveNormalForm(removeImpliesIffAndParentheses(expr), true);
	}
	
	/**
	 * Remove any instances of =>, <=> or () by expanding/deleting as appropriate.
	 */
	private static Expression removeImpliesIffAndParentheses(Expression expr)
	{
		Expression exprMod = null;
		try {
			exprMod = (Expression) expr.accept(new ASTTraverseModify()
			{
				public Object visitNow(ExpressionUnaryOp e) throws PrismLangException
				{
					// Remove parentheses: (a)
					if (Expression.isParenth(e)) {
						Expression a = (Expression) (e.getOperand().accept(this));
						// (a)  ==  a 
						return a;
					}
					return super.visitNow(e);
				}

				public Object visitNow(ExpressionBinaryOp e) throws PrismLangException
				{
					// Remove implication: a => b
					if (Expression.isImplies(e)) {
						Expression a = (Expression) (e.getOperand1().accept(this));
						Expression b = (Expression) (e.getOperand2().accept(this));
						// a => b  ==  !a | b 
						return Expression.Or(Expression.Not(a), b);
					}
					// Remove iff: a <=> b
					if (Expression.isIff(e)) {
						Expression a = (Expression) (e.getOperand1().accept(this));
						Expression b = (Expression) (e.getOperand2().accept(this));
						// a <=> b  ==  (a | !b) & (!a | b) 
						return Expression.And(Expression.Or(a, Expression.Not(b)), Expression.Or(Expression.Not(a.deepCopy()), b.deepCopy()));
					}
					return super.visitNow(e);
				}
			});
		} catch (PrismLangException e) {
			// Shouldn't happen since we do not throw PrismLangException above
		}
		return exprMod;
	}
	
	/**
	 * Do the main part of the conversion of a Boolean expression to positive normal form,
	 * i.e., push all negation inwards to the propositions. If {@code ltl} is false, it is assumed
	 * that the Boolean expression comprises only the Boolean operators !, & and |.
	 * If {@code ltl} is true, the expression can also contain temporal operators (X, U, F, G, R, W). 
	 * Anything else is treated as a proposition.
	 * The passed in expression is modified, and the result is returned. 
	 */
	private static Expression doConversionToPositiveNormalForm(Expression expr, boolean ltl)
	{
		// Remove negation
		if (Expression.isNot(expr)) {
			Expression neg = ((ExpressionUnaryOp) expr).getOperand();
			// Boolean operators
			if (Expression.isTrue(neg)) {
				// ! true  ==  false
				return new ExpressionLiteral(TypeBool.getInstance(), false);
			} else if (Expression.isFalse(neg)) {
				// ! false  ==  true
				return new ExpressionLiteral(TypeBool.getInstance(), true);
			} else if (Expression.isNot(neg)) {
				Expression a = ((ExpressionUnaryOp) neg).getOperand();
				// !(!a)  ==  a 
				return doConversionToPositiveNormalForm(a, ltl);
			} else if (Expression.isOr(neg)) {
				Expression a = ((ExpressionBinaryOp) neg).getOperand1();
				Expression b = ((ExpressionBinaryOp) neg).getOperand2();
				Expression aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl);
				Expression bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
				// !(a | b)  ==  !a & !b 
				return Expression.And(aNeg, bNeg);
			} else if (Expression.isAnd(neg)) {
				Expression a = ((ExpressionBinaryOp) neg).getOperand1();
				Expression b = ((ExpressionBinaryOp) neg).getOperand2();
				Expression aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl);
				Expression bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
				// !(a & b)  ==  !a | !b 
				return Expression.Or(aNeg, bNeg);
			}
			// Temporal operators (if required)
			else if (ltl) {
				if (neg instanceof ExpressionTemporal) {
					ExpressionTemporal exprTemp = (ExpressionTemporal) neg;
					Expression a = exprTemp.getOperand1();
					Expression b = exprTemp.getOperand2();
					Expression aNeg = null, bNeg = null, aCopy = null, bNegCopy = null;
					switch (exprTemp.getOperator()) {
					case ExpressionTemporal.P_X:
						bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						// !(X b)  ==  X !b
						return new ExpressionTemporal(ExpressionTemporal.P_X, null, bNeg);
					case ExpressionTemporal.P_U:
						aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl);
						bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						// !(a U b)  ==  !a R !b
						return new ExpressionTemporal(ExpressionTemporal.P_R, aNeg, bNeg);
					case ExpressionTemporal.P_F:
						 bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						// !(F b)  ==  G !b
						return new ExpressionTemporal(ExpressionTemporal.P_G, null, bNeg);
					case ExpressionTemporal.P_G:
						 bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						// !(G b)  ==  F !b
						return new ExpressionTemporal(ExpressionTemporal.P_F, null, bNeg);
					case ExpressionTemporal.P_W:
						aCopy = doConversionToPositiveNormalForm(a.deepCopy(), ltl);
						bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl);
						bNegCopy = doConversionToPositiveNormalForm(Expression.Not(b.deepCopy()), ltl);
						// !(a W b) == a&!b U !a&!b
						return new ExpressionTemporal(ExpressionTemporal.P_R, Expression.And(aCopy, bNeg), Expression.And(aNeg, bNegCopy));
					case ExpressionTemporal.P_R:
						aNeg = doConversionToPositiveNormalForm(Expression.Not(a), ltl);
						bNeg = doConversionToPositiveNormalForm(Expression.Not(b), ltl);
						// !(a R b)  ==  !a U !b
						return new ExpressionTemporal(ExpressionTemporal.P_U, aNeg, bNeg);
					default:
						// Don't change (shouldn't happen)
						return expr;
					}
				}
			} else {
				// Proposition (negated)
				return expr;
			}
		}
		// Preserve and
		if (Expression.isAnd(expr)) {
			Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1(), ltl);
			Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2(), ltl);
			return Expression.And(a, b);
		}
		// Preserve or
		if (Expression.isOr(expr)) {
			Expression a = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand1(), ltl);
			Expression b = doConversionToPositiveNormalForm(((ExpressionBinaryOp) expr).getOperand2(), ltl);
			return Expression.Or(a, b);
		}
		// Preserve temporal operators
		if (ltl && expr instanceof ExpressionTemporal) {
			Expression a = ((ExpressionTemporal) expr).getOperand1(); 
			Expression b = ((ExpressionTemporal) expr).getOperand2();
			Expression aConv = (a == null) ? null : doConversionToPositiveNormalForm(a, ltl);
			Expression bConv = (b == null) ? null : doConversionToPositiveNormalForm(b, ltl);
			return new ExpressionTemporal(((ExpressionTemporal) expr).getOperator(), aConv, bConv);
		}
		// Proposition
		return expr;
	}

	/**
	 * Convert an expression to disjunctive normal form (DNF).
	 * The passed in expression is modified, and the result is returned. 
	 */
	public static Expression convertToDNF(Expression expr)
	{
		return convertDNFListsToExpression(doConversionToDNF(convertToPositiveNormalForm(expr)));
	}

	/**
	 * Convert an expression to disjunctive normal form (DNF).
	 * The passed in expression is modified, and the result is returned as a list of lists of Expression;
	 */
	public static List<List<Expression>> convertToDNFLists(Expression expr)
	{
		return doConversionToDNF(convertToPositiveNormalForm(expr));
	}

	private static List<List<Expression>> doConversionToDNF(Expression expr)
	{
		// And
		if (Expression.isAnd(expr)) {
			Expression a = ((ExpressionBinaryOp) expr).getOperand1();
			Expression b = ((ExpressionBinaryOp) expr).getOperand2();
			List<List<Expression>> aDnf = doConversionToDNF(a);
			List<List<Expression>> bDnf = doConversionToDNF(b);
			// a1|a2|... & b1|b2|...  ==  a1&b1 | a1&b2 | ...
			List<List<Expression>> dnf = new ArrayList<List<Expression>>();
			for (List<Expression> ai : aDnf) {
				for (List<Expression> bj : bDnf) {
					List<Expression> aibj = new ArrayList<Expression>();
					aibj.addAll(ai);
					aibj.addAll(bj);
					dnf.add(aibj);
				}
			}
			return dnf;
		}
		// Or
		if (Expression.isOr(expr)) {
			Expression a = ((ExpressionBinaryOp) expr).getOperand1();
			Expression b = ((ExpressionBinaryOp) expr).getOperand2();
			List<List<Expression>> aDnf = doConversionToDNF(a);
			List<List<Expression>> bDnf = doConversionToDNF(b);
			// (a1|a2|...) | (b1|b2|...)  ==  a1|a2|...|b1|b2|...
			aDnf.addAll(bDnf);
			return aDnf;
		}
		// Convert proposition to trivial DNF
		List<List<Expression>> dnf = new ArrayList<List<Expression>>(1);
		List<Expression> disjunct = new ArrayList<Expression>(1);
		disjunct.add(expr);
		dnf.add(disjunct);
		return dnf;
	}

	/**
	 * Convert an expression to conjunctive normal form (CNF).
	 * The passed in expression is modified, and the result is returned. 
	 */
	public static Expression convertToCNF(Expression expr)
	{
		return convertCNFListsToExpression(doConversionToCNF(convertToPositiveNormalForm(expr)));
	}

	/**
	 * Convert an expression to conjunctive normal form (CNF).
	 * The passed in expression is modified, and the result is returned as a list of lists of Expression;
	 */
	public static List<List<Expression>> convertToCNFLists(Expression expr)
	{
		return doConversionToCNF(convertToPositiveNormalForm(expr));
	}

	private static List<List<Expression>> doConversionToCNF(Expression expr)
	{
		// Remove parentheses
		if (Expression.isParenth(expr)) {
			return doConversionToCNF(((ExpressionUnaryOp) expr).getOperand());
		}
		// Or
		if (Expression.isOr(expr)) {
			Expression a = ((ExpressionBinaryOp) expr).getOperand1();
			Expression b = ((ExpressionBinaryOp) expr).getOperand2();
			List<List<Expression>> aCnf = doConversionToCNF(a);
			List<List<Expression>> bCnf = doConversionToCNF(b);
			// a1&a2&... | b1&b2&...  ==  a1|b1 & a1|b2 & ...
			List<List<Expression>> cnf = new ArrayList<List<Expression>>();
			for (List<Expression> ai : aCnf) {
				for (List<Expression> bj : bCnf) {
					List<Expression> aibj = new ArrayList<Expression>();
					aibj.addAll(ai);
					aibj.addAll(bj);
					cnf.add(aibj);
				}
			}
			return cnf;
		}
		// And
		if (Expression.isAnd(expr)) {
			Expression a = ((ExpressionBinaryOp) expr).getOperand1();
			Expression b = ((ExpressionBinaryOp) expr).getOperand2();
			List<List<Expression>> aCnf = doConversionToCNF(a);
			List<List<Expression>> bCnf = doConversionToCNF(b);
			// (a1|a2|...) | (b1|b2|...)  ==  a1|a2|...|b1|b2|...
			aCnf.addAll(bCnf);
			return aCnf;
		}
		// Convert proposition to trivial CNF
		List<List<Expression>> cnf = new ArrayList<List<Expression>>(1);
		List<Expression> conjunct = new ArrayList<Expression>(1);
		conjunct.add(expr);
		cnf.add(conjunct);
		return cnf;
	}

	// Methods to convert And/Or classes to Expressions
	
	public static Expression convertDNFListsToExpression(List<List<Expression>> dnf)
	{
		Expression ret = convertConjunctionListToExpression(dnf.get(0));
		for (int i = 1; i < dnf.size(); i++) {
			ret = Expression.Or(ret, convertConjunctionListToExpression(dnf.get(i)));
		}
		return ret;
	}

	public static Expression convertCNFListsToExpression(List<List<Expression>> cnf)
	{
		Expression ret = convertDisjunctionListToExpression(cnf.get(0));
		for (int i = 1; i < cnf.size(); i++) {
			ret = Expression.And(ret, convertDisjunctionListToExpression(cnf.get(i)));
		}
		return ret;
	}

	public static Expression convertDisjunctionListToExpression(List<Expression> disjunction)
	{
		Expression ret = disjunction.get(0);
		for (int i = 1; i < disjunction.size(); i++) {
			ret = Expression.Or(ret, disjunction.get(i));
		}
		return ret;
	}

	public static Expression convertConjunctionListToExpression(List<Expression> conjunction)
	{
		Expression ret = conjunction.get(0);
		for (int i = 1; i < conjunction.size(); i++) {
			ret = Expression.And(ret, conjunction.get(i));
		}
		return ret;
	}

	// Test code
	
	public static void main(String args[])
	{
		PrismParser parser = new PrismParser();
		String ss[] = new String[] { "a&!(b=>c)", "(a|b)&(c|d|e)" };
		for (String s : ss) {
			try {
				Expression expr = parser.parseSingleExpression(new ByteArrayInputStream(s.getBytes()));
				System.out.println(expr + " in CNF is " + convertToCNF(expr.deepCopy()));
				System.out.println(expr + " in DNF is " + convertToDNF(expr.deepCopy()));
			} catch (PrismException e) {
				System.out.println("Error: " + e.getMessage());
			}
		}
	}
}