[Javabdd-checkins] SF.net SVN: javabdd: [461] trunk/JavaBDD/net/sf/javabdd
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [461] trunk/JavaBDD/net/sf/javabdd
|
From: <joe...@us...> - 2006-07-21 14:32:09
|
Revision: 461 Author: joewhaley Date: 2006-07-21 07:32:02 -0700 (Fri, 21 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=461&view=rev Log Message: ----------- Changed MicroFactory, JDDFactory to use new BDDFactoryIntImpl shared superclass. More bug fixes in the test cases. Now the test cases won't fail if a BDD library doesn't support a (nonessential) operation and throws UnsupportedOperationException. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-21 14:32:02 UTC (rev 461) @@ -588,7 +588,8 @@ allsatProfile[useLevel?LEVEL_r:f.level2Var(LEVEL_r)] = lo_empty ? (byte)1 : (byte)0; BDD rn = lo_empty ? r.high() : r.low(); - for (int v = rn.level() - 1; v > LEVEL_r; --v) { + int v = rn.isOne()||rn.isZero() ? f.varNum() - 1 : rn.level() - 1; + for ( ; v > LEVEL_r; --v) { allsatProfile[useLevel?v:f.level2Var(v)] = -1; } if (!lo_empty) { Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-21 14:32:02 UTC (rev 461) @@ -16,49 +16,49 @@ static final boolean USE_FINALIZER = false; - protected abstract void addref_impl(int v); - protected abstract void delref_impl(int v); - protected abstract int zero_impl(); - protected abstract int one_impl(); - protected abstract int invalid_bdd_impl(); - protected abstract int var_impl(int v); - protected abstract int level_impl(int v); - protected abstract int low_impl(int v); - protected abstract int high_impl(int v); - protected abstract int ithVar_impl(int var); - protected abstract int nithVar_impl(int var); + protected abstract void addref_impl(/*bdd*/int v); + protected abstract void delref_impl(/*bdd*/int v); + protected abstract /*bdd*/int zero_impl(); + protected abstract /*bdd*/int one_impl(); + protected abstract /*bdd*/int invalid_bdd_impl(); + protected abstract int var_impl(/*bdd*/int v); + protected abstract int level_impl(/*bdd*/int v); + protected abstract /*bdd*/int low_impl(/*bdd*/int v); + protected abstract /*bdd*/int high_impl(/*bdd*/int v); + protected abstract /*bdd*/int ithVar_impl(int var); + protected abstract /*bdd*/int nithVar_impl(int var); - protected abstract int ite_impl(int v1, int v2, int v3); - protected abstract int apply_impl(int v1, int v2, BDDOp opr); - protected abstract int not_impl(int v1); - protected abstract int applyAll_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int applyEx_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int applyUni_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int compose_impl(int v1, int v2, int var); - protected abstract int constrain_impl(int v1, int v2); - protected abstract int restrict_impl(int v1, int v2); - protected abstract int simplify_impl(int v1, int v2); - protected abstract int support_impl(int v); - protected abstract int exist_impl(int v1, int v2); - protected abstract int forAll_impl(int v1, int v2); - protected abstract int unique_impl(int v1, int v2); - protected abstract int fullSatOne_impl(int v); + protected abstract /*bdd*/int ite_impl(/*bdd*/int v1, /*bdd*/int v2, /*bdd*/int v3); + protected abstract /*bdd*/int apply_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr); + protected abstract /*bdd*/int not_impl(/*bdd*/int v1); + protected abstract /*bdd*/int applyAll_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int applyEx_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int applyUni_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int compose_impl(/*bdd*/int v1, /*bdd*/int v2, int var); + protected abstract /*bdd*/int constrain_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int restrict_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int simplify_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int support_impl(/*bdd*/int v); + protected abstract /*bdd*/int exist_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int forAll_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int unique_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int fullSatOne_impl(/*bdd*/int v); - protected abstract int replace_impl(int v, BDDPairing p); - protected abstract int veccompose_impl(int v, BDDPairing p); + protected abstract /*bdd*/int replace_impl(/*bdd*/int v, BDDPairing p); + protected abstract /*bdd*/int veccompose_impl(/*bdd*/int v, BDDPairing p); - protected abstract int nodeCount_impl(int v); - protected abstract double pathCount_impl(int v); - protected abstract double satCount_impl(int v); - protected abstract int satOne_impl(int v); - protected abstract int satOne_impl2(int v1, int v2, boolean pol); - protected abstract int nodeCount_impl2(int[] v); - protected abstract int[] varProfile_impl(int v); - protected abstract void printTable_impl(int v); + protected abstract int nodeCount_impl(/*bdd*/int v); + protected abstract double pathCount_impl(/*bdd*/int v); + protected abstract double satCount_impl(/*bdd*/int v); + protected abstract /*bdd*/int satOne_impl(/*bdd*/int v); + protected abstract /*bdd*/int satOne_impl2(/*bdd*/int v1, /*bdd*/int v2, boolean pol); + protected abstract int nodeCount_impl2(/*bdd*/int[] v); + protected abstract int[] varProfile_impl(/*bdd*/int v); + protected abstract void printTable_impl(/*bdd*/int v); public class IntBDD extends BDD { - protected int v; - protected IntBDD(int v) { + protected /*bdd*/int v; + protected IntBDD(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -75,8 +75,8 @@ return makeBDD(applyUni_impl(v, unwrap(that), opr, unwrap(var))); } public BDD applyWith(BDD that, BDDOp opr) { - int v2 = unwrap(that); - int v3 = apply_impl(v, v2, opr); + /*bdd*/int v2 = unwrap(that); + /*bdd*/int v3 = apply_impl(v, v2, opr); addref_impl(v3); delref_impl(v); if (this != that) @@ -146,7 +146,7 @@ return makeBDD(replace_impl(v, pair)); } public BDD replaceWith(BDDPairing pair) { - int v3 = replace_impl(v, pair); + /*bdd*/int v3 = replace_impl(v, pair); addref_impl(v3); delref_impl(v); v = v3; @@ -156,8 +156,8 @@ return makeBDD(restrict_impl(v, unwrap(var))); } public BDD restrictWith(BDD that) { - int v2 = unwrap(that); - int v3 = restrict_impl(v, v2); + /*bdd*/int v2 = unwrap(that); + /*bdd*/int v3 = restrict_impl(v, v2); addref_impl(v3); delref_impl(v); if (this != that) @@ -198,7 +198,7 @@ } public class IntBDDWithFinalizer extends IntBDD { - protected IntBDDWithFinalizer(int v) { + protected IntBDDWithFinalizer(/*bdd*/int v) { super(v); } @@ -214,19 +214,19 @@ } - protected IntBDD makeBDD(int v) { + protected IntBDD makeBDD(/*bdd*/int v) { if (USE_FINALIZER) return new IntBDDWithFinalizer(v); else return new IntBDD(v); } - protected static final int unwrap(BDD b) { + protected static final /*bdd*/int unwrap(BDD b) { return ((IntBDD) b).v; } - protected static final int[] unwrap(Collection/*<BDD>*/ c) { - int[] result = new int[c.size()]; + protected static final /*bdd*/int[] unwrap(Collection/*<BDD>*/ c) { + /*bdd*/int[] result = new /*bdd*/int[c.size()]; int k = -1; for (Iterator i = c.iterator(); i.hasNext(); ) { result[++k] = ((IntBDD) i.next()).v; @@ -235,8 +235,8 @@ } public class IntBDDVarSet extends BDDVarSet { - int v; - private IntBDDVarSet(int v) { + /*bdd*/int v; + private IntBDDVarSet(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -260,8 +260,8 @@ return makeBDDVarSet(apply_impl(v, unwrap(b), or)); } public BDDVarSet intersectWith(BDDVarSet b) { - int v2 = unwrap(b); - int v3 = apply_impl(v, v2, or); + /*bdd*/int v2 = unwrap(b); + /*bdd*/int v3 = apply_impl(v, v2, or); addref_impl(v3); delref_impl(v); if (this != b) @@ -274,7 +274,7 @@ } public int size() { int result = 0; - for (int p = v; p != one_impl(); p = high_impl(p)) { + for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) { if (p == zero_impl()) throw new BDDException("varset contains zero"); ++result; @@ -284,7 +284,7 @@ public int[] toArray() { int[] result = new int[size()]; int k = -1; - for (int p = v; p != one_impl(); p = high_impl(p)) { + for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) { result[++k] = var_impl(p); } return result; @@ -304,14 +304,14 @@ return makeBDDVarSet(apply_impl(v, unwrap(b), and)); } public BDDVarSet union(int var) { - int v2 = ithVar_impl(var); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = ithVar_impl(var); + /*bdd*/int v3 = apply_impl(v, v2, and); delref_impl(v2); return makeBDDVarSet(v3); } public BDDVarSet unionWith(BDDVarSet b) { - int v2 = unwrap(b); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = unwrap(b); + /*bdd*/int v3 = apply_impl(v, v2, and); addref_impl(v3); delref_impl(v); if (this != b) @@ -320,8 +320,8 @@ return this; } public BDDVarSet unionWith(int var) { - int v2 = ithVar_impl(var); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = ithVar_impl(var); + /*bdd*/int v3 = apply_impl(v, v2, and); addref_impl(v3); delref_impl(v); delref_impl(v2); @@ -348,14 +348,14 @@ } - protected IntBDDVarSet makeBDDVarSet(int v) { + protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) { if (USE_FINALIZER) return new IntBDDVarSetWithFinalizer(v); else return new IntBDDVarSet(v); } - protected static final int unwrap(BDDVarSet b) { + protected static final /*bdd*/int unwrap(BDDVarSet b) { return ((IntBDDVarSet) b).v; } @@ -371,11 +371,11 @@ } - public BDD ithVar(int var) { + public BDD ithVar(/*bdd*/int var) { return makeBDD(ithVar_impl(var)); } - public BDD nithVar(int var) { + public BDD nithVar(/*bdd*/int var) { return makeBDD(nithVar_impl(var)); } @@ -399,12 +399,12 @@ return makeBDD(zero_impl()); } - protected int[] to_free = new int[8]; - protected int to_free_length = 0; + protected /*bdd*/int[] to_free = new /*bdd*/int[8]; + protected /*bdd*/int to_free_length = 0; public void deferredFree(int v) { synchronized(to_free) { if (to_free_length == to_free.length) { - int[] t = new int[to_free.length * 2]; + /*bdd*/int[] t = new /*bdd*/int[to_free.length * 2]; System.arraycopy(to_free, 0, t, 0, to_free.length); to_free = t; } Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-21 14:32:02 UTC (rev 461) @@ -3,632 +3,257 @@ // Licensed under the terms of the GNU LGPL; see COPYING for details. package net.sf.javabdd; -import java.util.Collection; -import java.math.BigInteger; +import java.lang.reflect.Method; - /** * JDDFactory * * @author John Whaley * @version $Id$ */ -public class JDDFactory extends BDDFactory { +public class JDDFactory extends BDDFactoryIntImpl { - private final jdd.bdd.BDD bdd; - private int[] vars; // indexed by EXTERNAL - private int[] level2var; // internal -> external - private int[] var2level; // external -> internal + public static final String REVISION = "$Revision$"; - private JDDFactory(int nodenum, int cachesize) { - bdd = new jdd.bdd.BDD(nodenum, cachesize); - vars = new int[256]; - jdd.util.Options.verbose = true; + public String getVersion() { + return "JDDFactory "+REVISION.substring(11, REVISION.length()-2); } - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#init(int, int) - */ - public static BDDFactory init(int nodenum, int cachesize) { - BDDFactory f = new JDDFactory(nodenum, cachesize); - return f; + static final int INVALID_BDD = -1; + + // Redirection functions. + + protected void addref_impl(int v) { bdd.ref(v); } + protected void delref_impl(int v) { bdd.deref(v); } + protected int zero_impl() { return bdd.getZero(); } + protected int one_impl() { return bdd.getOne(); } + protected int invalid_bdd_impl() { return INVALID_BDD; } + protected int var_impl(int index) { + int v = level_impl(index); + return level2var != null ? level2var[v] : v; } - - /** - * Wrapper for the BDD index number used internally in the representation. - */ - private class bdd extends BDD { - int _index; - - static final int INVALID_BDD = -1; - - bdd(int index) { - this._index = index; - bdd.ref(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#getFactory() - */ - public BDDFactory getFactory() { - return JDDFactory.this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isZero() - */ - public boolean isZero() { - return _index == bdd.getZero(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isOne() - */ - public boolean isOne() { - return _index == bdd.getOne(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#var() - */ - public int var() { - int v = bdd.getVar(_index); - return level2var != null ? level2var[v] : v; - } - - public int level() { - int v = bdd.getVar(_index); - return v; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#high() - */ - public BDD high() { - return new bdd(bdd.getHigh(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#low() - */ - public BDD low() { - return new bdd(bdd.getLow(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#id() - */ - public BDD id() { - return new bdd(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#not() - */ - public BDD not() { - return new bdd(bdd.not(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD) - */ - public BDD ite(BDD thenBDD, BDD elseBDD) { - int x = _index; - int y = ((bdd) thenBDD)._index; - int z = ((bdd) elseBDD)._index; - return new bdd(bdd.ite(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) - */ - public BDD relprod(BDD that, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.relProd(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int) - */ - public BDD compose(BDD g, int var) { - int x = _index; - int y = ((bdd) g)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing) - */ - public BDD veccompose(BDDPairing pair) { - int x = _index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD) - */ - public BDD constrain(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) - */ - public BDD exist(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.exists(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) - */ - public BDD forAll(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.forall(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) - */ - public BDD unique(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD) - */ - public BDD restrict(BDD var) { - int x = _index; - int y = ((bdd) var)._index; - return new bdd(bdd.restrict(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD) - */ - public BDD restrictWith(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - int a = bdd.restrict(x, y); - //System.out.println("restrictWith("+System.identityHashCode(this)+") "+x+" -> "+a); - bdd.deref(x); - if (this != that) - that.free(); - bdd.deref(a); - this._index = a; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) - */ - public BDD simplify(BDDVarSet d) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; - return new bdd(bdd.simplify(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#support() - */ - public BDDVarSet support() { - int x = _index; - return new BDDVarSet.DefaultImpl(new bdd(bdd.support(x))); - } - - private int apply0(int x, int y, int z) { - int r; - switch (z) { - case 0: r = bdd.and(x, y); break; - case 1: r = bdd.xor(x, y); break; - case 2: r = bdd.or(x, y); break; - case 3: r = bdd.nand(x, y); break; - case 4: r = bdd.nor(x, y); break; - case 5: r = bdd.imp(x, y); break; - case 6: r = bdd.biimp(x, y); break; - case 7: r = bdd.and(x, bdd.not(y)); break; // diff - default: - throw new BDDException(); // TODO. - } - return r; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD apply(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - return new bdd(apply0(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD applyWith(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = apply0(x, y, z); - bdd.deref(x); - if (this != that) - that.free(); - bdd.ref(a); - this._index = a; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - // todo: combine. - int r = apply0(x, y, z); - bdd.ref(r); - int r2 = bdd.forall(r, a); - bdd.deref(r); - return new bdd(r2); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - // todo: combine. - int r = apply0(x, y, z); - bdd.ref(r); - int r2 = bdd.exists(r, a); - bdd.deref(r); - return new bdd(r2); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - throw new BDDException(); // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne() - */ - public BDD satOne() { - int x = _index; - return new bdd(bdd.oneSat(x)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) - */ - public BDD replace(BDDPairing pair) { - int x = _index; - return new bdd(bdd.replace(x, ((bddPairing) pair).pairing)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing) - */ - public BDD replaceWith(BDDPairing pair) { - int x = _index; - int y = bdd.replace(x, ((bddPairing) pair).pairing); - //System.out.println("replaceWith("+System.identityHashCode(this)+") "+x+" -> "+y); - bdd.deref(x); - bdd.ref(y); - _index = y; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#nodeCount() - */ - public int nodeCount() { - return bdd.nodeCount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount() - */ - public double satCount() { - return bdd.satCount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD) - */ - public boolean equals(BDD that) { - return this._index == ((bdd) that)._index; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#hashCode() - */ - public int hashCode() { - return _index; - } - - static final boolean USE_FINALIZER = false; - - /** - * @see java.lang.Object#finalize() - */ - /* - protected void finalize() throws Throwable { - super.finalize(); - if (USE_FINALIZER) { - if (false && _index >= 0) { - System.out.println("BDD not freed! "+System.identityHashCode(this)); - } - this.free(); - } - } - */ - - /** - * @see net.sf.javabdd.BDD#free() - */ - public void free() { - bdd.deref(_index); - _index = INVALID_BDD; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#fullSatOne() - */ - public BDD fullSatOne() { + protected int level_impl(int index) { + // NOTE: jdd seems to returns the total number of variables when + // calling getVar() on a terminal. + int v = bdd.getVar(index); + if (index == bdd.getOne() || index == bdd.getZero()) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) - */ - public BDD satOne(BDDVarSet var, boolean pol) { - // TODO Implement this. - throw new UnsupportedOperationException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#pathCount() - */ - public double pathCount() { + if (v == -1) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#varProfile() - */ - public int[] varProfile() { + return v; + } + protected int low_impl(int v) { + if (v == bdd.getOne() || v == bdd.getZero()) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#toVarSet() - */ - public BDDVarSet toVarSet() { - return new BDDVarSet.DefaultImpl(new bdd(_index)); - } - + return bdd.getLow(v); } - - private class bddPairing extends BDDPairing { - - private int[] from; - private int[] to; - private jdd.bdd.Permutation pairing; - - private bddPairing() { - reset(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#set(int, int) - */ - public void set(int oldvar, int newvar) { - for (int i = 0; i < from.length; ++i) { - if (from[i] == vars[oldvar]) { - to[i] = vars[newvar]; - pairing = bdd.createPermutation(from, to); - return; - } - } - int[] oldfrom = from; - from = new int[from.length + 1]; - System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); - from[oldfrom.length] = vars[oldvar]; - int[] oldto = to; - to = new int[to.length + 1]; - System.arraycopy(oldto, 0, to, 0, oldto.length); - to[oldto.length] = vars[newvar]; - pairing = bdd.createPermutation(from, to); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) - */ - public void set(int oldvar, BDD newvar) { + protected int high_impl(int v) { + if (v == bdd.getOne() || v == bdd.getZero()) throw new BDDException(); + return bdd.getHigh(v); + } + protected int ithVar_impl(int var) { + if (var >= bdd.numberOfVariables()) + throw new BDDException(); + return vars[var]; + } + protected int nithVar_impl(int var) { + if (var >= bdd.numberOfVariables()) + throw new BDDException(); + return bdd.not(vars[var]); + } + protected int ite_impl(int v1, int v2, int v3) { return bdd.ite(v1, v2, v3); } + protected int apply_impl(int x, int y, BDDOp opr) { + int r; + switch (opr.id) { + case 0: r = bdd.and(x, y); break; + case 1: r = bdd.xor(x, y); break; + case 2: r = bdd.or(x, y); break; + case 3: r = bdd.nand(x, y); break; + case 4: r = bdd.nor(x, y); break; + case 5: r = bdd.imp(x, y); break; + case 6: r = bdd.biimp(x, y); break; + case 7: r = bdd.and(x, bdd.not(y)); break; // diff + default: + throw new UnsupportedOperationException(); // TODO. } - - public void set(int[] oldvar, int[] newvar) { - int[] oldfrom = from; - from = new int[from.length + oldvar.length]; - System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); - for (int i = 0; i < oldvar.length; ++i) { - from[i + oldfrom.length] = vars[oldvar[i]]; - } - int[] oldto = to; - to = new int[to.length + newvar.length]; - System.arraycopy(oldto, 0, to, 0, oldto.length); - for (int i = 0; i < newvar.length; ++i) { - to[i + oldto.length] = vars[newvar[i]]; - } - //debug(); - pairing = bdd.createPermutation(from, to); + return r; + } + protected int not_impl(int v1) { return bdd.not(v1); } + protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { + // todo: combine. + int r = apply_impl(v1, v2, opr); + bdd.ref(r); + int r2 = bdd.forall(r, v3); + bdd.deref(r); + return r2; + } + protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { + if (opr == and) + return bdd.relProd(v1, v2, v3); + // todo: combine. + int r = apply_impl(v1, v2, opr); + bdd.ref(r); + int r2 = bdd.exists(r, v3); + bdd.deref(r); + return r2; + } + protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { + throw new UnsupportedOperationException(); // todo. + } + protected int compose_impl(int v1, int v2, int var) { + throw new UnsupportedOperationException(); // todo. + } + protected int constrain_impl(int v1, int v2) { + throw new UnsupportedOperationException(); // todo. + } + protected int restrict_impl(int v1, int v2) { return bdd.restrict(v1, v2); } + protected int simplify_impl(int v1, int v2) { return bdd.simplify(v1, v2); } + protected int support_impl(int v) { return bdd.support(v); } + protected int exist_impl(int v1, int v2) { return bdd.exists(v1, v2); } + protected int forAll_impl(int v1, int v2) { return bdd.forall(v1, v2); } + protected int unique_impl(int v1, int v2) { + throw new UnsupportedOperationException(); // todo. + } + protected int fullSatOne_impl(int v) { + if (v == bdd.getZero()) + return v; + int[] res = bdd.oneSat(v, null); + int result = bdd.getOne(); + for (int i = res.length - 1; i >= 0; --i) { + int u; + if (res[i] == 1) + u = bdd.mk(i, 0, result); + else + u = bdd.mk(i, result, 0); + bdd.ref(u); bdd.deref(result); + result = u; } - - void debug() { - for (int i = 0; i < from.length; ++i) { - System.out.println(bdd.getVar(from[i])+" -> "+bdd.getVar(to[i])); + bdd.deref(result); + return result; + } + + protected int replace_impl(int v, BDDPairing p) { return bdd.replace(v, ((bddPairing) p).pairing); } + protected int veccompose_impl(int v, BDDPairing p) { + throw new UnsupportedOperationException(); // todo. + } + + protected int nodeCount_impl(int v) { return bdd.nodeCount(v); } + protected double pathCount_impl(int v) { + throw new UnsupportedOperationException(); // todo. + } + protected double satCount_impl(int v) { return bdd.satCount(v); } + protected int satOne_impl(int v) { return bdd.oneSat(v); } + protected int satOne_impl2(int v1, int v2, boolean pol) { + if (v1 == bdd.getZero()) + return v1; + int[] res = bdd.oneSat(v1, null); + int result = bdd.getOne(); + for (int i = res.length - 1; i >= 0; --i) { + while (bdd.getVar(v2) < i) + v2 = bdd.getHigh(v2); + boolean p; + if (res[i] == 1) p = true; + else if (res[i] == 0) p = false; + else { + if (bdd.getVar(v2) != i) + continue; + p = pol; } + int u = bdd.mk(i, p?0:result, p?result:0); + bdd.ref(u); bdd.deref(result); + result = u; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#reset() - */ - public void reset() { - from = to = new int[] { }; - pairing = null; - } - + bdd.deref(result); + return result; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#zero() - */ - public BDD zero() { - return new bdd(bdd.getZero()); + protected int nodeCount_impl2(int[] v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#one() - */ - public BDD one() { - return new bdd(bdd.getOne()); + protected int[] varProfile_impl(int v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#initialize(int, int) - */ - protected void initialize(int nodenum, int cachesize) { - throw new BDDException(); + protected void printTable_impl(int v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#isInitialized() - */ - public boolean isInitialized() { - // TODO Auto-generated method stub - return true; + + // More redirection functions. + + protected void initialize(int initnodesize, int cs) { + bdd = new jdd.bdd.BDD(initnodesize, cs); + vars = new int[256]; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#done() - */ - public void done() { - bdd.cleanup(); + public void addVarBlock(int first, int last, boolean fixed) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setError(int) - */ + public void varBlockAll() { + throw new UnsupportedOperationException(); + } + public void clearVarBlocks() { + throw new UnsupportedOperationException(); + } + public void printOrder() { + throw new UnsupportedOperationException(); + } + public int getNodeTableSize() { + // todo. + return bdd.countRootNodes(); + } + public int setNodeTableSize(int x) { + // TODO. + return getNodeTableSize(); + } + public int setCacheSize(int x) { + // TODO. + return 0; + } + public boolean isInitialized() { return true; } + public void done() { bdd.cleanup(); bdd = null; } public void setError(int code) { - // TODO Implement this. + // todo: implement this } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#clearError() - */ public void clearError() { - // TODO Implement this. + // todo: implement this } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int) - */ public int setMaxNodeNum(int size) { - // TODO Auto-generated method stub - //throw new BDDException(); + // todo: implement this return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double) - */ public double setMinFreeNodes(double x) { int old = jdd.util.Configuration.minFreeNodesProcent; jdd.util.Configuration.minFreeNodesProcent = (int)(x * 100); return (double) old / 100.; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double) - */ - public double setIncreaseFactor(double x) { - // TODO. - return 0.; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMaxIncrease(int) - */ public int setMaxIncrease(int x) { int old = jdd.util.Configuration.maxNodeIncrease; jdd.util.Configuration.maxNodeIncrease = x; return old; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setNodeTableSize(int) - */ - public int setNodeTableSize(int x) { - // TODO. - return getNodeTableSize(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setCacheSize(int) - */ - public int setCacheSize(int x) { - // TODO. + public double setIncreaseFactor(double x) { + // todo: implement this return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getCacheSize() - */ + public int getNodeNum() { + // todo. + return bdd.countRootNodes(); + } public int getCacheSize() { // TODO Implement this. + return 0; + } + public int reorderGain() { throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setCacheRatio(int) - */ + public void printStat() { + bdd.showStats(); + } public double setCacheRatio(double x) { - // TODO Auto-generated method stub + // TODO Implement this. return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#varNum() - */ public int varNum() { return bdd.numberOfVariables(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setVarNum(int) - */ public int setVarNum(int num) { if (num > Integer.MAX_VALUE / 2) throw new BDDException(); @@ -664,128 +289,13 @@ } return old; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#duplicateVar(int) - */ - public int duplicateVar(int var) { - // TODO Implement this. + public void printAll() { throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#ithVar(int) - */ - public BDD ithVar(int var) { - if (var >= bdd.numberOfVariables()) - throw new BDDException(); - //int v = var2level != null ? var2level[var] : var; - int v = var; - return new bdd(vars[v]); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nithVar(int) - */ - public BDD nithVar(int var) { - if (var >= bdd.numberOfVariables()) - throw new BDDException(); - //int v = var2level != null ? var2level[var] : var; - int v = var; - return new bdd(bdd.not(vars[v])); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printAll() - */ - public void printAll() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD) - */ - public void printTable(BDD b) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#level2Var(int) - */ - public int level2Var(int level) { - return level2var != null ? level2var[level] : level; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#var2Level(int) - */ - public int var2Level(int var) { - return var2level != null ? var2level[var] : var; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void reorder(ReorderMethod m) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void autoReorder(ReorderMethod method) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int) - */ - public void autoReorder(ReorderMethod method, int max) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getReorderMethod() - */ - public ReorderMethod getReorderMethod() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getReorderTimes() - */ - public int getReorderTimes() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#disableReorder() - */ - public void disableReorder() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#enableReorder() - */ - public void enableReorder() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderVerbose(int) - */ - public int reorderVerbose(int v) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setVarOrder(int[]) - */ public void setVarOrder(int[] neworder) { - // todo: setting var order corrupts all existing BDD's! + // todo: setting var order corrupts all existing BDDs! if (var2level != null) - throw new BDDException(); + throw new UnsupportedOperationException(); if (bdd.numberOfVariables() != neworder.length) throw new BDDException(); @@ -809,139 +319,149 @@ //System.out.println("Set for domain "+d+": "+d.var.toStringWithDomains()); } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean) - */ - public void addVarBlock(BDD var, boolean fixed) { - throw new BDDException(); + public int level2Var(int level) { return level2var != null ? level2var[level] : level; } + public int var2Level(int var) { return var2level != null ? var2level[var] : var; } + public ReorderMethod getReorderMethod() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean) - */ - public void addVarBlock(int first, int last, boolean fixed) { - throw new BDDException(); + public int getReorderTimes() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#varBlockAll() - */ - public void varBlockAll() { - throw new BDDException(); + public void disableReorder() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#clearVarBlocks() - */ - public void clearVarBlocks() { - throw new BDDException(); + public void enableReorder() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printOrder() - */ - public void printOrder() { - throw new BDDException(); + public int reorderVerbose(int v) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection) - */ - public int nodeCount(Collection r) { - throw new BDDException(); + public void reorder(ReorderMethod m) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeTableSize() - */ - public int getNodeTableSize() { - // todo. - return bdd.countRootNodes(); + public void autoReorder(ReorderMethod method) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeNum() - */ - public int getNodeNum() { - // todo. - return bdd.countRootNodes(); + public void autoReorder(ReorderMethod method, int max) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderGain() - */ - public int reorderGain() { - throw new BDDException(); + public void swapVar(int v1, int v2) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printStat() - */ - public void printStat() { - bdd.showStats(); + + private jdd.bdd.BDD bdd; + private int[] vars; // indexed by EXTERNAL + private int[] level2var; // internal -> external + private int[] var2level; // external -> internal + + static { + jdd.util.Options.verbose = true; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#makePair() - */ - public BDDPairing makePair() { - return new bddPairing(); + + private JDDFactory(int nodenum, int cachesize) { + initialize(nodenum, cachesize); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#swapVar(int, int) + * @see net.sf.javabdd.BDDFactory#init(int, int) */ - public void swapVar(int v1, int v2) { - throw new BDDException(); + public static BDDFactory init(int nodenum, int cachesize) { + BDDFactory f = new JDDFactory(nodenum, cachesize); + return f; } - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger) - */ - protected BDDDomain createDomain(int a, BigInteger b) { - return new bddDomain(a, b); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createBitVector(int) - */ - protected BDDBitVector createBitVector(int a) { - return new bddBitVector(a); - } - - private class bddDomain extends BDDDomain { - - private bddDomain(int a, BigInteger b) { - super(a, b); + private class bddPairing extends BDDPairing { + + private int[] from; + private int[] to; + private jdd.bdd.Permutation pairing; + + private bddPairing() { + reset(); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDBitVector#getFactory() + * @see net.sf.javabdd.BDDPairing#set(int, int) */ - public BDDFactory getFactory() { return JDDFactory.this; } - - } - - private class bddBitVector extends BDDBitVector { - - private bddBitVector(int a) { - super(a); + public void set(int oldvar, int newvar) { + for (int i = 0; i < from.length; ++i) { + if (from[i] == vars[oldvar]) { + to[i] = vars[newvar]; + pairing = bdd.createPermutation(from, to); + return; + } + } + int[] oldfrom = from; + from = new int[from.length + 1]; + System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); + from[oldfrom.length] = vars[oldvar]; + int[] oldto = to; + to = new int[to.length + 1]; + System.arraycopy(oldto, 0, to, 0, oldto.length); + to[oldto.length] = vars[newvar]; + pairing = bdd.createPermutation(from, to); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDBitVector#getFactory() + * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) */ - public BDDFactory getFactory() { return JDDFactory.this; } - + public void set(int oldvar, BDD newvar) { + throw new UnsupportedOperationException(); + } + + public void set(int[] oldvar, int[] newvar) { + int[] oldfrom = from; + from = new int[from.length + oldvar.length]; + System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); + for (int i = 0; i < oldvar.length; ++i) { + from[i + oldfrom.length] = vars[oldvar[i]]; + } + int[] oldto = to; + to = new int[to.length + newvar.length]; + System.arraycopy(oldto, 0, to, 0, oldto.length); + for (int i = 0; i < newvar.length; ++i) { + to[i + oldto.length] = vars[newvar[i]]; + } + //debug(); + pairing = bdd.createPermutation(from, to); + } + + void debug() { + for (int i = 0; i < from.length; ++i) { + System.out.println(bdd.getVar(from[i])+" -> "+bdd.getVar(to[i])); + } + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDPairing#reset() + */ + public void reset() { + from = to = new int[] { }; + pairing = null; + } + } - public static final String REVISION = "$Revision$"; - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getVersion() - */ - public String getVersion() { - return "JDD "+REVISION.substring(11, REVISION.length()-2); + public BDDPairing makePair() { + return new bddPairing(); } + + public void registerGCCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterGCCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void registerReorderCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterReorderCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void registerResizeCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterResizeCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } } Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-21 14:32:02 UTC (rev 461) @@ -28,8 +28,16 @@ */ public class JFactory extends BDDFactoryIntImpl { - static final boolean VERIFY_ASSERTIONS = false; + /**** Options ****/ + + /** + * Flush the operation cache on every garbage collection. If this is false, + * we only clean the collected entries on every GC, rather than emptying the + * whole cache. For most problems, you should keep this set to true. + */ public static boolean FLUSH_CACHE_ON_GC = true; + + static final boolean VERIFY_ASSERTIONS = false; static final boolean CACHESTATS = false; static final boolean SWAPCOUNT = false; @@ -47,11 +55,20 @@ public static BDDFactory init(int nodenum, int cachesize) { BDDFactory f = new JFactory(); f.initialize(nodenum, cachesize); + if (CACHESTATS) addShutdownHook(f); return f; } - public boolean ZDD = false; + static void addShutdownHook(final BDDFactory f) { + Runtime.getRuntime().addShutdownHook(new Thread() { + public void run() { + System.out.println(f.getCacheStats().toString()); + } + }); + } + boolean ZDD = false; + /** * Implementation of BDDPairing used by JFactory. */ @@ -122,7 +139,7 @@ protected void addref_impl(int v) { bdd_addref(v); } protected void delref_impl(int v) { bdd_delref(v); } protected int zero_impl() { return BDDZERO; } - protected int one_impl() {return BDDONE; } + protected int one_impl() { return BDDONE; } protected int invalid_bdd_impl() { return INVALID_BDD; } protected int var_impl(int v) { return bdd_var(v); } protected int level_impl(int v) { return LEVEL(v); } @@ -917,25 +934,20 @@ int bdd_not(int r) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(r, bddfalse); if (applycache == null) applycache = BddCacheI_init(cachesize); again : for (;;) { try { INITREF(); - - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = ZDD ? znot_rec(r) : not_rec(r); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = bddfalse; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -948,10 +960,8 @@ BddCacheDataI entry; int res; - if (ISZERO(r)) - return bddtrue; - if (ISONE(r)) - return bddfalse; + if (ISCONST(r)) + return 1 - r; entry = BddCache_lookupI(applycache, NOTHASH(r)); @@ -1007,7 +1017,7 @@ int bdd_ite(int f, int g, int h) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(g, bddfalse); @@ -1020,18 +1030,13 @@ try { INITREF(); - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = ZDD ? zite_rec(f, g, h) : ite_rec(f, g, h); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -1201,7 +1206,7 @@ int bdd_replace(int r, bddPair pair) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(r, bddfalse); @@ -1214,18 +1219,13 @@ replacelast = pair.last; replaceid = (pair.id << 2) | CACHEID_REPLACE; - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = replace_rec(r); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -1298,7 +1298,7 @@ int bdd_apply(int l, int r, int op) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(l, bddfalse); CHECKa(r, bddfalse); @@ -1315,29 +1315,22 @@ INITREF(); applyop = op; - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); switch (op) { case bddop_and: res = ZDD ? zand_rec(l, r) : and_rec(l, r); break; case bddop_or: res = ZDD ? zor_rec(l, r) : or_rec(l, r); break; case bddop_diff: res = ZDD ? zdiff_rec(l, r) : apply_rec(l, r); break; default: res = apply_rec(l, r); break; } - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } - //validate(res); - checkresize(); return res; } @@ -1705,7 +1698,7 @@ int bdd_appex(int l, int r, int opr, int var) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(l, bddfalse); CHECKa(r, bddfalse); @@ -1734,18 +1727,16 @@ appexid = (var << 5) | (appexop << 1); /* FIXME: range! */ quantid = (appexid << 3) | CACHEID_APPEX; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = opr == bddop_and ? relprod_rec(l, r) : appquant_rec(l, r); - if (firstReorder == 0) + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -2073,7 +2064,7 @@ int bdd_constrain(int f, int c) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(c, bddfalse); @@ -2085,18 +2076,16 @@ INITREF(); miscid = CACHEID_CONSTRAIN; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = constrain_rec(f, c); - if (firstReorder == 0) + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -2166,7 +2155,7 @@ int bdd_compose(int f, int g, int var) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(g, bddfalse); @@ -2184,18 +2173,16 @@ composelevel = bddvar2level[var]; replaceid = (composelevel << 2) | CACHEID_COMPOSE; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = compose_rec(f, g); - if (fir... [truncated message content] |
