revisionlogic
Class ISent

java.lang.Object
  revisionlogic.ISent

Direct Known Subclasses:

Atom, BinaryCompound, Contradiction, MultipleCompound, Negation, Tautology

public abstract class ISent

extends java.lang.Object

ISent is an abstract class with a specific interface and some default implementations for sentences. The concrete subclasses of ISent must implement functions specified in the interface and may override ISent's default implementations.

Author:

Daphne Liu, daphnel@sfu.ca; Sven Thiele, sthiele@rz.uni-potsdam.de

Field Summary

static int	ATOM An int indicating the atomic sentence type.
static int	BIIMP An int indicating the biconditional sentence type.
static int	CONJ An int indicating the conjunction sentence type.
static int	CONT An int indicating the contradiction sentence type.
static int	DIS An int indicating the disjunction sentence type.
static int	IMP An int indicating the implication sentence type.
static int	NEG An int indicating the negation sentence type.
static int	TAUT An int indicating the tautological sentence type.

Constructor Summary

ISent()

Method Summary

abstract java.lang.Object	clone() Creates and returns a clone of this sentence.
(package private) abstract ISent	conjunctionsIn() Returns a reference to an equivalent ISent sentence, in which the outer conjunction signs are moved inside in the DNF transformation.
(package private) abstract ISent	disjunctionsIn() Returns a reference to an equivalent ISent sentence, in which the outer disjunction signs are moved inside in the CNF transformation.
abstract boolean	equals(java.lang.Object s) Checks if this sentence equals s.
(package private) abstract java.util.HashSet	getAtoms() Returns a set consisting of the literals of this sentence.
ISent	getCNF() Returns a reference to an equivalence ISent sentence after the cnf transformation.
ISent	getCNFUI() Returns a reference to an equivalence ISent sentence after the cnf transformation.
(package private) abstract int	getDepth() Returns the depth (levels of nesting) of this sentence.
(package private) java.lang.String	getDIMACSFormat(boolean isCNF) Returns the DIMACS string representation of this sentence as an input to the external satisfiability solver.
ISent	getDNFUI() Returns a reference to an equivalence ISent sentence after the dnf transformation.
java.lang.String	getLabel() Returns the string representation of this sentence.
(package private) abstract java.lang.StringBuffer	getLabelSB() Returns a string buffer holding the string representation of this sentence.
abstract int	getType() Returns the type of this sentence.
(package private) abstract ISent	implicationsOut() Returns a reference to an equivalent ISent sentence, in which, all the implications have been replaced with disjunctions, and all the biconditionals with a conjunction of two disjunctions.
boolean	isConsistent() Checks if this sentence is consistent and satisfiable.
(package private) boolean	isConsistent(ISent s0) Checks if this sentence is consistent with s0.
(package private) boolean	isConsistent(java.util.Vector v) Checks if this sentence is consistent with the conjunction of the sentences in v.
static boolean	isInconsistentSList(ISent cnfForm) Checks if the CNF sentence cnfForm is consistent and satisfiable.
(package private) boolean	isprConsistent() Checks if this CNF sentence is consistent and satisfiable.
(package private) abstract ISent	negationsIn() Returns a reference to an equivalent ISent sentence, in which the negation signs appear only on the literals.

Methods inherited from class java.lang.Object

finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ATOM

public static final int ATOM

An int indicating the atomic sentence type.

See Also:

Constant Field Values

NEG

public static final int NEG

An int indicating the negation sentence type.

See Also:

Constant Field Values

CONJ

public static final int CONJ

An int indicating the conjunction sentence type.

See Also:

Constant Field Values

DIS

public static final int DIS

An int indicating the disjunction sentence type.

See Also:

Constant Field Values

IMP

public static final int IMP

An int indicating the implication sentence type.

See Also:

Constant Field Values

BIIMP

public static final int BIIMP

An int indicating the biconditional sentence type.

See Also:

Constant Field Values

TAUT

public static final int TAUT

An int indicating the tautological sentence type.

See Also:

Constant Field Values

CONT

public static final int CONT

An int indicating the contradiction sentence type.

See Also:

Constant Field Values

Constructor Detail

ISent

public ISent()

Method Detail

implicationsOut

abstract ISent implicationsOut()

Returns a reference to an equivalent ISent sentence, in which, all the implications have been replaced with disjunctions, and all the biconditionals with a conjunction of two disjunctions.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a reference to an equivalent ISent sentence after the replacement of implications and biconditionals.

negationsIn

abstract ISent negationsIn()

Returns a reference to an equivalent ISent sentence, in which the negation signs appear only on the literals.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a reference to an equivalent ISent sentence after the re-distribution of the outer negation signs.

disjunctionsIn

abstract ISent disjunctionsIn()

Returns a reference to an equivalent ISent sentence, in which the outer disjunction signs are moved inside in the CNF transformation.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a reference to an equivalent ISent sentence after the re-distribution of the outer disjunction signs.

conjunctionsIn

abstract ISent conjunctionsIn()

Returns a reference to an equivalent ISent sentence, in which the outer conjunction signs are moved inside in the DNF transformation.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a reference to an equivalent ISent sentence after the re-distribution of the outer conjunction signs.

getDepth

abstract int getDepth()

Returns the depth (levels of nesting) of this sentence.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

an int indicating the depth of this sentence.

getLabelSB

abstract java.lang.StringBuffer getLabelSB()

Returns a string buffer holding the string representation of this sentence.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a string buffer holding the string representation of this sentence.

getAtoms

abstract java.util.HashSet getAtoms()

Returns a set consisting of the literals of this sentence.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a HashSet consisting of the literals of this sentence.

equals

public abstract boolean equals(java.lang.Object s)

Checks if this sentence equals s.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

true if s is a sentence of the same type with equal operands, false otherwise.

getType

public abstract int getType()

Returns the type of this sentence.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

an int indicating the sentence type.

clone

public abstract java.lang.Object clone()

Creates and returns a clone of this sentence.

This is an abstract method specification for the concrete subclasses of ISent.

Returns:

a reference to a clone of this sentence.

getLabel

public java.lang.String getLabel()

Returns the string representation of this sentence.

This is the default implementation for sentences.

Returns:

the string representation of this sentence.

getCNFUI

public ISent getCNFUI()

Returns a reference to an equivalence ISent sentence after the cnf transformation.

This is the default implementation for sentences. This method is invoked only by the ListSent constructors.

Returns:

a reference to an equivalence ISent in the CNF format.

getDNFUI

public ISent getDNFUI()

Returns a reference to an equivalence ISent sentence after the dnf transformation.

This is the default implementation for sentences. This method is invoked only by the ListSent constructors.

Returns:

a reference to an equivalence ISent in the DNF format.

isConsistent

public boolean isConsistent()

Checks if this sentence is consistent and satisfiable.

Returns:

true if this sentence is consistent and satisfiable, false otherwise.

isInconsistentSList

public static boolean isInconsistentSList(ISent cnfForm)

Checks if the CNF sentence cnfForm is consistent and satisfiable.

Parameters:

cnfForm - a reference to the CNF sentence to be checked for satisfiability.

Returns:

true if cnfForm is consistent and satisfiable.

isConsistent

boolean isConsistent(ISent s0)

Checks if this sentence is consistent with s0.

Parameters:

s0 - a reference to the sentence to be checked against this sentence.

Returns:

true if this sentence is consistent with s0, false otherwise.

isConsistent

boolean isConsistent(java.util.Vector v)

Checks if this sentence is consistent with the conjunction of the sentences in v.

Parameters:

v - the Vector of sentences whose conjunction are to be checked against this sentence.

Returns:

true if this sentence is consistent with the conjunction of the sentences in v, false otherwise.

isprConsistent

boolean isprConsistent()

Checks if this CNF sentence is consistent and satisfiable.

This method can be invoked only by ISent instances already in the CNF format.

Returns:

true if this CNF sentence is consistent and satisfiable, false otherwise.

getCNF

public ISent getCNF()

Returns a reference to an equivalence ISent sentence after the cnf transformation.

This is the default implementation for sentences.

Returns:

a reference to an equivalence ISent in the CNF format.

getDIMACSFormat

java.lang.String getDIMACSFormat(boolean isCNF)

Returns the DIMACS string representation of this sentence as an input to the external satisfiability solver.

This is the default implementation for sentences.

Parameters:

isCNF - a boolean which is true if this sentence is already in the CNF format, false otherwise.

Returns:

the DIMACS string representation of this sentence.