Mercurial > hg > Applications > JavaLite

changeset 60:ff125345619d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exists does not terminate...
author kono
date Wed, 09 Jan 2008 16:42:51 +0900
parents f97d0d631992
children 51e13324a3f1
files src/lite/BDDSolver.java src/lite/EmptySolver.java src/lite/ExistsSolver.java src/lite/ITLNodeFactory.java src/lite/ITLNodeParser.java src/lite/NextSolver.java src/sbdd/SBDDTest.java
diffstat 7 files changed, 39 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/BDDSolver.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/BDDSolver.java	Wed Jan 09 16:42:51 2008 +0900
@@ -163,7 +163,7 @@
 		case True: return sf.falseNode();
 		case False: return sf.trueNode();
 		}
-		return  sf.bddNode(var,low.toSBDD(sf),high.toSBDD(sf));
+		return  sf.bddNode(var,high.toSBDD(sf).not(sf),low.toSBDD(sf).not(sf));
 	}
 
 	int order(ITLSolver a,ITLSolver b) {
--- a/src/lite/EmptySolver.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/EmptySolver.java	Wed Jan 09 16:42:51 2008 +0900
@@ -31,6 +31,11 @@
 		}
 	}
 
+	@Override
+	public void setValue(boolean solver) {
+		value = solver;
+	}
+	
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
 		return sf.emptyNode().toSBDD(sf);
 	}
--- a/src/lite/ExistsSolver.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/ExistsSolver.java	Wed Jan 09 16:42:51 2008 +0900
@@ -10,11 +10,11 @@
 public class ExistsSolver extends ITLSolver {
 
 	ITLSolver node;
-	ITLSolver var;
+	VariableSolver var;
 	LinkedList<ITLSolver> oldVarList;
 	ITLSolver residue;
 
-	public ExistsSolver(ITLSolver var, ITLSolver node) {
+	public ExistsSolver(VariableSolver var, ITLSolver node) {
 		this.node = node;
 		this.var = var;
 		oldVarList = new LinkedList<ITLSolver>();
@@ -56,7 +56,7 @@
 			return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
 		} else if (value==sat.true_) {
 			restoreLocal(sat);
-			return next.sat(sat.true_());
+			return next.sat(sat.true_);
 		} else {
 			var.setValue(false);
 			residue = value;
@@ -71,7 +71,7 @@
 			if (value==null) {
 				return next.sat(residue);
 			} else if (value==sat.true_) {
-				return next.sat(sat.true_());
+				return next.sat(sat.true_);
 			} else {
 				return next.sat(sat.lf.existsNode(var,
 						sat.lf.orNode(residue,value)));
@@ -85,8 +85,9 @@
 			return next.sat(value);
 		}
 	}
+	
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
-		return sf.existsNode(var.toSBDD(sf), node.toSBDD(sf)).toSBDD(sf);
+		return sf.existsNode(var, node.toSBDD(sf)).toSBDD(sf);
 	}
 
 	
@@ -106,6 +107,7 @@
 		if (o.hashCode()!=hashCode()) return false;
 		if (o.getClass()==this.getClass()) {
 			ExistsSolver v = (ExistsSolver)o;
+			// should ignore local variable name
 			return var.equals(v.var)&& node.equals(v.node);
 		}
 		return false;
--- a/src/lite/ITLNodeFactory.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/ITLNodeFactory.java	Wed Jan 09 16:42:51 2008 +0900
@@ -36,7 +36,7 @@
 	}
 
 	public ITLSolver existsNode(ITLSolver var, ITLSolver node) {
-		return new ExistsSolver(var,node);
+		return new ExistsSolver((VariableSolver)var,node);
 	}
 
 	public ITLSolver falseNode() {
--- a/src/lite/ITLNodeParser.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Wed Jan 09 16:42:51 2008 +0900
@@ -123,19 +123,20 @@
 		return n;
 	}
 
-	public Node exprI3() {
+	@Override
+	public Node expr4() {
 		if (nextToken.type == TokenID.Next) {
 			nextToken();
-			return logicNodeFactory.nextNode(exprM1());
+			return logicNodeFactory.nextNode(expr4());
 		}
-		return exprM1();
+		return super.expr4();
 	}
 	
 	public Node exprI2() {
-		Node n = exprI3();
+		Node n = exprM1();
 		while(nextToken.type == TokenID.Chop) {
 			nextToken();
-			n = logicNodeFactory.chopNode(n, exprI3());
+			n = logicNodeFactory.chopNode(n, exprM1());
 		}
 		return n;
 	}
--- a/src/lite/NextSolver.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/lite/NextSolver.java	Wed Jan 09 16:42:51 2008 +0900
@@ -41,4 +41,13 @@
 		if (hash!=-1) return hash;
 		return hash = BDDSolver.NODEHASH(TokenID.Next.hash,node.hashCode(),0);
 	}
+
+	public boolean equals(Object o) {
+		if (o.hashCode()!=hashCode()) return false;
+		if (o.getClass()==this.getClass()) {
+			NextSolver v = (NextSolver)o;
+			return node.equals(v.node);
+		}
+		return false;
+	}
 }
--- a/src/sbdd/SBDDTest.java	Wed Jan 09 12:40:01 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Wed Jan 09 16:42:51 2008 +0900
@@ -48,7 +48,7 @@
 	public void verifyTest() {
 		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");
 
-		if (true) {
+		if (false) {
 		sat.showVerify("skip");
 		sat.showVerify(" '<>'p");
 		sat.showVerify("<>(p) = <>(p)");
@@ -60,11 +60,16 @@
 		sat.showVerify("~(true& ~q)");
 		// sat.showVerify("@(@(@(empty)))");
 		sat.showVerify("fin(p)=([](<>(p)))");
+		sat.showVerify("fin(p)");
 		}
-		sat.showVerify("fin(p)");
-		System.out.println(sat.state);
-		sat.p.parse("include('data/example').");
-		System.out.println(p.parseCommand.sat.state);
+		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);
+		// sat.p.parse("include('data/example').");
+		// System.out.println(p.parseCommand.sat.state);
 	}