net.sf.bddbddb
Class BDDSolver

java.lang.Object
  net.sf.bddbddb.Solver
      net.sf.bddbddb.BDDSolver

public class BDDSolver
extends Solver

An implementation of Solver that uses BDDs.

Version:

$Id: BDDSolver.java 652 2007-03-06 07:31:06Z joewhaley $

Author:

jwhaley

Nested Class Summary

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

Solver.MyReader

Field Summary

static java.lang.String	bddDomainInfoFileName Filename for BDD domain info file.
java.lang.String	BDDREORDER
java.lang.String	TRIALFILE
java.lang.String	VARORDER BDD variable ordering.

Fields inherited from class net.sf.bddbddb.Solver

err, out, startTime

Constructor Summary

BDDSolver()
Constructs a new BDD solver.

Method Summary

net.sf.javabdd.BDDDomain	allocateBDDDomain(Domain dom) Allocate a new BDD domain that matches the given domain.
void	cleanup() Clean up the solver, freeing the memory associated with it.
InferenceRule	createInferenceRule(java.util.List top, RuleTerm bottom) Create a new inference rule.
Relation	createRelation(java.lang.String name, java.util.List attributes) Create a new relation.
void	ensureCapacity(Domain d, java.math.BigInteger range)
void	ensureCapacity(Domain d, long v)
void	finish() Called after solving.
java.lang.String	getBaseName()
net.sf.javabdd.BDDDomain	getBDDDomain(Domain dom, int k) Get the k-th BDD domain allocated for a given domain.
net.sf.javabdd.BDDDomain	getBDDDomain(java.lang.String s) Get the BDD domain with the given name.
jwutil.collections.MultiMap	getBDDDomains() Return the map of field domains to sets of allocated BDD domains.
java.util.Collection	getBDDDomains(Domain dom) Get the set of BDD domains allocated for a given domain.
net.sf.javabdd.BDDFactory	getBDDFactory() Get the BDD factory used by this solver.
net.sf.javabdd.BDDPairing	getPairing(java.util.Map map)
void	initialize() Initialize all of the relations and rules.
void	initialize2() Initialize the values of equivalence relations.
void	reportStats() Report rule statistics.
void	setVariableOrdering() Set the BDD variable ordering based on VARORDER.
void	solve() Solve the rules.

Methods inherited from class net.sf.bddbddb.Solver

addBDDLibraryToClasspath, addSaveHook, clear, doCallbacks, execSolver, getBaseDir, getComparisonRelations, getDomain, getIterationFlowGraph, getNumberOfRelations, getRelation, getRelation, getRelations, getRelationsToLoad, getRelationsToSave, getRule, getRule, getRules, getRuleThatContains, load, load, main, main2, printUsage, run, save, stratify

Methods inherited from class java.lang.Object

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

Field Detail

bddDomainInfoFileName

public static java.lang.String bddDomainInfoFileName

Filename for BDD domain info file. The BDD domain info file contains the list of domains that are allocated

VARORDER

public java.lang.String VARORDER

BDD variable ordering.

TRIALFILE

public java.lang.String TRIALFILE

BDDREORDER

public java.lang.String BDDREORDER

Constructor Detail

BDDSolver

public BDDSolver()

Constructs a new BDD solver. Also initializes the BDD library.

Method Detail

getPairing

public net.sf.javabdd.BDDPairing getPairing(java.util.Map map)

ensureCapacity

public void ensureCapacity(Domain d,
                           long v)

ensureCapacity

public void ensureCapacity(Domain d,
                           java.math.BigInteger range)

initialize

public void initialize()

Description copied from class: Solver

Initialize all of the relations and rules.

Overrides:

initialize in class Solver

getBaseName

public java.lang.String getBaseName()

initialize2

public void initialize2()

Initialize the values of equivalence relations.

setVariableOrdering

public void setVariableOrdering()

Set the BDD variable ordering based on VARORDER.

solve

public void solve()

Description copied from class: Solver

Solve the rules.

Specified by:

solve in class Solver

finish

public void finish()

Description copied from class: Solver

Called after solving.

Specified by:

finish in class Solver

cleanup

public void cleanup()

Description copied from class: Solver

Clean up the solver, freeing the memory associated with it.

Specified by:

cleanup in class Solver

allocateBDDDomain

public net.sf.javabdd.BDDDomain allocateBDDDomain(Domain dom)

Allocate a new BDD domain that matches the given domain.

Parameters:

dom - domain to match

Returns:

new BDD domain

getBDDDomains

public java.util.Collection getBDDDomains(Domain dom)

Get the set of BDD domains allocated for a given domain.

Parameters:

dom - domain

Returns:

set of BDD domains

getBDDDomain

public net.sf.javabdd.BDDDomain getBDDDomain(Domain dom,
                                             int k)

Get the k-th BDD domain allocated for a given domain.

Parameters:

dom - domain

k - index

Returns:

k-th BDD domain allocated for the given domain

getBDDDomain

public net.sf.javabdd.BDDDomain getBDDDomain(java.lang.String s)

Get the BDD domain with the given name.

Parameters:

s - name of BDD domain

Returns:

BDD domain with the given name

getBDDDomains

public jwutil.collections.MultiMap getBDDDomains()

Return the map of field domains to sets of allocated BDD domains.

Returns:

map between field domains and sets of allocated BDD domains

createInferenceRule

public InferenceRule createInferenceRule(java.util.List top,
                                         RuleTerm bottom)

Description copied from class: Solver

Create a new inference rule.

Parameters:

top - list of subgoals of rule

bottom - head of rule

Returns:

new inference rule

createRelation

public Relation createRelation(java.lang.String name,
                               java.util.List attributes)

Description copied from class: Solver

Create a new relation.

Specified by:

createRelation in class Solver

Parameters:

name - name of relation

attributes - attributes of relation

Returns:

new relation

reportStats

public void reportStats()

Description copied from class: Solver

Report rule statistics.

getBDDFactory

public net.sf.javabdd.BDDFactory getBDDFactory()

Get the BDD factory used by this solver.

Returns:

BDD factory