comparison 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
comparison
equal deleted inserted replaced
63:d6a300cdd18e 64:80db395eeb30
119 } else { 119 } else {
120 // lf.bddNode(cond,high,low) won't work 120 // lf.bddNode(cond,high,low) won't work
121 if (low==null) low = sat.lf.falseNode(); 121 if (low==null) low = sat.lf.falseNode();
122 if (high==null) high = sat.lf.falseNode(); 122 if (high==null) high = sat.lf.falseNode();
123 // if (cond==null) cond = sat.lf.falseNode(); 123 // if (cond==null) cond = sat.lf.falseNode();
124 return next.sat(sat.lf.orNode( 124 ITLSolver value = sat.lf.orNode(
125 sat.lf.andNode(cond, high), 125 sat.lf.andNode(cond, high),
126 sat.lf.andNode(sat.lf.notNode(cond), low))); 126 sat.lf.andNode(sat.lf.notNode(cond), low));
127 if (value==sat.false_) value = null;
128 return next.sat(value);
127 } 129 }
128 } 130 }
129 } 131 }
130 132
131 133