469 (* prop_formula -> int list *) |
469 (* prop_formula -> int list *) |
470 fun forced_vars True = [] |
470 fun forced_vars True = [] |
471 | forced_vars False = [] |
471 | forced_vars False = [] |
472 | forced_vars (BoolVar i) = [i] |
472 | forced_vars (BoolVar i) = [i] |
473 | forced_vars (Not (BoolVar i)) = [~i] |
473 | forced_vars (Not (BoolVar i)) = [~i] |
474 | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) |
474 | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1, forced_vars fm2) |
475 | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) |
475 | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1, forced_vars fm2) |
476 (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) |
476 (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) |
477 (* precedence, and the next partial evaluation of the formula returns 'False'. *) |
477 (* precedence, and the next partial evaluation of the formula returns 'False'. *) |
478 | forced_vars _ = error "formula is not in negation normal form" |
478 | forced_vars _ = error "formula is not in negation normal form" |
479 (* int list -> prop_formula -> (int list * prop_formula) *) |
479 (* int list -> prop_formula -> (int list * prop_formula) *) |
480 fun eval_and_force xs fm = |
480 fun eval_and_force xs fm = |