Mercurial > hg > Applications > JavaLite

changeset 62:c392bd59155f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
あきらかに、exists はバグってるね。
author kono
date Thu, 10 Jan 2008 02:29:42 +0900
parents 51e13324a3f1
children d6a300cdd18e
files Changes src/sbdd/BDDSatisfier.java src/sbdd/SBDDTest.java
diffstat 3 files changed, 22 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Changes	Wed Jan 09 19:57:56 2008 +0900
+++ b/Changes	Thu Jan 10 02:29:42 2008 +0900
@@ -1,3 +1,16 @@
+Wed Jan  9 20:42:17 JST 2008
+
+あぁ、そうか。
+    define("forall(x,body)","~exists(x,~body)");
+    forall(a,(a;~a))
+では、 body は、exists に入る前に、(a;~a) に換えられちゃうので、
+exits は、その既に換えられてしまったa をlocal 変数にするこ
+とが出来ないわけね。名前は同じなんだけど。
+
+なので、変数を扱う時には、一旦、var = lf.variableNode(var.name);
+みたいなことをやっていたわけか。まぁ、それがいいのかなぁ。
+
+
 Tue Jan  8 02:16:17 JST 2008
 
     Sat 
--- a/src/sbdd/BDDSatisfier.java	Wed Jan 09 19:57:56 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Thu Jan 10 02:29:42 2008 +0900
@@ -95,6 +95,7 @@
 		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.");
--- a/src/sbdd/SBDDTest.java	Wed Jan 09 19:57:56 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Thu Jan 10 02:29:42 2008 +0900
@@ -48,7 +48,7 @@
 	public void verifyTest() {
 		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");
 
-		if (false) {
+		if (true) {
 		sat.showVerify("skip");
 		sat.showVerify(" '<>'p");
 		sat.showVerify("<>(p) = <>(p)");
@@ -61,14 +61,18 @@
 		// sat.showVerify("@(@(@(empty)))");
 		sat.showVerify("fin(p)=([](<>(p)))");
 		sat.showVerify("fin(p)");
-		}
+		sat.showVerify("all(x,@y)");
 		sat.showVerify("exists(x,@@x = ~x)");
-		//sat.showVerify("even(p)");
+		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("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);
 	}