# HG changeset patch
# User kono
# Date 1199956560 -32400
# Node ID 80db395eeb30a753085de07e4097e81afca36e14
# Parent  d6a300cdd18e1b465205e26096a02e72d1041c98
*** empty log message ***

diff -r d6a300cdd18e -r 80db395eeb30 Changes
--- a/Changes	Thu Jan 10 02:29:46 2008 +0900
+++ b/Changes	Thu Jan 10 18:16:00 2008 +0900
@@ -1,3 +1,9 @@
+Thu Jan 10 13:28:26 JST 2008
+
+hasChoicePoint は、variable 毎にフラグで持っても良い。
+その方が linear search しなくて良いので少し速い。
+けど、exists との相性は悪い。(かな?)
+
 Wed Jan  9 20:42:17 JST 2008
 
 あぁ、そうか。
diff -r d6a300cdd18e -r 80db395eeb30 src/lite/BDDSolver.java
--- a/src/lite/BDDSolver.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/lite/BDDSolver.java	Thu Jan 10 18:16:00 2008 +0900
@@ -121,9 +121,11 @@
 				if (low==null)  low = sat.lf.falseNode();
 				if (high==null) high = sat.lf.falseNode();
 				// if (cond==null) cond = sat.lf.falseNode();
-				return next.sat(sat.lf.orNode(
+				ITLSolver value = sat.lf.orNode(
 						sat.lf.andNode(cond, high),
-						sat.lf.andNode(sat.lf.notNode(cond), low)));
+						sat.lf.andNode(sat.lf.notNode(cond), low));
+				if (value==sat.false_) value = null;
+				return next.sat(value);
 			}
 		}
 	}
diff -r d6a300cdd18e -r 80db395eeb30 src/lite/ChopSolver.java
--- a/src/lite/ChopSolver.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/lite/ChopSolver.java	Thu Jan 10 18:16:00 2008 +0900
@@ -123,7 +123,9 @@
 				// we don't have to execute later case now, do it on next clock
 				ITLSolver former1 = sat.lf.chopNode(value,later);
 				// return disjunction with other choice
-				return next.sat(sat.lf.orNode(later1,former1));
+				ITLSolver v = sat.lf.orNode(later1,former1);
+				if (v==sat.false_) v = null;
+				return next.sat(v);
 			}
 		}
 	}
diff -r d6a300cdd18e -r 80db395eeb30 src/lite/ExistsSolver.java
--- a/src/lite/ExistsSolver.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/lite/ExistsSolver.java	Thu Jan 10 18:16:00 2008 +0900
@@ -1,7 +1,5 @@
 package lite;
 
-import java.util.LinkedList;
-
 import logicNode.parser.TokenID;
 
 import sbdd.SBDDFactoryInterface;
@@ -11,13 +9,12 @@
 
 	ITLSolver node;
 	VariableSolver var;
-	LinkedList<Boolean> oldVarList;
+	Boolean old;
 	ITLSolver residue;
 
 	public ExistsSolver(VariableSolver var, ITLSolver node) {
 		this.node = node;
 		this.var = var;
-		oldVarList = new LinkedList<Boolean>();
 	}
 	
 	
@@ -27,9 +24,8 @@
 
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
-		boolean old = var.value;
-		makeLocal(sat);
-		var.setValue(true);
+		old = var.value;
+		makeLocal(sat,true);
 		try {
 			return node.sat(sat, new Continuation(sat,next,this));
 		} catch (Backtrack e) {
@@ -41,20 +37,13 @@
 
 
 	private void restoreLocal(ITLSatisfier sat) {
-		if (oldVarList.size()>0) {
-			var.value = oldVarList.getLast();
-			oldVarList.removeLast();
-		} else {
-			sat.deleteChoicePoint(var);
-		}
+		sat.deleteChoicePoint(var);
+		var.setValue(old);
 	}
 
-	private void makeLocal(ITLSatisfier sat) {
-		if (sat.hasChoicePoint(var)) {
-			oldVarList.add(var.value);
-		} else {
-			sat.addChoicePoint(var);
-		}
+	private void makeLocal(ITLSatisfier sat,boolean newv) {
+		sat.addChoicePoint(var);
+		var.setValue(newv);
 	}
 
 	private ITLSolver restoreLocal(ITLSatisfier sat,boolean now,ITLSolver value,Continuation next) throws Backtrack {
@@ -62,8 +51,7 @@
 		try {
 			return next.sat(value);
 		} catch (Backtrack e) {
-			makeLocal(sat);
-			var.setValue(now);
+			makeLocal(sat,now);
 			throw sat.backtrack;
 		}
 	}
@@ -72,14 +60,24 @@
 	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
 		if (value==null) {
 			var.setValue(false);
-			return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
+			try {
+				return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
+			} catch (Backtrack e) {
+				var.setValue(true);
+				throw e;
+			}
 		} else if (value==sat.true_) {
-			return restoreLocal(sat,var.value,value,next);
+			return restoreLocal(sat,true,value,next);
 		} else {
 			var.setValue(false);
 			residue = value;
-			return node.sat(sat, new Continuation(sat,next,
+			try {
+				return node.sat(sat, new Continuation(sat,next,
 					new ExistsSolver2()));
+			} catch (Backtrack e) {
+				var.setValue(true);
+				throw e;
+			}
 		}
 	}
 
@@ -91,23 +89,24 @@
 			} else {
 				value = sat.lf.orNode(residue,value);
 				if (value==sat.true_)  {
+				} else if (value==sat.false_)  {
+					value = null;
 				} else {
 					value = sat.lf.existsNode(var,value);
 				}
 			}
-			return restoreLocal(sat,var.value,value,next);
+			return restoreLocal(sat,false,value,next);
 		}
 	}
 	
 	class ExistsSolver3 implements Next {
-
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			if (value==null) {
 			} else if (value==sat.true_) {
 			} else {
 				value = sat.lf.existsNode(var, value);
 			}
-			return restoreLocal(sat,var.value,value,next);
+			return restoreLocal(sat,false,value,next);
 		}
 	}
 	
diff -r d6a300cdd18e -r 80db395eeb30 src/lite/ITLNodeParser.java
--- a/src/lite/ITLNodeParser.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Thu Jan 10 18:16:00 2008 +0900
@@ -147,6 +147,7 @@
 		Node n;
 		LinkedList<Node> arg = new LinkedList<Node>();
 		while(nextToken.type!=TokenID.CloseParen) {
+			if (nextToken.type==TokenID.NULL) break;
 			n = exprI2();
 			arg.add(n);
 			if (nextToken.type == TokenID.And)
diff -r d6a300cdd18e -r 80db395eeb30 src/lite/ITLSatisfier.java
--- a/src/lite/ITLSatisfier.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/lite/ITLSatisfier.java	Thu Jan 10 18:16:00 2008 +0900
@@ -12,6 +12,7 @@
 	 */
 	private static final long serialVersionUID = 1L;
 	public ITLSolver true_;
+	public ITLSolver false_;
 	public SBDDFactoryInterface lf;
 
 	public Backtrack backtrack;
@@ -20,7 +21,8 @@
 	
 	public ITLSatisfier() {
 		backtrack = new Backtrack();
-		true_  = ITLNodeFactory.trueSolver;
+		true_   = ITLNodeFactory.trueSolver;
+		false_  = ITLNodeFactory.falseSolver;
 	}
 	
 	public ITLSatisfier(ITLSolver p) {
diff -r d6a300cdd18e -r 80db395eeb30 src/sbdd/BDDSatisfier.java
--- a/src/sbdd/BDDSatisfier.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Thu Jan 10 18:16:00 2008 +0900
@@ -41,6 +41,7 @@
 		init();
 		lf = new SBDDFactory();
 		true_ = SBDDFactory.trueSolver;
+		false_ = SBDDFactory.falseSolver;
 		state = sf.set();
 		state.getEntry(SBDDFactory.trueSolver).expanded = true;
 		state.getEntry(SBDDFactory.falseSolver).expanded = true;
@@ -95,7 +96,6 @@
 		queue = new LinkedList<SBDDEntry>();
 		AllNext allNext = new AllNext();
 		SBDDEntry b = state.getEntry(n);
-		this.clear(); // if not empty something wrong
 		if (b.expanded) {
 			// already checked
 			System.out.println("   already checked.");
@@ -107,6 +107,10 @@
 			e.expanded = true;
 			System.out.println(e.key+"->");
 			develop(e.key, allNext);
+			if (this.size()>0) {
+				System.err.println("cb remains "+this);
+				this.clear();
+			}
 		}
 	}
 		
diff -r d6a300cdd18e -r 80db395eeb30 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Thu Jan 10 02:29:46 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Thu Jan 10 18:16:00 2008 +0900
@@ -65,15 +65,13 @@
 		sat.showVerify("exists(x,@@x = ~x)");
 		sat.showVerify("all(x,@@x)");
 		sat.showVerify("even(p)");
-		sat.showVerify("Q, keep( @Q = ~Q),'[]'((Q->P))");
+		sat.showVerify("Q, keep( @Q = ~Q)");
 		}
-		sat.showVerify("Q, keep( @Q = ~Q)");
-		//sat.showVerify("evenp(p)");
-		//at.showVerify("keep(@q = ~q)");
-		//sat.showVerify("keep(q)");
+		sat.showVerify("even(p)");
+		sat.showVerify("evenp(p)");
 		//sat.showVerify("even(p)<->evenp(p)");
 		//System.out.println(sat.state);
-		// sat.p.parse("include('data/example').");
+		//sat.p.parse("include('data/example').");
 		// System.out.println(p.parseCommand.sat.state);
 	}