Mercurial > hg > Applications > JavaLite

changeset 89:aed27c25859e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Fri, 18 Jan 2008 16:50:12 +0900
parents 6b3535ea6958
children 8affa0aa0fc0
files src/lite/BDDSolver.java src/lite/ITLNodeFactory.java src/lite/ITLSatisfier.java src/sbdd/SBDDFactory.java src/sbdd/SBDDFactoryInterface.java
diffstat 5 files changed, 48 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/BDDSolver.java	Fri Jan 18 16:00:37 2008 +0900
+++ b/src/lite/BDDSolver.java	Fri Jan 18 16:50:12 2008 +0900
@@ -21,20 +21,13 @@
 		id = BDDID.Variable;
 	}
 
-	public BDDSolver(ITLSolver var, ITLSolver high, ITLSolver low) {
-		this.var = var;
-		this.high = (BDDSolver) high;
-		this.low  = (BDDSolver) low;
-		id = BDDID.Variable;
-	}
-
 	public BDDSolver(BDDID id, int hash) {
 		// primitives
 		this.id = id;
 		this.hash = hash;
 	}
 
-	public BDDSolver(ITLSolver v, ITLSolver high, ITLSolver low, BDDID id) {
+	public BDDSolver(ITLSolver v, BDDSolver high, BDDSolver low, BDDID id) {
 		// for modal node with id
 		this(v,high,low);
 		this.id = id;
@@ -130,7 +123,7 @@
 	}
 
 
-	public ITLSolver and(SBDDFactoryInterface sf,BDDSolver right) {
+	public BDDSolver and(SBDDFactoryInterface sf,BDDSolver right) {
 		switch(id) {
 		case True: return right;
 		case False: return sf.falseNode();
@@ -145,7 +138,7 @@
 			return sf.bddNode(var,high.and(sf,right),low.and(sf,right));
 	}
 
-	public ITLSolver or(SBDDFactoryInterface sf,BDDSolver right) {
+	public BDDSolver or(SBDDFactoryInterface sf,BDDSolver right) {
 		switch(id) {
 		case True: return sf.trueNode();
 		case False: return right;
@@ -160,7 +153,7 @@
 	}
 
 
-	public ITLSolver not(SBDDFactoryInterface sf) {
+	public BDDSolver not(SBDDFactoryInterface sf) {
 		switch(id) {
 		case True: return sf.falseNode();
 		case False: return sf.trueNode();
--- a/src/lite/ITLNodeFactory.java	Fri Jan 18 16:00:37 2008 +0900
+++ b/src/lite/ITLNodeFactory.java	Fri Jan 18 16:50:12 2008 +0900
@@ -4,13 +4,10 @@
 
 import parser.Command;
 import parser.MacroNodeParserInterface;
-import sbdd.SBDDFactoryInterface;
 import sbdd.SBDDSet;
 
-
-
-public class ITLNodeFactory implements	ITLNodeFactoryInterface<ITLSolver>,
-											SBDDFactoryInterface {
+public class ITLNodeFactory implements	ITLNodeFactoryInterface<ITLSolver> {
+											// SBDDFactoryInterface {
 
 	public static final ITLSolver trueSolver = new TrueSolver();
 	public static final ITLSolver falseSolver = new FalseSolver();	
@@ -94,7 +91,10 @@
 	}
 
 	public ITLSolver bddNode(ITLSolver cond, ITLSolver high, ITLSolver low) {
-		return new BDDSolver((VariableSolver)cond,high,low);
+		return orNode(
+				andNode(cond, high),
+				andNode(notNode(cond), low));
+		// return new BDDSolver((VariableSolver)cond,high,low);
 	}
 
 	public SBDDSet set() {
--- a/src/lite/ITLSatisfier.java	Fri Jan 18 16:00:37 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Fri Jan 18 16:50:12 2008 +0900
@@ -1,6 +1,7 @@
 package lite;
 
 
+import sbdd.SBDDFactory;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 import verifier.ChoicePointList;
@@ -29,7 +30,8 @@
 	
 	public ITLSatisfier(ITLSolver p) {
 		this();
-		lf = new ITLNodeFactory();
+		// lf = new ITLNodeFactory();
+		lf = new SBDDFactory();
 		this.empty = p; // have to be the same in the parser
 	}
 
--- a/src/sbdd/SBDDFactory.java	Fri Jan 18 16:00:37 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Fri Jan 18 16:50:12 2008 +0900
@@ -10,13 +10,13 @@
 
 public class SBDDFactory implements SBDDFactoryInterface {
 
-	public static final ITLSolver trueSolver   = new BDDSolver(ITLNodeFactory.trueSolver,BDDID.True,TokenID.True.hash);
-	public static final ITLSolver falseSolver  = new BDDSolver(ITLNodeFactory.falseSolver,BDDID.False,TokenID.False.hash);
-	public static final ITLSolver emptySolver  = new BDDSolver(ITLNodeFactory.emptySolver,trueSolver,falseSolver,BDDID.BDD);
+	public static final BDDSolver trueSolver   = new BDDSolver(ITLNodeFactory.trueSolver,BDDID.True,TokenID.True.hash);
+	public static final BDDSolver falseSolver  = new BDDSolver(ITLNodeFactory.falseSolver,BDDID.False,TokenID.False.hash);
+	public static final BDDSolver emptySolver  = new BDDSolver(ITLNodeFactory.emptySolver,trueSolver,falseSolver,BDDID.BDD);
 	public SBDDSet hash;
 	ITLNodeFactory itlf;
 	
-	SBDDFactory() {
+	public SBDDFactory() {
 		init();
 	}
 	
@@ -30,59 +30,59 @@
 	}
 	
 
-	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) {
+	public BDDSolver bddNode(ITLSolver lvar, BDDSolver solver, BDDSolver solver2) {
 		if (solver==solver2) return solver;
 		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
 		return hash.put(v); 
 	}
 
-	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2) {
-		BDDSolver former = solver.toSBDD(this);
+	public BDDSolver chopNode(ITLSolver solver, ITLSolver solver2) {
+		BDDSolver former = solver.toSBDD(this); // unnecesarry?
 		BDDSolver later = solver2.toSBDD(this);
 		if (former==emptySolver) return hash.put(later); 
 		if (later==emptySolver) return hash.put(former); 
-		ITLSolver v =  itlf.chopNode(solver.toSBDD(this),solver2.toSBDD(this));
+		ITLSolver v =  itlf.chopNode(former,later);
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Chop);
 		return hash.put(b);
 	}
 
-	public ITLSolver emptyNode() {
+	public BDDSolver emptyNode() {
 		return emptySolver;
 	}
 
-	public ITLSolver existsNode(ITLSolver solver, ITLSolver solver2) {
-		ITLSolver v =  itlf.existsNode(solver,solver2);
+	public BDDSolver existsNode(ITLSolver solver, ITLSolver solver2) {
+		ITLSolver v =  itlf.existsNode(solver,solver2.toSBDD(this));
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Exists);
 		return hash.put(b);
 	}
 
-	public ITLSolver falseNode() {
+	public BDDSolver falseNode() {
 		return falseSolver;
 	}
 
-	public ITLSolver nextNode(ITLSolver solver) {
+	public BDDSolver nextNode(ITLSolver solver) {
 		ITLSolver v =  itlf.nextNode(solver);
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Next);
 		return hash.put(b);
 	}
 
-	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
+	public BDDSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
 		ITLSolver v =  itlf.projectionNode(solver,solver2);
 		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Projection);
 		return hash.put(b);
 	}
 
-	public ITLSolver trueNode() {
+	public BDDSolver trueNode() {
 		return trueSolver;
 	}
 
-	public ITLSolver variableNode(String name, boolean value) {
+	public BDDSolver variableNode(String name, boolean value) {
 		ITLSolver v =  new BDDSolver(itlf.variableNode(name, value),trueSolver,falseSolver,BDDID.Variable);
 		return hash.put(v); 
 	}
 
 
-	public ITLSolver andNode(ITLSolver left, ITLSolver right) {
+	public BDDSolver andNode(ITLSolver left, ITLSolver right) {
 
 		BDDSolver lb = left.toSBDD(this);
 		BDDSolver rb = right.toSBDD(this);
@@ -90,28 +90,28 @@
 			return falseSolver;
 		if (lb==trueSolver)
 			return rb;
-		lb =  (BDDSolver) lb.and(this, rb);
+		lb = lb.and(this, rb);
 		return hash.put(lb);
 	}
 
 
-	public ITLSolver notNode(ITLSolver node) {
+	public BDDSolver notNode(ITLSolver node) {
 		BDDSolver nb = node.toSBDD(this);
 		if (nb==falseSolver) return trueSolver;
 		if (nb==trueSolver)	 return falseSolver;
-		nb = (BDDSolver) nb.not(this);
+		nb = nb.not(this);
 		return hash.put(nb);
 	}
 
 
-	public ITLSolver orNode(ITLSolver left, ITLSolver right) {
+	public BDDSolver orNode(ITLSolver left, ITLSolver right) {
 		BDDSolver lb = left.toSBDD(this);
 		BDDSolver rb = right.toSBDD(this);
 		if (lb==trueSolver||rb==trueSolver)
 			return trueSolver;
 		if (lb==falseSolver)
 			return rb;
-		lb = (BDDSolver) lb.or(this, rb);
+		lb = lb.or(this, rb);
 		return hash.put(lb);
 	}
 
--- a/src/sbdd/SBDDFactoryInterface.java	Fri Jan 18 16:00:37 2008 +0900
+++ b/src/sbdd/SBDDFactoryInterface.java	Fri Jan 18 16:50:12 2008 +0900
@@ -1,31 +1,32 @@
 package sbdd;
 
+import lite.BDDSolver;
 import lite.ITLSolver;
 
 
 public interface SBDDFactoryInterface {
 
-	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2);
+	public BDDSolver bddNode(ITLSolver lvar, BDDSolver solver, BDDSolver solver2);
 
-	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2);
+	public BDDSolver chopNode(ITLSolver solver, ITLSolver solver2);
 
-	public ITLSolver emptyNode();
+	public BDDSolver emptyNode();
 
-	public ITLSolver existsNode(ITLSolver solver, ITLSolver solver2);
+	public BDDSolver existsNode(ITLSolver solver, ITLSolver solver2);
 
-	public ITLSolver falseNode();
+	public BDDSolver falseNode();
 
-	public ITLSolver nextNode(ITLSolver solver);
+	public BDDSolver nextNode(ITLSolver solver);
 
-	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2);
+	public BDDSolver projectionNode(ITLSolver solver, ITLSolver solver2);
 
-	public ITLSolver trueNode();
+	public BDDSolver trueNode();
 
-	public ITLSolver variableNode(String name, boolean value);
+	public BDDSolver variableNode(String name, boolean value);
 
-	public ITLSolver andNode(ITLSolver left, ITLSolver right);
-	public ITLSolver orNode(ITLSolver left,ITLSolver right);
-	public ITLSolver notNode(ITLSolver node);
+	public BDDSolver andNode(ITLSolver left, ITLSolver right);
+	public BDDSolver orNode(ITLSolver left,ITLSolver right);
+	public BDDSolver notNode(ITLSolver node);
 
 	public SBDDSet set() ;