iclause.java

来自「Java版的SAT求解器」· Java 代码 · 共 44 行

/*
 * IBooleanLiteral.java
 *
 * Copyright 2004-2005 Positronic Software.
 *
 */

package positronic.satisfiability.elements;

import java.util.*;

 /** The <code>IClause</code> interface must be implemented by any class
  * definition of <code>Clause</code> contempleted as an alternative to
  * the <code>Clause</code> class provided by this package.
  *
  * @author  Kerry Michael Soileau
  * @version 1.1, 05/07/22
  */

public interface IClause extends Comparable
{
	boolean add(IBooleanLiteral b) throws Exception;
  Object clone();
  boolean contains(IBooleanLiteral bl) throws Exception;
  IBooleanLiteral differsSinglyFrom(IClause c) throws Exception;
  boolean dominates(IClause clause) throws Exception;
  Object[] getBooleanVariables();
  void getBooleanVariables(List hs) throws Exception;
  IBooleanLiteral getLiteralAt(int n) throws Exception;
  boolean isEmpty();
  boolean isMemberOf(List h) throws Exception;
  boolean isSatisfied();
  boolean isSingleton();
  IClause minus(IClause o) throws Exception;
  IClause or(IBooleanVariable bv) throws Exception;
  IClause orNot(IBooleanVariable bv) throws Exception;
  boolean remove(IBooleanLiteral b);
  Object remove(int i);
  IClause resolve(IBooleanLiteral ib) throws Exception;
  IClause resolve(IBooleanVariable b, boolean value) throws Exception;
  int size();
  IClause substitute(Map h) throws Exception;
  Object[] toArray();
}