--- a/src/lite/ExistsSolver.java	Wed Jan 09 16:42:51 2008 +0900
+++ b/src/lite/ExistsSolver.java	Wed Jan 09 19:57:56 2008 +0900
@@ -11,13 +11,13 @@
 
 	ITLSolver node;
 	VariableSolver var;
-	LinkedList<ITLSolver> oldVarList;
+	LinkedList<Boolean> oldVarList;
 	ITLSolver residue;
 
 	public ExistsSolver(VariableSolver var, ITLSolver node) {
 		this.node = node;
 		this.var = var;
-		oldVarList = new LinkedList<ITLSolver>();
+		oldVarList = new LinkedList<Boolean>();
 	}
 	
 	
@@ -29,23 +29,39 @@
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		makeLocal(sat);
 		var.setValue(true);
-		return node.sat(sat, new Continuation(sat,next,this));
+		try {
+			return node.sat(sat, new Continuation(sat,next,this));
+		} catch (Backtrack e) {
+			restoreLocal(sat);
+			throw sat.backtrack;
+		}
+	}
+
+
+	private void restoreLocal(ITLSatisfier sat) {
+		if (oldVarList.size()>0) {
+			var.value = oldVarList.getLast();
+			oldVarList.removeLast();
+		} else {
+			sat.deleteChoicePoint(var);
+		}
 	}
 
 	private void makeLocal(ITLSatisfier sat) {
 		if (sat.hasChoicePoint(var)) {
-			oldVarList.add(sat.lf.variableNode(var.toString(), var.value));
+			oldVarList.add(var.value);
 		} else {
 			sat.addChoicePoint(var);
 		}
 	}
 
-	private void restoreLocal(ITLSatisfier sat) {
-		if (oldVarList.size()>0) {
-			var.value = oldVarList.getLast().value;
-			oldVarList.removeLast();
-		} else {
-			sat.deleteChoicePoint(var);
+	private ITLSolver restoreLocal(ITLSatisfier sat,ITLSolver value,Continuation next) throws Backtrack {
+		restoreLocal(sat);
+		try {
+			return next.sat(value);
+		} catch (Backtrack e) {
+			makeLocal(sat);
+			throw sat.backtrack;
 		}
 	}
 	
@@ -55,8 +71,7 @@
 			var.setValue(false);
 			return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
 		} else if (value==sat.true_) {
-			restoreLocal(sat);
-			return next.sat(sat.true_);
+			return restoreLocal(sat,value,next);
 		} else {
 			var.setValue(false);
 			residue = value;
@@ -67,22 +82,19 @@
 
 	class ExistsSolver2 implements Next {
 		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
-			restoreLocal(sat);
 			if (value==null) {
-				return next.sat(residue);
+				value = residue;
 			} else if (value==sat.true_) {
-				return next.sat(sat.true_);
 			} else {
-				return next.sat(sat.lf.existsNode(var,
-						sat.lf.orNode(residue,value)));
+				value = sat.lf.existsNode(var,sat.lf.orNode(residue,value));
 			}
+			return restoreLocal(sat,value,next);
 		}
 	}
 	class ExistsSolver3 implements Next {
 
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			restoreLocal(sat);
-			return next.sat(value);
+			return restoreLocal(sat,value,next);
 		}
 	}
 	

--- a/src/lite/VariableSolver.java	Wed Jan 09 16:42:51 2008 +0900
+++ b/src/lite/VariableSolver.java	Wed Jan 09 19:57:56 2008 +0900
@@ -47,7 +47,7 @@
 	
 
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
-		return sf.variableNode(name, value).toSBDD(sf);
+		return sf.bddNode(this, sf.trueNode(), sf.falseNode()).toSBDD(sf);
 	}
 	
 	public int hashCode() {
@@ -55,6 +55,10 @@
 		return hash = name.hashCode();
 	}
 	
+	@Override
+	public void setValue(boolean value) {
+		this.value = value;
+	}
 
 	public boolean equals(Object o) {
 		if (o.hashCode()!=hashCode()) return false;

--- a/src/sbdd/SBDDTest.java	Wed Jan 09 16:42:51 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Wed Jan 09 19:57:56 2008 +0900
@@ -62,12 +62,13 @@
 		sat.showVerify("fin(p)=([](<>(p)))");
 		sat.showVerify("fin(p)");
 		}
-		sat.showVerify("even(p)");
+		sat.showVerify("exists(x,@@x = ~x)");
+		//sat.showVerify("even(p)");
 		//sat.showVerify("evenp(p)");
 		//at.showVerify("keep(@q = ~q)");
 		//sat.showVerify("keep(q)");
 		//sat.showVerify("even(p)<->evenp(p)");
-		// System.out.println(sat.state);
+		System.out.println(sat.state);
 		// sat.p.parse("include('data/example').");
 		// System.out.println(p.parseCommand.sat.state);
 	}