From e2d4f4fdc519f51f2b2b92bae52f909304cd8fe0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 12 Nov 2014 17:29:11 +0100 Subject: [PATCH] Added theory lemma as possible premise for clauses --- sat/res.ml | 19 ++++---- sat/res.mli | 4 +- sat/solver.ml | 100 +++++++-------------------------------- sat/solver_types.ml | 20 ++++---- sat/solver_types.mli | 3 +- sat/solver_types_intf.ml | 6 ++- 6 files changed, 49 insertions(+), 103 deletions(-) diff --git a/sat/res.ml b/sat/res.ml index 159cd731..6d009487 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -6,10 +6,10 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make(St : Solver_types.S)(Proof : sig type proof end) = struct +module Make(St : Solver_types.S) = struct (* Type definitions *) - type lemma = Proof.proof + type lemma = St.proof type clause = St.clause type atom = St.atom type int_cl = clause * St.atom list @@ -86,11 +86,11 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct (* Adding hyptoheses *) let is_unit_hyp = function - | [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> []) + | [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> History []) | _ -> false let make_unit_hyp a = - let aux a = St.(make_clause (fresh_name ()) [a] 1 false []) in + 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 @@ -114,8 +114,9 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct else if is_unit_hyp cl || not St.(c.learnt) then begin H.add proof cl Assumption; true - end else - false + 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) @@ -131,7 +132,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct | [] -> 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 [c; d] in + 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") @@ -177,7 +178,9 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct if is_proved (c, cl) then [] else - St.(c.cpremise) + match St.(c.cpremise) with + | St.History l -> l + | St.Lemma _ -> assert false let rec do_clause = function | [] -> () diff --git a/sat/res.mli b/sat/res.mli index 6b783978..8d20af96 100644 --- a/sat/res.mli +++ b/sat/res.mli @@ -6,6 +6,6 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (St : Solver_types.S)(Proof : sig type proof end) - -> S with type atom= St.atom and type clause = St.clause and type lemma = Proof.proof +module Make : functor (St : Solver_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/sat/solver.ml b/sat/solver.ml index a06a21a5..522a0c18 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -13,8 +13,8 @@ module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t) = struct - module St = Solver_types.Make(F) - module Proof = Res.Make(St)(Th) + module St = Solver_types.Make(F)(Th) + module Proof = Res.Make(St) open St @@ -245,7 +245,7 @@ module Make (F : Formula_intf.S) a.neg.is_true <- false; a.var.level <- -1; a.var.reason <- None; - a.var.vpremise <- []; + a.var.vpremise <- History []; insert_var_order a.var done; Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) @@ -356,8 +356,8 @@ module Make (F : Formula_intf.S) let slice_get i = (Vec.get env.trail i).lit let slice_push lit l lemma = let atoms = List.rev_map add_atom (lit :: (List.rev_map F.neg l)) in - let c = St.make_clause (St.fresh_name ()) atoms (List.length atoms) true [] in - enqueue (St.add_atom lit) (decision_level ()) (Some c) + let c = make_clause (fresh_name ()) atoms (List.length atoms) true (Lemma lemma) in + enqueue (add_atom lit) (decision_level ()) (Some c) let current_slice () = Th.({ start = env.tatoms_qhead; @@ -373,7 +373,7 @@ module Make (F : Formula_intf.S) propagate () | Th.Unsat (l, p) -> let l = List.rev_map St.add_atom l in - let c = St.make_clause (St.fresh_name ()) l (List.length l) true [] in + let c = St.make_clause (St.fresh_name ()) l (List.length l) true (History []) in Some c and propagate () = @@ -544,81 +544,12 @@ module Make (F : Formula_intf.S) var_decay_activity (); clause_decay_activity () - - (* - let theory_analyze dep = 0, [], [], 1 - let atoms, sz, max_lvl, c_hist = - Ex.fold_atoms - (fun a (acc, sz, max_lvl, c_hist) -> - let c_hist = List.rev_append a.var.vpremise c_hist in - let c_hist = match a.var.reason with - | None -> c_hist | Some r -> r:: c_hist in - if a.var.level = 0 then acc, sz, max_lvl, c_hist - else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist - ) dep ([], 0, 0, []) - in - if atoms = [] then begin - (* check_inconsistency_of dep; *) - report_t_unsat dep - (* une conjonction de faits unitaires etaient deja unsat *) - end; - let name = fresh_dname() in - let c_clause = make_clause name atoms sz false c_hist in - (* eprintf "c_clause: %a@." Debug.clause c_clause; *) - c_clause.removed <- true; - - 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 history = ref [] in - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.seen <- true; - seen := q :: !seen; - if q.var.level >= max_lvl then incr pathC - else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level - end - end - done; - - (* look for the next node to expand *) - while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; - decr pathC; - let p = Vec.get env.trail !tr_ind in - decr tr_ind; - match !pathC, p.var.reason with - | 0, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl - done; - List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size - *) - 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 cancel_until blevel; - record_learnt_clause blevel learnt history size + record_learnt_clause blevel learnt (History history) size let search n_of_conflicts n_of_learnts = let conflictC = ref 0 in @@ -700,9 +631,11 @@ module Make (F : Formula_intf.S) if a.var.level = 0 then raise Trivial else (a::trues) @ unassigned @ falses @ r, init else if a.neg.is_true then - if a.var.level = 0 then + if a.var.level = 0 then match a.var.vpremise with + | History v -> partition_aux trues unassigned falses - (List.rev_append (a.var.vpremise) init) r + (List.rev_append v init) r + | Lemma _ -> assert false else partition_aux trues unassigned (a::falses) init r else partition_aux trues (a::unassigned) falses init r in @@ -712,15 +645,16 @@ module Make (F : Formula_intf.S) let add_clause ~cnumber atoms = if env.is_unsat then raise Unsat; let init_name = string_of_int cnumber in - let init0 = make_clause init_name atoms (List.length atoms) false [] in + let init0 = make_clause init_name atoms (List.length atoms) false (History []) in try let atoms, init = if decision_level () = 0 then let atoms, init = List.fold_left (fun (atoms, init) a -> if a.is_true then raise Trivial; - if a.neg.is_true then - atoms, (List.rev_append (a.var.vpremise) init) + if a.neg.is_true then match a.var.vpremise with + | History v -> atoms, (List.rev_append v init) + | Lemma p -> assert false else a::atoms, init ) ([], [init0]) atoms in List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init @@ -733,7 +667,7 @@ module Make (F : Formula_intf.S) | a::_::_ -> let name = fresh_name () in - let clause = make_clause name atoms size false init in + let clause = make_clause name atoms size false (History init) in attach_clause clause; Vec.push env.clauses clause; if a.neg.is_true then begin @@ -744,7 +678,7 @@ module Make (F : Formula_intf.S) | [a] -> cancel_until 0; - a.var.vpremise <- init; + a.var.vpremise <- History init; enqueue a 0 None; match propagate () with None -> () | Some confl -> report_unsat confl diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 2eba53b9..a415aca5 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -15,9 +15,10 @@ open Printf module type S = Solver_types_intf.S -module Make (F : Formula_intf.S) = struct +module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct type formula = F.t + type proof = Th.proof type var = { vid : int; @@ -47,7 +48,9 @@ module Make (F : Formula_intf.S) = struct and reason = clause option - and premise = clause list + and premise = + | History of clause list + | Lemma of proof let dummy_lit = F.dummy @@ -59,7 +62,7 @@ module Make (F : Formula_intf.S) = struct reason = None; weight = -1.; seen = false; - vpremise = [] } + vpremise = History [] } and dummy_atom = { var = dummy_var; lit = dummy_lit; @@ -76,7 +79,7 @@ module Make (F : Formula_intf.S) = struct activity = -1.; removed = false; learnt = false; - cpremise = [] } + cpremise = History [] } let () = dummy_atom.watched <- Vec.make_empty dummy_clause @@ -102,7 +105,7 @@ module Make (F : Formula_intf.S) = struct reason = None; weight = 0.; seen = false; - vpremise = []; + vpremise = History []; } and pa = { var = var; @@ -140,7 +143,7 @@ module Make (F : Formula_intf.S) = struct activity = 0.; cpremise = premise} - let empty_clause = make_clause "Empty" [] 0 false [] + let empty_clause = make_clause "Empty" [] 0 false (History []) let fresh_lname = let cpt = ref 0 in @@ -188,8 +191,9 @@ module Make (F : Formula_intf.S) = struct else if a.neg.is_true then sprintf "[F%s]" (level a) else "" - let pp_premise b v = - List.iter (fun {name=name} -> bprintf b "%s," name) v + let pp_premise b = function + | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v + | Lemma _ -> bprintf b "th_lemma" let pp_atom b a = bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" diff --git a/sat/solver_types.mli b/sat/solver_types.mli index 36950bd7..ecc41d8b 100644 --- a/sat/solver_types.mli +++ b/sat/solver_types.mli @@ -13,5 +13,6 @@ module type S = Solver_types_intf.S -module Make : functor (F : Formula_intf.S) -> S with type formula = F.t +module Make : functor (F : Formula_intf.S)(Th : Theory_intf.S) + -> S with type formula = F.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index e0bcdca2..1a59ad4d 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -15,6 +15,8 @@ module type S = sig (** The signatures of clauses used in the Solver. *) type formula + type proof + type varmap val ma : varmap ref @@ -48,7 +50,9 @@ module type S = sig } and reason = clause option - and premise = clause list + and premise = + | History of clause list + | Lemma of proof (** Recursive types for literals (atoms) and clauses *) val dummy_var : var