diff --git a/sat/res.ml b/sat/res.ml index c0b9daa9..a12da3a7 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -8,161 +8,161 @@ module type S = Res_intf.S module Make(St : Solver_types.S)(Proof : sig type t end) = struct - (* Type definitions *) - type lemma = Proof.t - type clause = St.clause - type atom = St.atom - type int_cl = St.atom list + (* Type definitions *) + type lemma = Proof.t + type clause = St.clause + type atom = St.atom + type int_cl = St.atom list - type node = - | Assumption - | Lemma of lemma - | Resolution of atom * int_cl * int_cl - (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) + type node = + | Assumption + | Lemma of lemma + | Resolution of atom * int_cl * int_cl + (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) - exception Tautology - exception Resolution_error of string + exception Tautology + exception Resolution_error of string - (* Proof graph *) - module H = Hashtbl.Make(struct - type t = St.atom list - let hash= Hashtbl.hash - let equal = List.for_all2 (==) + (* Proof graph *) + module H = Hashtbl.Make(struct + type t = St.atom list + let hash= Hashtbl.hash + let equal = List.for_all2 (==) end) - let proof : node H.t = H.create 1007;; + let proof : node H.t = H.create 1007;; - (* Misc functions *) - let compare_atoms a b = - Pervasives.compare St.(a.aid) St.(b.aid) + (* Misc functions *) + let compare_atoms a b = + Pervasives.compare St.(a.aid) St.(b.aid) - let equal_atoms a b = St.(a.aid) = St.(b.aid) + let equal_atoms a b = St.(a.aid) = St.(b.aid) - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause + (* Compute resolution of 2 clauses *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if equal_atoms a b then + aux resolved (a :: acc) r + else if equal_atoms St.(a.neg) b then + aux (St.(a.var.pa) :: resolved) acc r + else + aux resolved (a :: acc) (b :: r) + in + let resolved, new_clause = aux [] [] l in + resolved, List.rev new_clause - let to_list c = - let v = St.(c.atoms) in - let l = ref [] in - for i = 0 to Vec.size v - 1 do - l := (Vec.get v i) :: !l - done; - let l, res = resolve (List.sort_uniq compare_atoms !l) in - if l <> [] then - raise (Resolution_error "Input cause is a tautology"); - res + let to_list c = + let v = St.(c.atoms) in + let l = ref [] in + for i = 0 to Vec.size v - 1 do + l := (Vec.get v i) :: !l + done; + let l, res = resolve (List.sort_uniq compare_atoms !l) in + if l <> [] then + raise (Resolution_error "Input cause is a tautology"); + res - (* Adding new proven clauses *) - let is_proved c = H.mem proof c + (* Adding new proven clauses *) + let is_proved c = H.mem proof c - let rec add_res c d = - add_clause c; - add_clause d; - let cl_c = to_list c in - let cl_d = to_list d in - let l = List.merge compare_atoms cl_c cl_d in - let resolved, new_clause = resolve l in - match resolved with - | [] -> raise (Resolution_error "No literal to resolve over") - | [a] -> - H.add proof new_clause (Resolution (a, cl_c, cl_d)); - new_clause - | _ -> raise (Resolution_error "Resolved to a tautology") + let rec add_res c d = + add_clause c; + add_clause d; + let cl_c = to_list c in + let cl_d = to_list d in + let l = List.merge compare_atoms cl_c cl_d in + let resolved, new_clause = resolve l in + match resolved with + | [] -> raise (Resolution_error "No literal to resolve over") + | [a] -> + H.add proof new_clause (Resolution (a, cl_c, cl_d)); + new_clause + | _ -> raise (Resolution_error "Resolved to a tautology") - and add_clause c = - let cl = to_list c in - if is_proved cl then - () - else if not St.(c.learnt) then - H.add proof cl Assumption - else begin - let history = St.(c.cpremise) in - () - (* TODO - match history with - | a :: (_ :: _) as r -> - List.fold_left add_res a r - *) - end + and add_clause c = + let cl = to_list c in + if is_proved cl then + () + else if not St.(c.learnt) then + H.add proof cl Assumption + else begin + let history = St.(c.cpremise) in + () + (* TODO + match history with + | a :: (_ :: _) as r -> + List.fold_left add_res a r + *) + end - (* Print proof graph *) - let _i = ref 0 - let new_id () = incr _i; "id_" ^ (string_of_int !_i) + (* Print proof graph *) + let _i = ref 0 + let new_id () = incr _i; "id_" ^ (string_of_int !_i) - let ids : (bool * string) H.t = H.create 1007;; - let cl_id c = - try - snd (H.find ids c) - with Not_found -> - let id = new_id () in - H.add ids c (false, id); - id + let ids : (bool * string) H.t = H.create 1007;; + let cl_id c = + try + snd (H.find ids c) + with Not_found -> + let id = new_id () in + H.add ids c (false, id); + id - let is_drawn c = - try - fst (H.find ids c) - with Not_found -> - false + let is_drawn c = + try + fst (H.find ids c) + with Not_found -> + false - let has_drawn c = - assert (H.mem ids c); - let b, id = H.find ids c in - assert (not b); - H.replace ids c (true, id) + let has_drawn c = + assert (H.mem ids c); + let b, id = H.find ids c in + assert (not b); + H.replace ids c (true, id) - let print_atom fmt a = - Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) + let print_atom fmt a = + Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) - let rec print_clause fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> print_atom fmt a - | a :: (_ :: _) as r -> Format.fprintf fmt "%a \\/ %a" print_atom a print_clause r + let rec print_clause fmt = function + | [] -> Format.fprintf fmt "[]" + | [a] -> print_atom fmt a + | a :: (_ :: _) as r -> Format.fprintf fmt "%a \\/ %a" print_atom a print_clause r - let print_dot_rule f arg fmt cl = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - (cl_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\">" f arg + let print_dot_rule f arg fmt cl = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + (cl_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\">" f arg - let print_dot_edge c fmt d = - Format.fprintf fmt "%s -> %s;@\n" (cl_id c) (cl_id d) + let print_dot_edge c fmt d = + Format.fprintf fmt "%s -> %s;@\n" (cl_id c) (cl_id d) - let print_dot_proof fmt cl = - match H.find proof cl with - | Assumption -> - let aux fmt () = - Format.fprintf fmt "%a" print_clause cl - in - print_dot_rule aux () fmt cl - | Lemma _ -> - let aux fmt () = - Format.fprintf fmt "%ato prove ..." print_clause cl - in - print_dot_rule aux () fmt cl - | Resolution (r, c, d) -> - let aux fmt () = - Format.fprintf fmt "%a%a" - print_clause cl print_atom r - in - Format.fprintf fmt "%a%a%a" - (print_dot_rule aux ()) cl - (print_dot_edge cl) c - (print_dot_edge cl) d + let print_dot_proof fmt cl = + match H.find proof cl with + | Assumption -> + let aux fmt () = + Format.fprintf fmt "%a" print_clause cl + in + print_dot_rule aux () fmt cl + | Lemma _ -> + let aux fmt () = + Format.fprintf fmt "%ato prove ..." print_clause cl + in + print_dot_rule aux () fmt cl + | Resolution (r, c, d) -> + let aux fmt () = + Format.fprintf fmt "%a%a" + print_clause cl print_atom r + in + Format.fprintf fmt "%a%a%a" + (print_dot_rule aux ()) cl + (print_dot_edge cl) c + (print_dot_edge cl) d - let print_dot fmt cl = - assert (is_proved cl); - Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof cl + let print_dot fmt cl = + assert (is_proved cl); + Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof cl end diff --git a/sat/res.mli b/sat/res.mli index a957e1e4..5d3fbf14 100644 --- a/sat/res.mli +++ b/sat/res.mli @@ -7,4 +7,4 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S module Make : functor (St : Solver_types.S)(Proof : sig type t end) - -> S with type clause = St.clause and type lemma = Proof.t + -> S with type clause = St.clause and type lemma = Proof.t diff --git a/sat/res_intf.ml b/sat/res_intf.ml index 593326fd..5e732ab7 100644 --- a/sat/res_intf.ml +++ b/sat/res_intf.ml @@ -1,7 +1,7 @@ (* Copyright 2014 Guillaume Bury *) module type S = sig - type clause - type lemma + type clause + type lemma end diff --git a/sat/solver.ml b/sat/solver.ml index dd8789fc..a8a8b473 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -466,32 +466,32 @@ module Make (F : Formula_intf.S) let locked c = Vec.exists (fun v -> match v.reason with - | Some c' -> c ==c' - | _ -> false + | Some c' -> c ==c' + | _ -> false ) env.vars (* remove some learnt clauses *) let reduce_db () = - let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in - Vec.sort env.learnts f_sort_db; - let lim2 = Vec.size env.learnts in - let lim1 = lim2 / 2 in - let j = ref 0 in - for i = 0 to lim1 - 1 do - let c = Vec.get env.learnts i in - if Vec.size c.atoms > 2 && not (locked c) then - remove_clause c - else - begin Vec.set env.learnts !j c; incr j end - done; - for i = lim1 to lim2 - 1 do - let c = Vec.get env.learnts i in - if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then - remove_clause c - else - begin Vec.set env.learnts !j c; incr j end - done; - Vec.shrink env.learnts (lim2 - !j) + let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in + Vec.sort env.learnts f_sort_db; + let lim2 = Vec.size env.learnts in + let lim1 = lim2 / 2 in + let j = ref 0 in + for i = 0 to lim1 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + for i = lim1 to lim2 - 1 do + let c = Vec.get env.learnts i in + if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then + remove_clause c + else + begin Vec.set env.learnts !j c; incr j end + done; + Vec.shrink env.learnts (lim2 - !j) (* remove from [vec] the clauses that are satisfied in the current trail *) let remove_satisfied vec = @@ -792,7 +792,7 @@ module Make (F : Formula_intf.S) check_vec env.learnts (* fixpoint of propagation and decisions until a model is found, or a - conflict is reached *) + conflict is reached *) let solve () = if env.is_unsat then raise (Unsat env.unsat_core); let n_of_conflicts = ref (to_float env.restart_first) in @@ -800,8 +800,8 @@ module Make (F : Formula_intf.S) try while true do begin try - search (to_int !n_of_conflicts) (to_int !n_of_learnts); - with Restart -> () + search (to_int !n_of_conflicts) (to_int !n_of_learnts); + with Restart -> () end; n_of_conflicts := !n_of_conflicts *. env.restart_inc; n_of_learnts := !n_of_learnts *. env.learntsize_inc; @@ -924,7 +924,7 @@ module Make (F : Formula_intf.S) let pop l = if l > current_level() - then invalid_arg "cannot pop() to level, it is too high"; + then invalid_arg "cannot pop() to level, it is too high"; let i = Vec.get env.levels l in (* see whether we can reset [env.is_unsat] *) if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( diff --git a/sat/solver.mli b/sat/solver.mli index 3f472335..792530f5 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -18,7 +18,7 @@ module Make (F : Formula_intf.S) sig (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *) - + exception Unsat of St.clause list val solve : unit -> unit diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 529028c2..f33f5e2f 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -64,8 +64,8 @@ module Make (F : Formula_intf.S) = struct { var = dummy_var; lit = dummy_lit; watched = Obj.magic 0; - (* should be [Vec.make_empty dummy_clause] - but we have to break the cycle *) + (* should be [Vec.make_empty dummy_clause] + but we have to break the cycle *) neg = dummy_atom; is_true = false; aid = -102 } diff --git a/util/parser.ml b/util/parser.ml index 5eeb2511..4863338d 100644 --- a/util/parser.ml +++ b/util/parser.ml @@ -3,52 +3,52 @@ exception Syntax_error of int type line = - | Empty - | Comment - | Pcnf of int * int - | Clause of int list + | Empty + | Comment + | Pcnf of int * int + | Clause of int list let ssplit = Str.split (Str.regexp "[ \t]+") let of_input f = - match ssplit (input_line f) with - | [] -> Empty - | "c" :: _ -> Comment - | "p" :: "cnf" :: i :: j :: [] -> - begin try - Pcnf (int_of_string i, int_of_string j) - with Invalid_argument _ -> - raise (Syntax_error (-1)) - end - | l -> - begin try - begin match List.rev_map int_of_string l with - | 0 :: r -> Clause r - | _ -> raise (Syntax_error (-1)) - end - with Invalid_argument _ -> raise (Syntax_error (-1)) - end + match ssplit (input_line f) with + | [] -> Empty + | "c" :: _ -> Comment + | "p" :: "cnf" :: i :: j :: [] -> + begin try + Pcnf (int_of_string i, int_of_string j) + with Invalid_argument _ -> + raise (Syntax_error (-1)) + end + | l -> + begin try + begin match List.rev_map int_of_string l with + | 0 :: r -> Clause r + | _ -> raise (Syntax_error (-1)) + end + with Invalid_argument _ -> raise (Syntax_error (-1)) + end let parse_with todo file = - let f = open_in file in - let line = ref 0 in - try - while true do - incr line; - todo (of_input f) - done - with - | Syntax_error _ -> - raise (Syntax_error !line) - | End_of_file -> - close_in f + let f = open_in file in + let line = ref 0 in + try + while true do + incr line; + todo (of_input f) + done + with + | Syntax_error _ -> + raise (Syntax_error !line) + | End_of_file -> + close_in f let cnf = ref [] let parse_line = function - | Empty | Comment | Pcnf _ -> () - | Clause l -> cnf := l :: !cnf + | Empty | Comment | Pcnf _ -> () + | Clause l -> cnf := l :: !cnf let parse f = - cnf := []; - parse_with parse_line f; - !cnf + cnf := []; + parse_with parse_line f; + !cnf