net.sf.bddbddb
Class BDDInferenceRule

java.lang.Object
  extended by net.sf.bddbddb.InferenceRule
      extended by 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


Copyright © 2004-2008 Stanford SUIF Compiler Group. All Rights Reserved.