From f5f9a4ab69fa6390cbbeafeec9539c0fd96f8059 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 31 Mar 2017 15:05:53 +0200 Subject: [PATCH] Extend the 'seen' field to store more information --- src/core/internal.ml | 24 +++++++++++++++-------- src/core/solver_types.ml | 36 ++++++++++++++++++++++++++++++++--- src/core/solver_types_intf.ml | 19 +++++++++++++++++- 3 files changed, 67 insertions(+), 12 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index ef91c71d..e18b2f5e 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -320,14 +320,22 @@ module Make (* Eliminates atom doublons in clauses *) let eliminate_doublons clause : clause = + let trivial = ref false in let duplicates = ref [] in let res = ref [] in Array.iter (fun a -> - if a.var.seen then duplicates := a :: !duplicates - else (a.var.seen <- true; res := a :: !res) + if seen a then duplicates := a :: !duplicates + else (mark a; res := a :: !res) ) clause.atoms; - List.iter (fun a -> a.var.seen <- false) !res; - if !duplicates = [] then + List.iter (fun a -> + begin match a.var.seen with + | Both -> trivial := true + | _ -> () + end; + clear a.var) !res; + if !trivial then + raise Trivial + else if !duplicates = [] then clause else make_clause (fresh_lname ()) !res (History [clause]) @@ -632,8 +640,8 @@ module Make | Some Bcp cl -> history := cl :: !history | _ -> assert false end; - if not q.var.seen then begin - q.var.seen <- true; + if not (q.var.seen = Both) then begin + q.var.seen <- Both; seen := q :: !seen; if q.var.v_level > 0 then begin var_bump_activity q.var; @@ -650,7 +658,7 @@ module Make (* look for the next node to expand *) while let q = get_atom !tr_ind in - (not q.var.seen) || + (not (q.var.seen = Both)) || (q.var.v_level < conflict_level) do decr tr_ind; @@ -671,7 +679,7 @@ module Make c := cl | n, _ -> assert false done; - List.iter (fun q -> q.var.seen <- false) !seen; + List.iter (fun q -> clear q.var) !seen; let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in let level, is_uip = backtrack_lvl l in { cr_backtrack_lvl = level; diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 63dfc0b6..6055b05a 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -30,6 +30,12 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct type formula = E.Formula.t type proof = E.proof + type seen = + | Nope + | Both + | Positive + | Negative + type lit = { lid : int; term : term; @@ -43,7 +49,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct pa : atom; na : atom; mutable used : int; - mutable seen : bool; + mutable seen : seen; mutable v_level : int; mutable v_weight : float; mutable v_assignable: lit list option; @@ -92,7 +98,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct pa = dummy_atom; na = dummy_atom; used = 0; - seen = false; + seen = Nope; v_level = -1; v_weight = -1.; v_assignable = None; @@ -160,7 +166,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct pa = pa; na = na; used = 0; - seen = false; + seen = Nope; v_level = -1; v_weight = 0.; v_assignable = None; @@ -205,6 +211,30 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let empty_clause = make_clause "Empty" [] (History []) + (* Marking helpers *) + let clear v = v.seen <- Nope + + let seen a = + let pos = (a == a.var.pa) in + match a.var.seen, pos with + | Nope, _ -> false + | Both, _ + | Positive, true + | Negative, false -> true + | Positive, false + | Negative, true -> false + + let mark a = + let pos = (a == a.var.pa) in + match a.var.seen with + | Both -> () + | Nope -> + a.var.seen <- (if pos then Positive else Negative) + | Positive -> + if pos then () else a.var.seen <- Both + | Negative -> + if pos then a.var.seen <- Both else () + (* Decisions & propagations *) type t = | Lit of lit diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 059f70fb..0dbebffd 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -35,6 +35,12 @@ module type S = sig type proof (** The types of terms, formulas and proofs. All of these are user-provided. *) + type seen = + | Nope + | Both + | Positive + | Negative + type lit = { lid : int; (** Unique identifier *) term : term; (** Wrapped term *) @@ -49,7 +55,7 @@ module type S = sig pa : atom; (** Link for the positive atom *) na : atom; (** Link for the negative atom *) mutable used : int; (** Number of attached clause that contain the var *) - mutable seen : bool; (** Boolean used during propagation *) + mutable seen : seen; (** Boolean used during propagation *) mutable v_level : int; (** Level of decision/propagation *) mutable v_weight : float; (** Variable weight (for the heap) *) mutable v_assignable: lit list option; @@ -163,6 +169,17 @@ module type S = sig val make_clause : ?tag:int -> string -> atom list -> premise -> clause (** [make_clause name atoms size premise] creates a clause with the given attributes. *) + + (** {2 Helpers} *) + + val mark : atom -> unit + (** Mark the atom as seen, using the 'seen' field in the variable. *) + val seen : atom -> bool + (** Returns wether the atom has been marked as seen. *) + val clear : var -> unit + (** Clear the 'seen' field of the variable. *) + + (** {2 Clause names} *) val fresh_name : unit -> string