diff --git a/.merlin b/.merlin index d9bc3db3..63265db9 100644 --- a/.merlin +++ b/.merlin @@ -1,12 +1,10 @@ S sat S smt S solver -S mcsolver S util B _build/ B _build/sat B _build/smt B _build/solver -B _build/mcsolver B _build/util diff --git a/Makefile b/Makefile index fb58f8a1..5edfdad9 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= -DIRS=-Is mcsolver,solver,sat,smt,util,util/smtlib +DIRS=-Is solver,sat,smt,util,util/smtlib DOC=msat.docdir/index.html TEST=sat_solve.native bench_stats.native diff --git a/_tags b/_tags index 589352bd..59ab6e13 100644 --- a/_tags +++ b/_tags @@ -3,7 +3,6 @@ : for-pack(Msat), package(zarith) : for-pack(Msat) : for-pack(Msat) -: for-pack(Msat) # enable stronger inlining everywhere : inline(15) diff --git a/msat.mlpack b/msat.mlpack index b23032f6..b62d96df 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -12,6 +12,7 @@ Plugin_intf # Auxiliary modules Res +Mcproof Tseitin Tseitin_intf diff --git a/solver/.merlin b/solver/.merlin index 9350d683..d9b70b68 100644 --- a/solver/.merlin +++ b/solver/.merlin @@ -1,7 +1,6 @@ S ./ -S ../common/ +S ../util/ B ../_build/ -B ../_build/sat/ +B ../_build/solver/ B ../_build/util/ -B ../_build/common/ diff --git a/mcsolver/expr_intf.ml b/solver/expr_intf.ml similarity index 100% rename from mcsolver/expr_intf.ml rename to solver/expr_intf.ml diff --git a/solver/mcproof.ml b/solver/mcproof.ml new file mode 100644 index 00000000..bc9cd0e4 --- /dev/null +++ b/solver/mcproof.ml @@ -0,0 +1,375 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module type S = Res_intf.S + +module Make(St : Mcsolver_types.S) = struct + + (* Type definitions *) + type lemma = St.proof + type clause = St.clause + type atom = St.atom + type int_cl = clause * 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 *) + + exception Insuficient_hyps + exception Resolution_error of string + + (* Proof graph *) + let hash_cl cl = + Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl) + + let equal_cl cl_c cl_d = + try + List.for_all2 (==) cl_c cl_d + with Invalid_argument _ -> + false + + module H = Hashtbl.Make(struct + type t = St.atom list + let hash = hash_cl + let equal = equal_cl + end) + let proof : node H.t = H.create 1007;; + let unit_hyp : (clause * St.atom list) H.t = H.create 37;; + + (* Misc functions *) + let equal_atoms a b = St.(a.aid) = St.(b.aid) + let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) + + let merge = List.merge compare_atoms + + let _c = ref 0 + let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c) + + (* Printing functions *) + let rec print_cl fmt = function + | [] -> Format.fprintf fmt "[]" + | [a] -> St.print_atom fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r + + (* 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.tag.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 + + (* Adding hyptoheses *) + let is_unit_hyp = function + | [a] -> St.(a.var.level = 0 && a.var.tag.reason = Bcp None && a.var.tag.vpremise <> History []) + | _ -> false + + let make_unit_hyp a = + let aux a = St.(make_clause (fresh_name ()) [a] 1 false (History [])) in + if St.(a.is_true) then + aux a + else if St.(a.neg.is_true) then + aux St.(a.neg) + else + assert false + + let unit_hyp a = + let a = St.(a.var.tag.pa) in + try + H.find unit_hyp [a] + with Not_found -> + let c = make_unit_hyp a in + let cl = to_list c in + H.add unit_hyp [a] (c, cl); + (c, cl) + + let is_proved (c, cl) = + if H.mem proof cl then + true + else if is_unit_hyp cl || not St.(c.learnt) then begin + H.add proof cl Assumption; + true + end else match St.(c.cpremise) with + | St.Lemma p -> H.add proof cl (Lemma p); true + | St.History _ -> false + + let is_proven c = is_proved (c, to_list c) + + let add_res (c, cl_c) (d, cl_d) = + Log.debug 7 " Resolving clauses :"; + Log.debug 7 " %a" St.pp_clause c; + Log.debug 7 " %a" St.pp_clause d; + assert (is_proved (c, cl_c)); + assert (is_proved (d, cl_d)); + let l = merge 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, (c, cl_c), (d, cl_d))); + let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in + Log.debug 5 "New clause : %a" St.pp_clause new_c; + new_c, new_clause + | _ -> raise (Resolution_error "Resolved to a tautology") + + let rec diff_learnt acc l l' = + match l, l' with + | [], _ -> l' @ acc + | a :: r, b :: r' -> + if equal_atoms a b then + diff_learnt acc r r' + else + diff_learnt (b :: acc) l r' + | _ -> raise (Resolution_error "Impossible to derive correct clause") + + let clause_unit a = match St.(a.var.level, a.var.tag.reason) with + | 0, St.Bcp Some c -> c, to_list c + | 0, St.Bcp None -> + let c, cl = unit_hyp a in + if is_proved (c, cl) then + c, cl + else + assert false + | _ -> + raise (Resolution_error "Could not find a reason needed to resolve") + + let add_clause c cl l = (* We assume that all clauses in l are already proved ! *) + match l with + | a :: r -> + Log.debug 5 "Resolving (with history) %a" St.pp_clause c; + let temp_c, temp_cl = List.fold_left add_res a r in + Log.debug 10 " Switching to unit resolutions"; + let new_c, new_cl = (ref temp_c, ref temp_cl) in + while not (equal_cl cl !new_cl) do + let unit_to_use = diff_learnt [] cl !new_cl in + let unit_r = List.map (fun a -> clause_unit a) unit_to_use in + let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in + new_c := temp_c; + new_cl := temp_cl; + done + | _ -> assert false + + let need_clause (c, cl) = + if is_proved (c, cl) then + [] + else + match St.(c.cpremise) with + | St.History l -> l + | St.Lemma _ -> assert false + + let rec do_clause = function + | [] -> () + | c :: r -> + let cl = to_list c in + match need_clause (c, cl) with + | [] -> do_clause r + | history -> + let history_cl = List.rev_map (fun c -> c, to_list c) history in + let to_prove = List.filter (fun (c, cl) -> not (is_proved (c, cl))) history_cl in + let to_prove = (List.rev_map fst to_prove) in + begin match to_prove with + | [] -> + add_clause c cl history_cl; + do_clause r + | _ -> do_clause (to_prove @ (c :: r)) + end + + let prove c = + Log.debug 3 "Proving : %a" St.pp_clause c; + do_clause [c]; + Log.debug 3 "Proved : %a" St.pp_clause c + + let rec prove_unsat_cl (c, cl) = match cl with + | [] -> true + | a :: r -> + Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; + let d = match St.(a.var.level, a.var.tag.reason) with + | 0, St.Bcp Some d -> d + | 0, St.Bcp None -> + let d, cl_d = unit_hyp a in + if is_proved (d, cl_d) then d else raise Exit + | _ -> raise Exit + in + prove d; + let cl_d = to_list d in + prove_unsat_cl (add_res (c, cl) (d, cl_d)) + + let prove_unsat_cl c = + try + prove_unsat_cl c + with Exit -> + false + + let learn v = + Vec.iter (fun c -> Log.debug 15 "history : %a" St.pp_clause c) v; + Vec.iter prove v + + let assert_can_prove_unsat c = + Log.debug 1 "=================== Proof ====================="; + prove c; + if not (prove_unsat_cl (c, to_list c)) then + raise Insuficient_hyps + + (* Interface exposed *) + type proof_node = { + conclusion : clause; + step : step; + } + and proof = unit -> proof_node + and step = + | Hypothesis + | Lemma of lemma + | Resolution of proof * proof * atom + + let rec return_proof (c, cl) () = + Log.debug 8 "Returning proof for : %a" St.pp_clause c; + let st = match H.find proof cl with + | Assumption -> Hypothesis + | Lemma l -> Lemma l + | Resolution (a, cl_c, cl_d) -> + Resolution (return_proof cl_c, return_proof cl_d, a) + in + { conclusion = c; step = st } + + let prove_unsat c = + assert_can_prove_unsat c; + return_proof (St.empty_clause, []) + + (* Compute unsat-core *) + let compare_cl c d = + let rec aux = function + | [], [] -> 0 + | a :: r, a' :: r' -> begin match compare_atoms a a' with + | 0 -> aux (r, r') + | x -> x + end + | _ :: _ , [] -> -1 + | [], _ :: _ -> 1 + in + aux (to_list c, to_list d) + + let unsat_core proof = + let rec aux proof = + let p = proof () in + match p.step with + | Hypothesis | Lemma _ -> [p.conclusion] + | Resolution (proof1, proof2, _) -> + List.rev_append (aux proof1) (aux proof2) + in + List.sort_uniq compare_cl (aux proof) + + (* Print proof graph *) + let _i = ref 0 + let new_id () = incr _i; "id_" ^ (string_of_int !_i) + + let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; + let c_id c = + try + snd (Hashtbl.find ids c) + with Not_found -> + let id = new_id () in + Hashtbl.add ids c (false, id); + id + + let clear_ids () = + Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids + + let is_drawn c = + ignore (c_id c); + fst (Hashtbl.find ids c) + + let has_drawn c = + if not (is_drawn c) then + let b, id = Hashtbl.find ids c in + Hashtbl.replace ids c (true, id) + else + () + + (* We use a custom function instead of the functions in Solver_type, + so that atoms are sorted before printing. *) + let print_clause fmt c = print_cl fmt (to_list c) + + let print_dot_rule opt f arg fmt cl = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg + + let print_dot_edge id_c fmt id_d = + Format.fprintf fmt "%s -> %s;@\n" id_c id_d + + let print_res_atom id fmt a = + Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a + + let print_res_node concl p1 p2 fmt atom = + let id = new_id () in + Format.fprintf fmt "%a;@\n%a%a%a" + (print_res_atom id) atom + (print_dot_edge (c_id concl)) id + (print_dot_edge id) (c_id p1) + (print_dot_edge id) (c_id p2) + + let color s = match s.[0] with + | 'E' -> "BGCOLOR=\"GREEN\"" + | 'L' -> "BGCOLOR=\"GREEN\"" + | _ -> "BGCOLOR=\"GREY\"" + + let rec print_dot_proof fmt p = + if not (is_drawn p.conclusion) then begin + has_drawn p.conclusion; + match p.step with + | Hypothesis -> + let aux fmt () = + Format.fprintf fmt "%aHypothesis%s" + print_clause p.conclusion St.(p.conclusion.name) + in + print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion + | Lemma _ -> + let aux fmt () = + Format.fprintf fmt "%aLemma%s" + print_clause p.conclusion St.(p.conclusion.name) + in + print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion + | Resolution (proof1, proof2, a) -> + let aux fmt () = + Format.fprintf fmt "%a%s%s" + print_clause p.conclusion + "Resolution" St.(p.conclusion.name) + in + let p1 = proof1 () in + let p2 = proof2 () in + Format.fprintf fmt "%a%a%a%a" + (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion + (print_res_node p.conclusion p1.conclusion p2.conclusion) a + print_dot_proof p1 + print_dot_proof p2 + end + + let print_dot fmt proof = + clear_ids (); + Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) + +end + diff --git a/solver/mcproof.mli b/solver/mcproof.mli new file mode 100644 index 00000000..8c201639 --- /dev/null +++ b/solver/mcproof.mli @@ -0,0 +1,11 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module type S = Res_intf.S + +module Make : functor (St : Mcsolver_types.S) + -> S with type atom = St.atom and type clause = St.clause and type lemma = St.proof +(** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/mcsolver/mcsolver.ml b/solver/mcsolver.ml similarity index 86% rename from mcsolver/mcsolver.ml rename to solver/mcsolver.ml index 9c63fb20..d40acb11 100644 --- a/mcsolver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -14,7 +14,7 @@ module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct module St = Mcsolver_types.Make(E)(Th) - (* module Proof = Res.Make(St) *) + module Proof = Mcproof.Make(St) open St @@ -30,11 +30,6 @@ module Make (E : Expr_intf.S) ul_learnt : int; (* number of learnt clauses *) } - (* Type for trail elements *) - type trail_elt = - | Semantic of semantic var - | Boolean of atom - (* Singleton type containing the current state *) type env = { @@ -56,7 +51,7 @@ module Make (E : Expr_intf.S) mutable var_inc : float; (* increment for variables' activity *) - trail : trail_elt Vec.t; + trail : (semantic var, atom) Either.t Vec.t; (* decision stack + propagated atoms *) trail_lim : int Vec.t; @@ -127,7 +122,7 @@ module Make (E : Expr_intf.S) learnts = Vec.make 0 dummy_clause; (*updated during parsing*) clause_inc = 1.; var_inc = 1.; - trail = Vec.make 601 (Boolean dummy_atom); + trail = Vec.make 601 (Either.mk_right dummy_atom); trail_lim = Vec.make 601 (-1); user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0}; qhead = 0; @@ -161,17 +156,20 @@ module Make (E : Expr_intf.S) let to_float i = float_of_int i let to_int f = int_of_float f - let get_elt_weight = function - | Term v -> v.weight - | Formula v -> v.weight + (* Accessors for variables *) + let get_var_id v = v.vid + let get_var_level v = v.level + let get_var_weight v = v.weight - let set_elt_weight e w = match e with - | Term v -> v.weight <- w - | Formula v -> v.weight <- w + let set_var_weight v w = v.weight <- w + let set_var_level v l = v.level <- l - let get_elt_level = function - | Term v -> v.level - | Formula v -> v.level + let get_elt_id e = Either.destruct e get_var_id get_var_id + let get_elt_weight e = Either.destruct e get_var_weight get_var_weight + let get_elt_level e = Either.destruct e get_var_level get_var_level + + let set_elt_weight e = Either.destruct e set_var_weight set_var_weight + let set_elt_level e = Either.destruct e set_var_level set_var_level let f_weight i j = get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i) @@ -180,13 +178,12 @@ module Make (E : Expr_intf.S) get_elt_level (St.get_var i) < 0 (* Var/clause activity *) - let rec insert_var_order = function - | Term v -> - Iheap.insert f_weight env.order v.vid - | Formula v -> - Iheap.insert f_weight env.order v.vid; - Th.iter_assignable - (fun t -> insert_var_order (Term (St.add_term t))) v.tag.pa.lit + let rec insert_var_order e = Either.destruct e + (fun v -> Iheap.insert f_weight env.order v.vid) + (fun v -> + Iheap.insert f_weight env.order v.vid; + Th.iter_assignable (fun t -> + insert_var_order (Either.mk_left (St.add_term t))) v.tag.pa.lit) let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay @@ -263,15 +260,15 @@ module Make (E : Expr_intf.S) env.qhead <- Vec.get env.trail_lim lvl; env.tatoms_qhead <- env.qhead; for c = Vec.size env.trail - 1 downto env.qhead do - match Vec.get env.trail c with - | Boolean a -> + Either.destruct (Vec.get env.trail c) + (fun a -> ()) + (fun a -> a.is_true <- false; a.neg.is_true <- false; a.var.level <- -1; a.var.tag.reason <- Bcp None; a.var.tag.vpremise <- History []; - insert_var_order (Formula a.var) - | Semantic a -> () + insert_var_order (Either.mk_right a.var)) done; Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); @@ -296,24 +293,58 @@ module Make (E : Expr_intf.S) a.var.level <- lvl; a.var.tag.reason <- reason; Log.debug 8 "Enqueue: %a" pp_atom a; - Vec.push env.trail (Boolean a) + Vec.push env.trail (Either.mk_right a) let enqueue_assign v value lvl = v.tag.assigned <- Some value; v.level <- lvl; - Vec.push env.trail (Semantic v) + Log.debug 5 "Enqueue: %a" St.pp_semantic_var v; + Vec.push env.trail (Either.mk_left v) (* conflict analysis *) + let max_lvl_atoms l = + List.fold_left (fun (max_lvl, acc) a -> + if a.var.level = max_lvl then (max_lvl, a :: acc) + else if a.var.level > max_lvl then (a.var.level, [a]) + else (max_lvl, acc)) (0, []) l + let analyze c_clause = - let pathC = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = ref [] in - let c = ref c_clause in - let tr_ind = ref (Vec.size env.trail - 1) in - let size = ref 1 in + let tr_ind = ref (Vec.size env.trail) in + let blevel = ref 0 in + let is_uip = ref false in + let c = ref (Proof.to_list c_clause) in let history = ref [] in + + let is_semantic a = match a.var.tag.reason with + | Semantic _ -> true + | _ -> false + in + + try while true do + let l, atoms = max_lvl_atoms !c in + match atoms with + | [] | _ :: [] -> + blevel := -1; + raise Exit + | _ when List.for_all is_semantic atoms -> + blevel := l - 1; + raise Exit + | _ -> + decr tr_ind; + Either.destruct (Vec.get env.trail !tr_ind) + (fun v -> ()) + (fun a -> match a.var.tag.reason with + | Bcp (Some d) -> + let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in + begin match tmp with + | [b] when b == a.neg -> c := !c + | _ -> () + end + | _ -> ()) + done; assert false + with Exit -> + !blevel, !c, !history, !is_uip + (* while !cond do if !c.learnt then clause_bump_activity !c; history := !c :: !history; @@ -349,27 +380,33 @@ module Make (E : Expr_intf.S) | n, Some cl -> c := cl done; List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size + *) - let record_learnt_clause blevel learnt history size = + let record_learnt_clause blevel learnt history is_uip = begin match learnt with | [] -> assert false | [fuip] -> assert (blevel = 0); fuip.var.tag.vpremise <- history; let name = fresh_lname () in - let uclause = make_clause name learnt size true history in + let uclause = make_clause name learnt (List.length learnt) true history in Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause; Vec.push env.learnts uclause; enqueue_bool fuip 0 (Bcp (Some uclause)) | fuip :: _ -> let name = fresh_lname () in - let lclause = make_clause name learnt size true history in + let lclause = make_clause name learnt (List.length learnt) true history in Log.debug 2 "New clause learnt : %a" St.pp_clause lclause; Vec.push env.learnts lclause; attach_clause lclause; clause_bump_activity lclause; - enqueue_bool fuip blevel (Bcp (Some lclause)) + if is_uip then + enqueue_bool fuip blevel (Bcp (Some lclause)) + else begin + env.decisions <- env.decisions + 1; + new_decision_level(); + enqueue_bool fuip blevel (Bcp None) + end end; var_decay_activity (); clause_decay_activity () @@ -377,9 +414,9 @@ module Make (E : Expr_intf.S) let add_boolean_conflict confl = env.conflicts <- env.conflicts + 1; if decision_level() = 0 then report_unsat confl; (* Top-level conflict *) - let blevel, learnt, history, size = analyze confl in + let blevel, learnt, history, is_uip = analyze confl in cancel_until blevel; - record_learnt_clause blevel learnt (History history) size + record_learnt_clause blevel learnt (History history) is_uip (* Add a new clause *) exception Trivial @@ -536,16 +573,15 @@ module Make (E : Expr_intf.S) (* Propagation (boolean and theory *) let _th_cnumber = ref 0 - let slice_get i = match (Vec.get env.trail i) with - | Boolean a -> Th.Lit a.lit - | Semantic {tag={term; assigned = Some v}} -> Th.Assign (term, v) - | _ -> assert false + let slice_get i = Either.destruct (Vec.get env.trail i) + (function {tag={term; assigned = Some v}} -> Th.Assign (term, v) | _ -> assert false) + (fun a -> Th.Lit a.lit) let slice_push l lemma = decr _th_cnumber; let atoms = List.rev_map (fun x -> add_atom x) l in Iheap.grow_to_by_double env.order (St.nb_vars ()); - List.iter (fun a -> insert_var_order (Formula a.var)) atoms; + List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms; add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma) let current_slice () = Th.({ @@ -573,12 +609,12 @@ module Make (E : Expr_intf.S) let num_props = ref 0 in let res = ref None in while env.qhead < Vec.size env.trail do - match Vec.get env.trail env.qhead with - | Boolean a -> + Either.destruct (Vec.get env.trail env.qhead) + (fun a -> ()) + (fun a -> env.qhead <- env.qhead + 1; incr num_props; - propagate_atom a res - | Semantic a -> () + propagate_atom a res) done; env.propagations <- env.propagations + !num_props; env.simpDB_props <- env.simpDB_props - !num_props; @@ -598,7 +634,7 @@ module Make (E : Expr_intf.S) if sz1 > 2 && (sz2 = 2 || c < 0) then -1 else 1 - (* returns true if the clause is used as a reason for a propagation, +(* returns true if the clause is used as a reason for a propagation, and therefore can be needed in case of conflict. In this case the clause can't be forgotten *) let locked c = false (* @@ -662,16 +698,16 @@ module Make (E : Expr_intf.S) (* Decide on a new litteral *) let rec pick_branch_lit () = let max = Iheap.remove_min f_weight env.order in - match St.get_var max with - | Term v -> + Either.destruct (St.get_var max) + (fun v -> let value = Th.assign v.tag.term in env.decisions <- env.decisions + 1; new_decision_level(); let current_level = decision_level () in assert (v.level < 0); -(* Log.debug 5 "Assigning %a to %a" St.pp_atom v.tag.pa; *) - enqueue_assign v value current_level - | Formula v -> + Log.debug 5 "Deciding on %a" St.pp_semantic_var v; + enqueue_assign v value current_level) + (fun v -> if v.level>= 0 then begin assert (v.tag.pa.is_true || v.tag.na.is_true); pick_branch_lit () @@ -683,9 +719,9 @@ module Make (E : Expr_intf.S) assert (v.level < 0); Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa; enqueue_bool v.tag.pa current_level (Bcp None) - | Th.Bool b -> + | Th.Valued (b, lvl) -> let a = if b then v.tag.pa else v.tag.na in - enqueue_bool a (decision_level ()) (Bcp None) + enqueue_bool a lvl (Bcp None)) let search n_of_conflicts n_of_learnts = let conflictC = ref 0 in diff --git a/mcsolver/mcsolver.mli b/solver/mcsolver.mli similarity index 100% rename from mcsolver/mcsolver.mli rename to solver/mcsolver.mli diff --git a/mcsolver/mcsolver_types.ml b/solver/mcsolver_types.ml similarity index 90% rename from mcsolver/mcsolver_types.ml rename to solver/mcsolver_types.ml index 46d14b02..f6013de4 100644 --- a/mcsolver/mcsolver_types.ml +++ b/solver/mcsolver_types.ml @@ -65,30 +65,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct | History of clause list | Lemma of proof - type elt = - | Term of semantic var - | Formula of boolean var - - (* Accessors for variables *) - let get_elt_id = function - | Term v -> v.vid - | Formula v -> v.vid - - let get_elt_weight = function - | Term v -> v.weight - | Formula v -> v.weight - - let get_elt_level = function - | Term v -> v.level - | Formula v -> v.level - - let set_elt_weight e w = match e with - | Term v -> v.weight <- w - | Formula v -> v.weight <- w - - let set_elt_level e l = match e with - | Term v -> v.level <- l - | Formula v -> v.level <- l + type elt = (semantic var, boolean var) Either.t (* Dummy values *) let dummy_lit = E.dummy @@ -100,7 +77,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct tag = { pa = dummy_atom; na = dummy_atom; - reason = None; + reason = Bcp None; seen = false; vpremise = History []; }; } @@ -131,7 +108,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct let f_map = ref MF.empty let t_map = ref MT.empty - let vars = Vec.make 107 (Formula dummy_var) + let vars = Vec.make 107 (Either.mk_right dummy_var) let nb_vars () = Vec.size vars let get_var i = Vec.get vars i let iter_vars f = Vec.iter f vars @@ -171,7 +148,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in f_map := MF.add lit var !f_map; incr cpt_mk_var; - Vec.push vars (Formula var); + Vec.push vars (Either.mk_right var); var, negated let make_semantic_var t = @@ -187,7 +164,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct } in incr cpt_mk_var; t_map := MT.add t res !t_map; - Vec.push vars (Term res); + Vec.push vars (Either.mk_left res); res let add_term t = make_semantic_var t @@ -221,6 +198,8 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct fun () -> incr cpt; "C" ^ (string_of_int !cpt) (* Pretty printing for atoms and clauses *) + let print_semantic_var fmt v = E.Term.print fmt v.tag.term + let print_atom fmt a = E.Formula.print fmt a.lit let print_atoms fmt v = @@ -255,6 +234,14 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v | Lemma _ -> bprintf b "th_lemma" + let pp_assign b = function + | None -> () + | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t) + + let pp_semantic_var b v = + bprintf b "%d [lit:%s]%a" + (v.vid+1) (Log.on_fmt E.Term.print v.tag.term) pp_assign v.tag.assigned + let pp_atom b a = bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) diff --git a/mcsolver/mcsolver_types.mli b/solver/mcsolver_types.mli similarity index 92% rename from mcsolver/mcsolver_types.mli rename to solver/mcsolver_types.mli index 42cfda42..981053df 100644 --- a/mcsolver/mcsolver_types.mli +++ b/solver/mcsolver_types.mli @@ -14,5 +14,5 @@ module type S = Mcsolver_types_intf.S module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S) - -> S with type term= E.Term.t and type formula = E.Formula.t and type proof = Th.proof + -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) diff --git a/mcsolver/mcsolver_types_intf.ml b/solver/mcsolver_types_intf.ml similarity index 94% rename from mcsolver/mcsolver_types_intf.ml rename to solver/mcsolver_types_intf.ml index c7bc10f9..ae7213ee 100644 --- a/mcsolver/mcsolver_types_intf.ml +++ b/solver/mcsolver_types_intf.ml @@ -18,7 +18,6 @@ module type S = sig type formula type proof - type 'a var = { vid : int; tag : 'a; @@ -62,9 +61,7 @@ module type S = sig | History of clause list | Lemma of proof - type elt = - | Term of semantic var - | Formula of boolean var + type elt = (semantic var, boolean var) Either.t (** Recursive types for literals (atoms) and clauses *) val dummy_var : boolean var @@ -96,10 +93,12 @@ module type S = sig (** Fresh names for clauses *) val print_atom : Format.formatter -> atom -> unit + val print_semantic_var : Format.formatter -> semantic var -> unit val print_clause : Format.formatter -> clause -> unit (** Pretty printing functions for atoms and clauses *) val pp_atom : Buffer.t -> atom -> unit + val pp_semantic_var : Buffer.t -> semantic var -> unit val pp_clause : Buffer.t -> clause -> unit (** Debug function for atoms and clauses (very verbose) *) diff --git a/mcsolver/plugin_intf.ml b/solver/plugin_intf.ml similarity index 99% rename from mcsolver/plugin_intf.ml rename to solver/plugin_intf.ml index 6c267d6b..65683755 100644 --- a/mcsolver/plugin_intf.ml +++ b/solver/plugin_intf.ml @@ -50,7 +50,7 @@ module type S = sig | Unsat of formula list * proof type eval_res = - | Bool of bool + | Valued of bool * int | Unknown val dummy : level diff --git a/solver/res.ml b/solver/res.ml index 4933e70f..7332dbd0 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -45,6 +45,8 @@ module Make(St : Solver_types.S) = struct let equal_atoms a b = St.(a.aid) = St.(b.aid) let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) + let merge = List.merge compare_atoms + let _c = ref 0 let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c) @@ -123,7 +125,7 @@ module Make(St : Solver_types.S) = struct Log.debug 7 " %a" St.pp_clause d; assert (is_proved (c, cl_c)); assert (is_proved (d, cl_d)); - let l = List.merge compare_atoms cl_c cl_d in + let l = merge cl_c cl_d in let resolved, new_clause = resolve l in match resolved with | [] -> raise (Resolution_error "No literal to resolve over") diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 49ff532c..58332393 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -1,24 +1,18 @@ (* Copyright 2014 Guillaume Bury *) module type S = sig - (** Sinature for a module handling proof by resolution from sat solving traces *) + (** Signature for a module handling proof by resolution from sat solving traces *) + + (** {3 Type declarations} *) + + exception Insuficient_hyps + (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) type atom type clause type lemma (** Abstract types for atoms, clauses and theoriy-specific lemmas *) - val is_proven : clause -> bool - (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *) - - exception Insuficient_hyps - val learn : clause Vec.t -> unit - (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *) - - val assert_can_prove_unsat : clause -> unit - (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved. - @raise Insuficient_hyps if it is impossible. *) - type proof_node = { conclusion : clause; step : step; @@ -28,6 +22,31 @@ module type S = sig | Hypothesis | Lemma of lemma | Resolution of proof * proof * atom + (** Lazy type for proof trees. *) + + (** {3 Resolution helpers} *) + val to_list : clause -> atom list + (** Returns the sorted list of atoms of a clause. *) + + val merge : atom list -> atom list -> atom list + (** Merge two sorted atom list using a suitable comparison function. *) + + val resolve : atom list -> atom list * atom list + (** Performs a "resolution step" on a sorted list of atoms. + [resolve (List.merge l1 l2)] where [l1] and [l2] are sorted atom lists should return the pair + [\[a\], l'], where [l'] is the result of the resolution of [l1] and [l2] over [a]. *) + + (** {3 Proof building functions} *) + + val is_proven : clause -> bool + (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *) + + val learn : clause Vec.t -> unit + (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *) + + val assert_can_prove_unsat : clause -> unit + (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved. + @raise Insuficient_hyps if it is impossible. *) val prove_unsat : clause -> proof (** Given a conflict clause [c], returns a proof of the empty clause. Same as [assert_can_prove_unsat] but returns diff --git a/util/either.ml b/util/either.ml new file mode 100644 index 00000000..ba1eb9bc --- /dev/null +++ b/util/either.ml @@ -0,0 +1,11 @@ + +type ('a, 'b) t = + | Left of 'a + | Right of 'b + +let mk_left a = Left a +let mk_right b = Right b + +let destruct e f_left f_right = match e with + | Left a -> f_left a + | Right b -> f_right b diff --git a/util/either.mli b/util/either.mli new file mode 100644 index 00000000..2e2a8ba8 --- /dev/null +++ b/util/either.mli @@ -0,0 +1,11 @@ + + +type ('a, 'b) t = + | Left of 'a + | Right of 'b + +val mk_left : 'a -> ('a, 'b) t +val mk_right : 'b -> ('a, 'b) t + +val destruct : ('a, 'b) t -> + ('a -> 'c) -> ('b -> 'c) -> 'c