org.kahina.logic.sat.muc

Class MUCState

java.lang.Object

org.kahina.core.KahinaState

org.kahina.logic.sat.muc.MUCState

All Implemented Interfaces:

java.io.Serializable, KahinaListener

public class MUCState
extends KahinaState

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
static boolean	VERBOSE

Fields inherited from class org.kahina.core.KahinaState

consoleLines, consoleMessages, matchCountByBreakpoint, warnThresholdByBreakpoint

Constructor Summary

Constructors

Constructor and Description
MUCState(MUCInstance kahina)
MUCState(MUCInstance kahina, CnfSatInstance satInstance, MUCStatistics stat, MiniSATFiles files)

Method Summary

Methods

Modifier and Type	Method and Description
void	addAndDistributeIrreducibilityInfo(int parentID, int failedReductionID)
void	addAndDistributeReducibilityInfo(int childID, int reductionID, int link)
int	autarkyReduction(int ucID)
BlocklessBlockHandler	getBlocklessBlocks()
java.util.List<java.util.TreeSet<java.lang.Integer>>	getBlocksForUC(int ucID)
ColoredPathDAG	getDecisionGraph()
MiniSATFiles	getFiles()
MUCInstance	getKahina()
MUCMetaInstance	getMetaInstance()
PartitionBlockHandler	getPartitionBlocks()
RecursiveBlockHandler	getRecursiveBlocks()
UCReducerList	getReducers()
CnfSatInstance	getSatInstance()
MUCStep	getSelectedStep()
MUCStatistics	getStatistics()
void	initialize()
void	learnMetaBlock(java.util.TreeSet<java.lang.Integer> metaBlock)
void	learnMetaClause(java.util.TreeSet<java.lang.Integer> metaClause)
void	learnMetaUnits(MUCStep uc)
void	modelRotation(CompleteAssignment model, int ucID, int transClID, java.util.TreeSet<java.lang.Integer> derivedCritical)
protected void	processSelection()
void	propagateIrreducibilityInfo(int parentID, int childID)
void	propagateReducibilityInfo(int childID, int parentID)
int	registerMUC(java.lang.Integer[] mucCandidates, java.lang.Integer[] muc, MUCInstruction lastInstruction, int parentID)
int	registerMUC(MUCStep newStep, int parentID, java.util.List<java.lang.Integer> selCandidates)
void	reset()
void	setFiles(MiniSATFiles files)
void	setSatInstance(CnfSatInstance satInstance)
void	setStatistics(MUCStatistics stat)
void	updateDecisionNode(int stepID)
boolean	usesBlocks()
boolean	usesMetaLearning()

Methods inherited from class org.kahina.core.KahinaState

consoleMessage, get, getConsoleMessages, getLineReferencesForStep, getMatchCountByBreakpoint, getSelectedStepID, getStepCount, getSteps, getWarnThresholdByBreakpoint, loadSteps, nextStepID, processEvent, retrieve, store

Methods inherited from class java.lang.Object

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

Field Detail

VERBOSE

public static boolean VERBOSE

Constructor Detail

MUCState

public MUCState(MUCInstance kahina)

MUCState

public MUCState(MUCInstance kahina,
        CnfSatInstance satInstance,
        MUCStatistics stat,
        MiniSATFiles files)

Method Detail

initialize

public void initialize()

Overrides:

initialize in class KahinaState

reset

public void reset()

getKahina

public MUCInstance getKahina()

usesBlocks

public boolean usesBlocks()

usesMetaLearning

public boolean usesMetaLearning()

getSelectedStep

public MUCStep getSelectedStep()

getSatInstance

public CnfSatInstance getSatInstance()

getMetaInstance

public MUCMetaInstance getMetaInstance()

getStatistics

public MUCStatistics getStatistics()

getFiles

public MiniSATFiles getFiles()

getDecisionGraph

public ColoredPathDAG getDecisionGraph()

getReducers

public UCReducerList getReducers()

getBlocklessBlocks

public BlocklessBlockHandler getBlocklessBlocks()

getPartitionBlocks

public PartitionBlockHandler getPartitionBlocks()

getRecursiveBlocks

public RecursiveBlockHandler getRecursiveBlocks()

getBlocksForUC

public java.util.List<java.util.TreeSet<java.lang.Integer>> getBlocksForUC(int ucID)

registerMUC

public int registerMUC(MUCStep newStep,
              int parentID,
              java.util.List<java.lang.Integer> selCandidates)

registerMUC

public int registerMUC(java.lang.Integer[] mucCandidates,
              java.lang.Integer[] muc,
              MUCInstruction lastInstruction,
              int parentID)

setSatInstance

public void setSatInstance(CnfSatInstance satInstance)

setStatistics

public void setStatistics(MUCStatistics stat)

setFiles

public void setFiles(MiniSATFiles files)

processSelection

protected void processSelection()

Overrides:

processSelection in class KahinaState

autarkyReduction

public int autarkyReduction(int ucID)

modelRotation

public void modelRotation(CompleteAssignment model,
                 int ucID,
                 int transClID,
                 java.util.TreeSet<java.lang.Integer> derivedCritical)

learnMetaBlock

public void learnMetaBlock(java.util.TreeSet<java.lang.Integer> metaBlock)

learnMetaClause

public void learnMetaClause(java.util.TreeSet<java.lang.Integer> metaClause)

learnMetaUnits

public void learnMetaUnits(MUCStep uc)

addAndDistributeIrreducibilityInfo

public void addAndDistributeIrreducibilityInfo(int parentID,
                                      int failedReductionID)

addAndDistributeReducibilityInfo

public void addAndDistributeReducibilityInfo(int childID,
                                    int reductionID,
                                    int link)

propagateIrreducibilityInfo

public void propagateIrreducibilityInfo(int parentID,
                               int childID)

propagateReducibilityInfo

public void propagateReducibilityInfo(int childID,
                             int parentID)

updateDecisionNode

public void updateDecisionNode(int stepID)