LogicalDBInterface.java

Go to the documentation of this file.

/*
 * (c) copyright 2008, Technische Universitaet Graz and Technische Universitaet Wien
 *
 * This file is part of jdiagengine.
 *
 * jdiagengine 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 3 of the License, or
 * (at your option) any later version.
 *
 * jdiagengine 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 jdiagengine. If not, see <http://www.gnu.org/licenses/>.
 *
 * Authors: Joerg Weber, Franz Wotawa
 * Contact: jweber@ist.tugraz.at (preferred), or fwotawa@ist.tugraz.at
 *
 */


package ATPInterface;

import java.util.ArrayList;
import java.util.BitSet;

import theoremprover.IllegalAssumption;

public interface LogicalDBInterface {

    int addRules(String subDB, boolean replace, ArrayList newRules) 
        throws LogicParseException;

    int addFDGEdges(ArrayList edgeStrings, boolean replace) throws LogicParseException;

    boolean checkConsistency(boolean useFaultModes)
        throws LogicParseException;

    /*
     * Queries is a list of strings representing propositions. For each query q,
     * this method checks separately if "SD |_| OBS |_| {-ab(c) | c in COMP} |_| q"
     * holds (i.e., if q is consistent with all the other sentences).
     *
     * For any query q at index i in queries, the value of bit i in the BitSet result indicates
     * whether q is entailed.
     */
    void performConsistencyChecks(ArrayList queries, boolean useFaultModes, BitSet result)
        throws LogicParseException;

    ArrayList computeMinDiag(int maxExplSize, int maxNumExpl,
                             boolean useFaultModes, boolean verboseOutput)
        throws LogicParseException, IllegalAssumption;

    ArrayList computeDEs(int maxExplSize, int maxNumExpl,
                         boolean computeBetaDE, int maxDFChainSize, boolean mergeDEs,
                         boolean discardOrderPerms, ArrayList minDiags)
        throws LogicParseException, IllegalAssumption;
    
    int getTotalNumRules();

    int getSubDBNumRules(String subDB);
    
    ArrayList createSubDBStats();

    ArrayList getSubDBRules(String name);

    /*
     * Returns statistical data on the Failure Dep. Graph.
     */
    public FDGStat createFDGStats();
}