net.sf.bddbddb
Class BDDInferenceRule

java.lang.Object
  net.sf.bddbddb.InferenceRule
      net.sf.bddbddb.BDDInferenceRule

All Implemented Interfaces:

IterationElement

public class BDDInferenceRule
extends InferenceRule

An implementation of InferenceRule that uses BDDs.

Version:

$Id: BDDInferenceRule.java 650 2006-11-29 08:08:45Z joewhaley $

Author:

jwhaley

Nested Class Summary

class

BDDInferenceRule.VarOrderComparator

Nested classes/interfaces inherited from class net.sf.bddbddb.InferenceRule

InferenceRule.DependenceNavigator

Field Summary

static long	LONG_TIME
static int	MAX_FBO_TRIALS
protected net.sf.javabdd.BDD[]	oldRelationValues Values for subgoals, used for incrementalization.
protected BDDSolver	solver
int	updateCount Number of times update() has been called on this rule.
protected java.util.Map	variableToBDDDomain Map from variables to their BDD domains.

Fields inherited from class net.sf.bddbddb.InferenceRule

bottom, id, necessaryVariables, top, unnecessaryVariables

Method Summary

void	copyOptions(InferenceRule r) Copy the options from another rule into this one.
net.sf.javabdd.BDD	evalRelations(net.sf.javabdd.BDDFactory bdd, net.sf.javabdd.BDD[] relationValues, net.sf.javabdd.BDDVarSet[] canQuantifyAfter, long time)
net.sf.javabdd.BDD[]	evalRelationsIncremental(net.sf.javabdd.BDDFactory bdd, net.sf.javabdd.BDD[] newRelationValues, net.sf.javabdd.BDD[] rallRelationValues, net.sf.javabdd.BDDVarSet[] canQuantifyAfter)
void	free() Free the memory associated with this rule.
void	reportStats() Report statistics about this rule.
java.lang.String	toString()
boolean	update() Update the head relation of this rule based on the subgoal relations.

Methods inherited from class net.sf.bddbddb.InferenceRule

calculateNecessaryVariables, checkUnnecessaryVariables, fromXMLElement, generateIR_incremental, generateIR, getAttribute, getHead, getNecessaryVariables, getRelationToDefiningRule, getRelationToUsingRule, getSubgoals, getUnnecessaryVariables, getVariable, getVariables, getVarNameMap, hashCode, numberOfVariables, split, toXMLElement

Methods inherited from class java.lang.Object

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

Field Detail

solver

protected BDDSolver solver

See Also:

InferenceRule.solver

oldRelationValues

protected net.sf.javabdd.BDD[] oldRelationValues

Values for subgoals, used for incrementalization.

variableToBDDDomain

protected java.util.Map variableToBDDDomain

Map from variables to their BDD domains.

updateCount

public int updateCount

Number of times update() has been called on this rule.

LONG_TIME

public static final long LONG_TIME

See Also:

Constant Field Values

MAX_FBO_TRIALS

public static int MAX_FBO_TRIALS

Method Detail

copyOptions

public void copyOptions(InferenceRule r)

Description copied from class: InferenceRule

Copy the options from another rule into this one.

Overrides:

copyOptions in class InferenceRule

update

public boolean update()

Description copied from class: InferenceRule

Update the head relation of this rule based on the subgoal relations. Returns true if the head relation changed.

Specified by:

update in class InferenceRule

Returns:

true if the head relation changed

evalRelations

public net.sf.javabdd.BDD evalRelations(net.sf.javabdd.BDDFactory bdd,
                                        net.sf.javabdd.BDD[] relationValues,
                                        net.sf.javabdd.BDDVarSet[] canQuantifyAfter,
                                        long time)

evalRelationsIncremental

public net.sf.javabdd.BDD[] evalRelationsIncremental(net.sf.javabdd.BDDFactory bdd,
                                                     net.sf.javabdd.BDD[] newRelationValues,
                                                     net.sf.javabdd.BDD[] rallRelationValues,
                                                     net.sf.javabdd.BDDVarSet[] canQuantifyAfter)

reportStats

public void reportStats()

Description copied from class: InferenceRule

Report statistics about this rule.

Specified by:

reportStats in class InferenceRule

free

public void free()

Description copied from class: InferenceRule

Free the memory associated with this rule. After calling this, the rule can no longer be used.

Overrides:

free in class InferenceRule

toString

public java.lang.String toString()

Overrides:

toString in class InferenceRule