/* $Id: LogicalEquivalence.java,v 1.3 2005/06/08 21:55:56 m31 Exp $
 *
 * This file is part of the project "Hilbert II" - http://www.qedeq.org
 *
 * Copyright 2000-2005,  Michael Meyling <mime@qedeq.org>.
 *
 * "Hilbert II" 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.
 *
 * This program 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.
 */

package org.qedeq.kernel.bo.logic;

import org.qedeq.kernel.base.elli.Element;


/**
 * This class deals with {@link org.qedeq.kernel.base.elli.Element}s and could check
 * if two formulas are logically equivalent.
 *
 * TODO mime 20050205: work in progress
 *
 * @version $Revision: 1.3 $
 * @author  Michael Meyling
 */
public final class LogicalEquivalence {

    /**
     * Constructor.
     */
    private LogicalEquivalence() {
        // nothing to do
    }

    /**
     * Assures that two words are logically equivalent.
     *
     * @param   formula1    First formula.
     * @param   formula2    Second formula.
     * @throws  CheckException  Check failed.
     */
    public static final void checkEquivalence(final Element formula1,
            final Element formula2)
            throws CheckException {
        if (formula1.equals(formula2)) {
            return;
        }
        if (formula1.isAtom() || formula2.isAtom()) {
            return; // TODO mime 20050330: where is the check???
        }
        final String op1 = formula1.getList().getOperator();
        final String op2 = formula2.getList().getOperator();
        if (op1.equals(op2) && (op1.equals(FormulaChecker.CONJUNCTION_OPERATOR)
                || op1.equals(FormulaChecker.DISJUNCTION_OPERATOR))) {
            final EqualFormulaSet sub1 = new EqualFormulaSet(formula1.getList());
            final EqualFormulaSet sub2 = new EqualFormulaSet(formula2.getList());
            if (sub1.equals(sub2)) {
                return;
            }

        }
        throw new CheckException("no logical equivalence found", formula2);
    }

}