org.kahina.logic.sat.muc.data

Class MUCMetaInstance

java.lang.Object

org.kahina.core.data.KahinaObject

org.kahina.logic.sat.data.KahinaSatInstance

org.kahina.logic.sat.data.cnf.CnfSatInstance

org.kahina.logic.sat.muc.data.MUCMetaInstance

All Implemented Interfaces:

java.io.Serializable

public class MUCMetaInstance
extends CnfSatInstance

See Also:

Serialized Form

Field Summary

Fields inherited from class org.kahina.logic.sat.data.cnf.CnfSatInstance

clauseIDs, clauseStore, maxVarID, needsRebuild, occurrenceMap, reverseConversionTable

Fields inherited from class org.kahina.logic.sat.data.KahinaSatInstance

symbolTable

Fields inherited from class org.kahina.core.data.KahinaObject

needsUpdate

Constructor Summary

Constructors

Constructor and Description
MUCMetaInstance(int numOrigClauses)

Method Summary

Methods

Modifier and Type	Method and Description
java.util.Collection<java.util.TreeSet<java.lang.Integer>>	getBlocks()
void	learnNewBlock(java.util.TreeSet<java.lang.Integer> block)
void	learnNewClause(java.util.TreeSet<java.lang.Integer> clause)
void	setBlockHandler(LiteralBlockHandler blockHandler)

Methods inherited from class org.kahina.logic.sat.data.cnf.CnfSatInstance

addClause, announceAddedClauses, announceChangedClauses, applyAssignmentDestructively, applyDontCareFilter, computeOccurrenceMap, copy, deleteVariablesDestructively, deriveUnitsByPropagation, discardOccurrenceMap, extractMaxAutarkyDestructively, generateClauseToIndexMap, getClause, getClauseByID, getCountOccourrence, getHighestVar, getNumVariables, getSize, getSubsumedClauseIndices, idxToId, isDontCareClause, needsRebuild, needsUpdate, printAllClauses, reduceToLeanKernel, removeClauseID, removeClauseIndex, selectClauses, setSubsumptionCheck

Methods inherited from class org.kahina.logic.sat.data.KahinaSatInstance

getSymbolForLiteral, setSymbolMapping

Methods inherited from class org.kahina.core.data.KahinaObject

requireUpdate

Methods inherited from class java.lang.Object

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

Constructor Detail

MUCMetaInstance

public MUCMetaInstance(int numOrigClauses)

Method Detail

setBlockHandler

public void setBlockHandler(LiteralBlockHandler blockHandler)

learnNewBlock

public void learnNewBlock(java.util.TreeSet<java.lang.Integer> block)

learnNewClause

public void learnNewClause(java.util.TreeSet<java.lang.Integer> clause)

getBlocks

public java.util.Collection<java.util.TreeSet<java.lang.Integer>> getBlocks()