diff --git a/solver/internal.ml b/solver/internal.ml index 8a79bea4..716581b6 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -304,7 +304,8 @@ module Make let partition atoms = (* Parittion litterals for new clauses *) let rec partition_aux trues unassigned falses history = function - | [] -> trues @ unassigned @ falses, history + | [] -> + trues @ unassigned @ falses, history | a :: r -> if a.is_true then if a.var.v_level = 0 then raise Trivial @@ -352,27 +353,18 @@ module Make (* Adding/removing clauses *) let attach_clause c = if not c.attached then begin + Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c); c.attached <- true; Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c; - if c.learnt then - env.learnts_literals <- env.learnts_literals + Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals + Vec.size c.atoms end let detach_clause c = if c.attached then begin c.attached <- false; Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c); - (* Not necessary, cleanup is done during propagation - Vec.remove (Vec.get c.atoms 0).neg.watched c; - Vec.remove (Vec.get c.atoms 1).neg.watched c; - *) - if c.learnt then - env.learnts_literals <- env.learnts_literals - Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals - Vec.size c.atoms + Vec.remove (Vec.get c.atoms 0).neg.watched c; + Vec.remove (Vec.get c.atoms 1).neg.watched c; end let remove_clause c = detach_clause c @@ -383,6 +375,7 @@ module Make (* cancel down to [lvl] excluded *) let cancel_until lvl = if decision_level () > lvl then begin + Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl); env.elt_head <- Vec.get env.elt_levels lvl; env.th_head <- env.elt_head; for c = env.elt_head to Vec.size env.elt_queue - 1 do @@ -424,10 +417,8 @@ module Make begin match l with | [ a ] -> if history = [] then r - else begin - let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in - Bcp tmp_cl - end + else + Bcp (make_clause (fresh_tname ()) l 1 (History (cl :: history))) | _ -> assert false end | r -> r @@ -522,7 +513,8 @@ module Make end done; assert false with Exit -> - let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in + let learnt = List.fast_sort ( + fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in let blevel = backtrack_lvl !is_uip learnt in blevel, learnt, List.rev !history, !is_uip @@ -542,7 +534,10 @@ module Make let history = ref [] in assert (decision_level () > 0); while !cond do - if !c.learnt then clause_bump_activity !c; + begin match !c.cpremise with + | History _ -> clause_bump_activity !c + | Hyp _ | Lemma _ -> () + end; history := !c :: !history; (* visit the current predecessors *) for j = 0 to Vec.size !c.atoms - 1 do @@ -601,13 +596,13 @@ module Make report_unsat confl else begin let name = fresh_lname () in - let uclause = make_clause name learnt (List.length learnt) true history in + let uclause = make_clause name learnt (List.length learnt) history in Vec.push env.clauses_learnt uclause; enqueue_bool fuip 0 (Bcp uclause) end | fuip :: _ -> let name = fresh_lname () in - let lclause = make_clause name learnt (List.length learnt) true history in + let lclause = make_clause name learnt (List.length learnt) history in Vec.push env.clauses_learnt lclause; attach_clause lclause; clause_bump_activity lclause; @@ -643,7 +638,7 @@ module Make let clause = if history = [] then init else make_clause ?tag:init.tag (fresh_name ()) - atoms size true (History (init :: history)) + atoms size (History (init :: history)) in Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); Vec.push vec clause; @@ -651,15 +646,18 @@ module Make | [] -> report_unsat clause | a::b::_ -> - attach_clause clause; if a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in - cancel_until lvl; - add_boolean_conflict clause - end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in - cancel_until lvl; - enqueue_bool a lvl (Bcp clause) + Vec.sort clause.atoms (fun a b -> + compare b.var.v_level a.var.v_level); + attach_clause clause; + add_boolean_conflict init + end else begin + attach_clause clause; + if b.neg.is_true && not a.is_true && not a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in + cancel_until lvl; + enqueue_bool a lvl (Bcp clause) + end end | [a] -> Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); @@ -681,8 +679,7 @@ module Make (* true clause, keep it in watched *) Vec.set watched !new_sz c; incr new_sz; - end - else + end else try (* look for another watch lit *) for k = 2 to Vec.size atoms - 1 do let ak = Vec.get atoms k in @@ -743,7 +740,7 @@ module Make let atoms = List.rev_map (fun x -> new_atom x) l in Iheap.grow_to_by_double env.order (St.nb_elt ()); List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms; - let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) in + let c = make_clause (fresh_tname ()) atoms (List.length atoms) (Lemma lemma) in add_clause c let slice_propagate f lvl = @@ -781,7 +778,7 @@ module Make let l = List.rev_map new_atom l in Iheap.grow_to_by_double env.order (St.nb_elt ()); List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; - let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in + let c = St.make_clause (St.fresh_tname ()) l (List.length l) (Lemma p) in Some c end @@ -963,7 +960,7 @@ module Make let add_clauses ?tag cnf = let aux cl = let c = make_clause ?tag (fresh_hname ()) - cl (List.length cl) false (Hyp (current_level ())) in + cl (List.length cl) (Hyp (current_level ())) in add_clause c; (* Clauses can be added after search has begun (and thus we are not at level 0, so better not do anything at this point. diff --git a/solver/res.ml b/solver/res.ml index 2195ef0d..b74a0cc9 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -83,7 +83,7 @@ module Make(St : Solver_types.S) = struct cmp_cl (to_list c) (to_list d) let prove conclusion = - assert St.(conclusion.learnt || conclusion.cpremise <> History []); + assert St.(conclusion.cpremise <> History []); conclusion let prove_unsat c = @@ -93,7 +93,7 @@ module Make(St : Solver_types.S) = struct | Some St.Bcp d -> d | _ -> assert false) l in - St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l)) + St.make_clause (fresh_pcl_name ()) [] 0 (St.History (c :: l)) let prove_atom a = if St.(a.is_true && a.var.v_level = 0) then begin @@ -126,8 +126,8 @@ module Make(St : Solver_types.S) = struct begin match r with | [] -> (l, c, d, a) | _ -> - let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true - (St.History [c; d]) in + let new_clause = St.make_clause (fresh_pcl_name ()) + l (List.length l) (St.History [c; d]) in chain_res (new_clause, l) r end | _ -> assert false @@ -140,7 +140,6 @@ module Make(St : Solver_types.S) = struct | St.Lemma l -> {conclusion; step = Lemma l; } | St.Hyp _ -> - assert (not conclusion.St.learnt); { conclusion; step = Hypothesis; } | St.History [] -> assert false diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 524d08f6..76894b3a 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -58,7 +58,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct name : string; tag : int option; atoms : atom Vec.t; - learnt : bool; c_level : int; mutable cpremise : premise; mutable activity : float; @@ -106,7 +105,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct activity = -1.; attached = false; c_level = -1; - learnt = false; visited = false; cpremise = History [] } @@ -182,7 +180,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let var, negated = make_boolean_var lit in if negated then var.na else var.pa - let make_clause ?tag name ali sz_ali is_learnt premise = + let make_clause ?tag name ali sz_ali premise = let atoms = Vec.from_list ali sz_ali dummy_atom in let level = match premise with @@ -195,12 +193,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct atoms = atoms; attached = false; visited = false; - learnt = is_learnt; c_level = level; activity = 0.; cpremise = premise} - let empty_clause = make_clause "Empty" [] 0 false (History []) + let empty_clause = make_clause "Empty" [] 0 (History []) (* Decisions & propagations *) type t = (lit, atom) Either.t @@ -298,9 +295,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let pp_atoms_vec out vec = Vec.print ~sep:"" pp_atom out vec - let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} = - Format.fprintf out "%s%s@[{@[%a@]}@ cpremise={@[%a@]}@]" - name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp + let pp_clause out {name=name; atoms=arr; cpremise=cp; } = + Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" + name pp_atoms_vec arr pp_premise cp end diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 740ee05d..619558f4 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -53,7 +53,6 @@ module type S = sig name : string; tag : int option; atoms : atom Vec.t; - learnt : bool; c_level : int; mutable cpremise : premise; mutable activity : float; @@ -117,7 +116,7 @@ module type S = sig val empty_clause : clause (** The empty clause *) - val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause + val make_clause : ?tag:int -> string -> atom list -> int -> premise -> clause (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) (** {2 Clause names} *)