Mercurial > hg > Applications > JavaLite
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 |