Mercurial > hg > Applications > JavaLite

changeset 78:70cc3ff5c73b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Thu, 17 Jan 2008 11:09:15 +0900
parents c92c9e11d525
children c263dc76d1a7
files src/lite/BDDSolver.java src/lite/ChopSolver.java src/lite/Continuation.java src/lite/ITLCommander.java src/lite/ITLSolver.java
diffstat 5 files changed, 12 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/BDDSolver.java	Thu Jan 17 10:42:05 2008 +0900
+++ b/src/lite/BDDSolver.java	Thu Jan 17 11:09:15 2008 +0900
@@ -199,7 +199,7 @@
 
 	public boolean equals(Object o) {
 		if (o==this) return true;
-		if (o.hashCode()!=hashCode()) return false;
+		// if (o.hashCode()!=hashCode()) return false;
 		if (o.getClass()==this.getClass()) {
 			BDDSolver v = (BDDSolver)o;
 			switch(id) {
--- a/src/lite/ChopSolver.java	Thu Jan 17 10:42:05 2008 +0900
+++ b/src/lite/ChopSolver.java	Thu Jan 17 11:09:15 2008 +0900
@@ -8,9 +8,6 @@
 
 	protected ITLSolver former;
 	private ITLSolver later;
-	//private VariableSolver innerEmpty;
-	//private ITLSolver outerEmpty;
-	ITLSolver later1;
 
 	/*
 	 *    Interval Temporal Logic Chop Operator
@@ -118,13 +115,14 @@
 				return former.sat(sat,  new Continuation(sat,next, new ChopSolver4()));
 			} else {
 				// try innerMore case with this next term
-				later1 = value;
-				return former.sat(sat,  new Continuation(sat,next, new ChopSolver6()));
+				return former.sat(sat,  new Continuation(sat,next, new ChopSolver6(value)));
 			}
 		}
 	}
 	
 	class ChopSolver6 implements Next {
+		ITLSolver later1;
+		ChopSolver6(ITLSolver value) { later1 = value; }
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
 			try {
 			if (value==null) {  // former is fail on more inerval
--- a/src/lite/Continuation.java	Thu Jan 17 10:42:05 2008 +0900
+++ b/src/lite/Continuation.java	Thu Jan 17 11:09:15 2008 +0900
@@ -8,6 +8,11 @@
 	public Continuation next;
 	public Next solver;
 
+	/*
+	 * Depth first search stack
+	 * we use CPS style programming for try/throw backtrack
+	 * but it is better to use stack base implementation?
+	 */
 	public Continuation(ITLSatisfier sat, Continuation next, Next solver) {
 		// keep next and our boss's state (solver)
 		this.sat = sat; this.next = next; this.solver = solver;
--- a/src/lite/ITLCommander.java	Thu Jan 17 10:42:05 2008 +0900
+++ b/src/lite/ITLCommander.java	Thu Jan 17 11:09:15 2008 +0900
@@ -110,7 +110,7 @@
 			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
 			diag.counterExample(sat.last, length);
 		}
-		System.out.println("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
+		parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
 		return value;
 	}
 
--- a/src/lite/ITLSolver.java	Thu Jan 17 10:42:05 2008 +0900
+++ b/src/lite/ITLSolver.java	Thu Jan 17 11:09:15 2008 +0900
@@ -10,9 +10,8 @@
 public class ITLSolver extends LogicSolver 
 	implements Next,BDDInterface {
 	
-	public boolean value;
-	public int hash=-1;
-	public int order=-1;
+	public int hash=-1;     // hash value cache
+	public int order=-1;    // BDD variable order for this subterm
 	
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return null;