From 245941efdb87306f7f5d0b9cd48bcf1e5fa93a49 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 13 Jul 2016 16:23:34 +0200 Subject: [PATCH] Remember more added clauses --- _tags | 1 - solver/internal.ml | 91 ++++++++++++++++++++----------------- solver/solver_types.ml | 6 +-- solver/solver_types_intf.ml | 2 +- 4 files changed, 54 insertions(+), 46 deletions(-) diff --git a/_tags b/_tags index 2ea41d17..4a5fd955 100644 --- a/_tags +++ b/_tags @@ -1,5 +1,4 @@ : for-pack(Msat) -#: : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) diff --git a/solver/internal.ml b/solver/internal.ml index 8dc7fa79..aa6a6681 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -351,24 +351,29 @@ module Make (* Adding/removing clauses *) let attach_clause c = - 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 + if not c.attached then begin + 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 = - Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c); - c.removed <- true; - (* 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 + 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 + end let remove_clause c = detach_clause c @@ -413,13 +418,16 @@ module Make let simpl_reason = function | (Bcp cl) as r -> - let l, history = partition (Vec.to_list cl.atoms) in + Log.debugf 90 "Simplifying reason: %a" (fun k -> k St.pp_clause cl); + let atoms = Vec.to_list cl.atoms in + let l, history = partition atoms in begin match l with | [ a ] -> if history = [] then r - else + else begin let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in Bcp tmp_cl + end | _ -> assert false end | r -> r @@ -605,7 +613,7 @@ module Make clause_bump_activity lclause; if is_uip then enqueue_bool fuip blevel (Bcp lclause) - else begin + else begin env.next_decision <- Some fuip.neg end end; @@ -622,28 +630,28 @@ module Make record_learnt_clause confl blevel learnt (History history) is_uip (* Add a new clause *) - let add_clause ?(force=false) init0 = - Log.debugf 90 "Adding clause:@[%a@]" (fun k -> k St.pp_clause init0); - let vec = match init0.cpremise with - | Lemma _ -> env.clauses_learnt + let add_clause ?(force=false) init = + Log.debugf 90 "Adding clause:@[%a@]" (fun k -> k St.pp_clause init); + let vec = match init.cpremise with + | Lemma _ -> env.clauses_theory | History [] -> env.clauses_hyps | History _ -> assert false in try - let atoms, history = partition (Vec.to_list init0.atoms) in + let atoms, history = partition (Vec.to_list init.atoms) in let size = List.length atoms in + let clause = + if history = [] then init + else make_clause ?tag:init.tag (fresh_name ()) + atoms size true (History (init :: history)) + in + Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); + Vec.push vec clause; match atoms with | [] -> - Log.debugf 1 "New clause (unsat) :@ @[%a@]" (fun k->k St.pp_clause init0); - report_unsat init0 + report_unsat clause | a::b::_ -> - let clause = - if history = [] then init0 - else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history)) - in - Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); attach_clause clause; - Vec.push vec 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; @@ -656,9 +664,10 @@ module Make | [a] -> Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a); cancel_until 0; - enqueue_bool a 0 (Bcp init0) + enqueue_bool a 0 (Bcp clause) with Trivial -> - Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0) + Vec.push vec init; + Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init) let propagate_in_clause a c i watched new_sz = let atoms = c.atoms in @@ -709,7 +718,7 @@ module Make try for i = 0 to Vec.size watched - 1 do let c = Vec.get watched i in - if not c.removed then propagate_in_clause a c i watched new_sz_w + if c.attached then propagate_in_clause a c i watched new_sz_w done; with Conflict c -> assert (!res = None); @@ -786,10 +795,10 @@ module Make let res = ref None in while env.elt_head < Vec.size env.elt_queue do begin match Vec.get env.elt_queue env.elt_head with - | Either.Left _ -> () - | Either.Right a -> - incr num_props; - propagate_atom a res + | Either.Left _ -> () + | Either.Right a -> + incr num_props; + propagate_atom a res end; env.elt_head <- env.elt_head + 1; done; @@ -958,8 +967,8 @@ module Make 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. - match propagate () with - | None -> () | Some confl -> report_unsat confl + match propagate () with + | None -> () | Some confl -> report_unsat confl *) in List.iter aux cnf diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 34baa3ba..01e39816 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -62,7 +62,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct c_level : int; mutable cpremise : premise; mutable activity : float; - mutable removed : bool; + mutable attached : bool; } and reason = @@ -102,7 +102,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct tag = None; atoms = Vec.make_empty dummy_atom; activity = -1.; - removed = false; + attached = false; c_level = -1; learnt = false; cpremise = History [] } @@ -191,7 +191,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct { name = name; tag = tag; atoms = atoms; - removed = false; + attached = false; learnt = is_learnt; c_level = level; activity = 0.; diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index a09ce96b..b755fb8c 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -57,7 +57,7 @@ module type S = sig c_level : int; mutable cpremise : premise; mutable activity : float; - mutable removed : bool; + mutable attached : bool; } and reason =