equal
deleted
inserted
replaced
500 case fm' of |
500 case fm' of |
501 True => SOME xs' |
501 True => SOME xs' |
502 | False => NONE |
502 | False => NONE |
503 | _ => |
503 | _ => |
504 let |
504 let |
505 val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) |
505 val x = the (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) |
506 in |
506 in |
507 case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) |
507 case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) |
508 SOME xs'' => SOME xs'' |
508 SOME xs'' => SOME xs'' |
509 | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) |
509 | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) |
510 end |
510 end |
891 val ls = map int_from_string ids |
891 val ls = map int_from_string ids |
892 (* the conflict clause must be resolved with the unit clauses *) |
892 (* the conflict clause must be resolved with the unit clauses *) |
893 (* for its literals to obtain the empty clause *) |
893 (* for its literals to obtain the empty clause *) |
894 val vids = map (fn l => l div 2) ls |
894 val vids = map (fn l => l div 2) ls |
895 val rs = cid :: map (fn v => !clause_offset + v) vids |
895 val rs = cid :: map (fn v => !clause_offset + v) vids |
896 val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 |
896 val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1 |
897 in |
897 in |
898 (* update clause table and conflict id *) |
898 (* update clause table and conflict id *) |
899 clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) |
899 clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) |
900 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); |
900 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); |
901 empty_id := new_empty_id |
901 empty_id := new_empty_id |