edu::tum::cs::logic::Formula Class Reference

Inheritance diagram for edu::tum::cs::logic::Formula:

[legend]

List of all members.

Public Member Functions
void	addAllGroundingsTo (Collection< Formula > collection, Database db, WorldVariables worldVars, boolean simplify) throws Exception
Vector< Formula >	getAllGroundings (Database db, WorldVariables worldVars, boolean simplify) throws Exception
abstract void	getGroundAtoms (Set< GroundAtom > ret)
abstract void	getVariables (Database db, Map< String, String > ret) throws Exception
abstract Formula	ground (Map< String, String > binding, WorldVariables worldVars, Database db) throws Exception
abstract boolean	isTrue (IPossibleWorld w)
abstract Formula	simplify (Database evidence)
abstract Formula	toCNF ()
abstract Formula	toNNF ()
Static Public Member Functions
static Formula	fromString (String f) throws ParseException
static void	main (String[] args) throws ParseException
Protected Member Functions
void	generateGroundings (Collection< Formula > ret, Database db, Map< String, String > binding, String[] varNames, int i, Map< String, String > var2domName, WorldVariables worldVars, boolean simplify) throws Exception

---

Detailed Description

Definition at line 13 of file Formula.java.

---

Member Function Documentation

void edu::tum::cs::logic::Formula::addAllGroundingsTo	(	Collection< Formula >	collection,
		Database	db,
		WorldVariables	worldVars,
		boolean	simplify
	)			throws Exception [inline]

generates all groundings and adds them to the given collection

Parameters:

	collection
	db
	worldVars
	simplify	whether to use the evidence in the database to simplify ground formulas

Exceptions:

Exception

Definition at line 59 of file Formula.java.

static Formula edu::tum::cs::logic::Formula::fromString

(

String

f

)

throws ParseException [inline, static]

Definition at line 115 of file Formula.java.

void edu::tum::cs::logic::Formula::generateGroundings	(	Collection< Formula >	ret,
		Database	db,
		Map< String, String >	binding,
		String[]	varNames,
		int	i,
		Map< String, String >	var2domName,
		WorldVariables	worldVars,
		boolean	simplify
	)			throws Exception [inline, protected]

recursively generates groundings of the formula

Parameters:

	ret	the collection in which to store the generated groundings
	db	the database in which all usable constant symbols are found
	binding	a mapping of variable names to constant names
	varNames	the variables that are to be grounded
	i	the current index of the variable in varNames to ground next
	var2domName	a mapping of variable names to domain names (that contains as keys at least the variables in varNames)
	worldVars	the collection of variables (ground atoms) that defines the set of possible worlds
	simplify	whether to use the evidence in the database to simplify ground formulas

Exceptions:

Exception

Definition at line 78 of file Formula.java.

Vector<Formula> edu::tum::cs::logic::Formula::getAllGroundings	(	Database	db,
		WorldVariables	worldVars,
		boolean	simplify
	)			throws Exception [inline]

gets a list of all groundings of the formula for a particular set of objects

Parameters:

	db	the database containing all relevant constant symbols (objects) to use for grounding
	worldVars	the collection of variables (ground atoms) that defines the set of possible worlds
	simplify	whether to use the evidence in the database to simplify ground formulas

Returns:

Exceptions:

Exception

Definition at line 45 of file Formula.java.

abstract void edu::tum::cs::logic::Formula::getGroundAtoms

(

Set< GroundAtom >

ret

)

[pure virtual]

gets the set of ground atoms appearing in this (grounded) formula

Parameters:

ret

the set to write to

Implemented in edu::tum::cs::logic::ComplexFormula, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::TrueFalse, and edu::tum::cs::logic::UngroundedFormula.

abstract void edu::tum::cs::logic::Formula::getVariables	(	Database	db,
		Map< String, String >	ret
	)			throws Exception [pure virtual]

gets a mapping from names of meta-variables appearing in the formula to the types/domains they apply to

Parameters:

	db
	ret	mapping in which to store the result

Exceptions:

Exception

Implemented in edu::tum::cs::logic::Atom, edu::tum::cs::logic::ComplexFormula, edu::tum::cs::logic::Equality, edu::tum::cs::logic::Exist, edu::tum::cs::logic::ForAll, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Literal, and edu::tum::cs::logic::TrueFalse.

abstract Formula edu::tum::cs::logic::Formula::ground	(	Map< String, String >	binding,
		WorldVariables	worldVars,
		Database	db
	)			throws Exception [pure virtual]

grounds this formula for a particular binding of its variables

Parameters:

	binding	the variable binding
	worldVars	the set of ground atoms (which is needed to return the ground versions of atoms)
	db	a database containing a set of constants for each type that can be used to ground quantified formulas (can be null if the formula does not contain any quantified variables)

Returns:

Exceptions:

Exception

Implemented in edu::tum::cs::logic::Atom, edu::tum::cs::logic::ComplexFormula, edu::tum::cs::logic::Equality, edu::tum::cs::logic::Exist, edu::tum::cs::logic::ForAll, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Literal, and edu::tum::cs::logic::TrueFalse.

abstract boolean edu::tum::cs::logic::Formula::isTrue

(

IPossibleWorld

w

)

[pure virtual]

Implemented in edu::tum::cs::logic::Biimplication, edu::tum::cs::logic::Conjunction, edu::tum::cs::logic::Disjunction, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Implication, edu::tum::cs::logic::Negation, edu::tum::cs::logic::sat::Clause, edu::tum::cs::logic::TrueFalse, and edu::tum::cs::logic::UngroundedFormula.

static void edu::tum::cs::logic::Formula::main

(

String[]

args

)

throws ParseException [inline, static]

Definition at line 119 of file Formula.java.

abstract Formula edu::tum::cs::logic::Formula::simplify

(

Database

evidence

)

[pure 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)

Returns:

a simplified version of the formula that incorporates the evidence

Implemented in edu::tum::cs::logic::Biimplication, edu::tum::cs::logic::Conjunction, edu::tum::cs::logic::Disjunction, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Implication, edu::tum::cs::logic::Negation, edu::tum::cs::logic::sat::Clause, edu::tum::cs::logic::TrueFalse, and edu::tum::cs::logic::UngroundedFormula.

abstract Formula edu::tum::cs::logic::Formula::toCNF

(

)

[pure virtual]

Implemented in edu::tum::cs::logic::Atom, edu::tum::cs::logic::Biimplication, edu::tum::cs::logic::Conjunction, edu::tum::cs::logic::Disjunction, edu::tum::cs::logic::Equality, edu::tum::cs::logic::Exist, edu::tum::cs::logic::ForAll, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Implication, edu::tum::cs::logic::Literal, edu::tum::cs::logic::Negation, edu::tum::cs::logic::sat::Clause, and edu::tum::cs::logic::TrueFalse.

abstract Formula edu::tum::cs::logic::Formula::toNNF

(

)

[pure virtual]

Implemented in edu::tum::cs::logic::Atom, edu::tum::cs::logic::Biimplication, edu::tum::cs::logic::Conjunction, edu::tum::cs::logic::Disjunction, edu::tum::cs::logic::Equality, edu::tum::cs::logic::Exist, edu::tum::cs::logic::ForAll, edu::tum::cs::logic::GroundAtom, edu::tum::cs::logic::GroundLiteral, edu::tum::cs::logic::Implication, edu::tum::cs::logic::Literal, edu::tum::cs::logic::Negation, edu::tum::cs::logic::sat::Clause, and edu::tum::cs::logic::TrueFalse.

---

The documentation for this class was generated from the following file:

• Formula.java