diff src/lite/BDDSolver.java @ 64:80db395eeb30 quantifier-worked

*** empty log message ***
author kono
date Thu, 10 Jan 2008 18:16:00 +0900
parents d6a300cdd18e
children 4ced2af1ff09
line wrap: on
line diff
--- 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);
 			}
 		}
 	}