edu::tum::cs::logic::sat::Clause Class Reference

Inheritance diagram for edu::tum::cs::logic::sat::Clause:

Classes
class	TautologyException
Public Member Functions
	Clause (Formula f) throws Exception
boolean	isTrue (IPossibleWorld w)
Formula	simplify (Database evidence)
Formula	toCNF ()
Formula	toNNF ()
String	toString ()
Public Attributes
GroundLiteral[]	lits

Detailed Description

Definition at line 12 of file Clause.java.

Constructor & Destructor Documentation

edu::tum::cs::logic::sat::Clause::Clause ( Formula f ) throws Exception [inline]

Definition at line 16 of file Clause.java.

Member Function Documentation

boolean edu::tum::cs::logic::sat::Clause::isTrue ( IPossibleWorld w ) [inline, virtual]

Implements edu::tum::cs::logic::Formula.

Definition at line 58 of file Clause.java.

Formula edu::tum::cs::logic::sat::Clause::simplify ( Database evidence ) [inline, virtual]

simplifies the formula by removing parts of the formula that can be evaluated

Parameters:

evidence

an evidence database with which to evaluate ground atoms (may be null; if null, will only simplify based on TrueFalse instances appearing within the formula)