edu::tum::cs::logic::sat::weighted::WeightedClausalKB Class Reference

List of all members.

Public Member Functions
void	addClause (WeightedClause wc)
void	addClause (WeightedFormula wf, WeightedClause wc)
void	addFormula (WeightedFormula wf, boolean makeWeightPositive) throws Exception
HashMap< WeightedClause, Formula >	getClause2Formula ()
Set< Entry< WeightedFormula, Vector< WeightedClause > > >	getFormulasAndClauses ()
Iterator< WeightedClause >	iterator ()
void	print ()
int	size ()
	WeightedClausalKB ()
	WeightedClausalKB (Iterable< WeightedFormula > kb, boolean requirePositiveWeights) throws Exception
Protected Attributes
HashMap< WeightedClause, Formula >	cl2Formula
Vector< WeightedClause >	clauses
edu.tum.cs.util.datastruct.Map2List < WeightedFormula, WeightedClause >	formula2clauses

---

Detailed Description

A knowledge base of weighted clauses that is built up from general weighted formulas (retaining a mapping from formulas to clauses and vice versa)

Author:

wernickr, jain

Definition at line 18 of file WeightedClausalKB.java.

---

Constructor & Destructor Documentation

edu::tum::cs::logic::sat::weighted::WeightedClausalKB::WeightedClausalKB	(	Iterable< WeightedFormula >	kb,
		boolean	requirePositiveWeights
	)			throws Exception [inline]

constructs a weighted clausal KB from a collection of weighted formulas

Parameters:

	kb	some collection of weighted formulas
	requirePositiveWeights	whether to negate formulas with negative weights to yield positive weights only

Exceptions:

java.lang.Exception

Definition at line 30 of file WeightedClausalKB.java.

edu::tum::cs::logic::sat::weighted::WeightedClausalKB::WeightedClausalKB

(

)

[inline]

constructs an empty weighted clausal KB

Definition at line 40 of file WeightedClausalKB.java.

---

Member Function Documentation

void edu::tum::cs::logic::sat::weighted::WeightedClausalKB::addClause

(

WeightedClause

wc

)

[inline]

adds a weighted clause to the KB (where the weighted formula the clause originated from is the clause itself)

Parameters:

wc

the weighted clause to add

Definition at line 93 of file WeightedClausalKB.java.

void edu::tum::cs::logic::sat::weighted::WeightedClausalKB::addClause	(	WeightedFormula	wf,
		WeightedClause	wc
	)			[inline]

adds a weighted clause to this KB

Parameters:

	wf	the weighted formula whose CNF the clause appears in
	wc	the clause to add

Definition at line 83 of file WeightedClausalKB.java.

void edu::tum::cs::logic::sat::weighted::WeightedClausalKB::addFormula	(	WeightedFormula	wf,
		boolean	makeWeightPositive
	)			throws Exception [inline]

adds an arbitrary formula to the knowledge base (converting it to CNF and splitting it into clauses)

Parameters:

	wf	formula whose clauses to add (it is automatically converted to CNF and split into clauses; the association between the formula and its clauses is retained)
	makeWeightPositive	whether to negate the formula if its weight is negative

Exceptions:

java.lang.Exception

Definition at line 52 of file WeightedClausalKB.java.

HashMap<WeightedClause, Formula> edu::tum::cs::logic::sat::weighted::WeightedClausalKB::getClause2Formula

(

)

[inline]

Returns:

a mapping from weighted clauses to the original formulas they were part of.

Definition at line 125 of file WeightedClausalKB.java.

Set<Entry<WeightedFormula,Vector<WeightedClause> > > edu::tum::cs::logic::sat::weighted::WeightedClausalKB::getFormulasAndClauses

(

)

[inline]

gets a set of entries with formulas and the clauses that the formulas are made up of when converted to CNF

Returns:

Definition at line 133 of file WeightedClausalKB.java.

Iterator<WeightedClause> edu::tum::cs::logic::sat::weighted::WeightedClausalKB::iterator

(

)

[inline]

Method returns the iterator of the weighted clauses in knowledge base.

Returns:

Iterator of weighted clauses

Definition at line 101 of file WeightedClausalKB.java.

void edu::tum::cs::logic::sat::weighted::WeightedClausalKB::print

(

)

[inline]

prints all weighted clauses in the knowledge base to stdout

Definition at line 116 of file WeightedClausalKB.java.

int edu::tum::cs::logic::sat::weighted::WeightedClausalKB::size

(

)

[inline]

returns the number of weighted clauses in the knowledge base.

Returns:

size of the knowledge base (number of weighted clauses)

Definition at line 109 of file WeightedClausalKB.java.

---

Member Data Documentation

HashMap<WeightedClause, Formula> edu::tum::cs::logic::sat::weighted::WeightedClausalKB::cl2Formula [protected]

Definition at line 21 of file WeightedClausalKB.java.

Vector<WeightedClause> edu::tum::cs::logic::sat::weighted::WeightedClausalKB::clauses [protected]

Definition at line 20 of file WeightedClausalKB.java.

edu.tum.cs.util.datastruct.Map2List<WeightedFormula, WeightedClause> edu::tum::cs::logic::sat::weighted::WeightedClausalKB::formula2clauses [protected]

Definition at line 22 of file WeightedClausalKB.java.

---

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

• WeightedClausalKB.java