Merge branch '0.3.1'

_tags

@@ -1,8 +1,8 @@
 # colors
-true: color(always)
+true: bin_annot, color(always)
 
 # optimization options
-true: optimize(3), bin_annot, unbox_closures, unbox_closures_factor(20)
+true: optimize(3), unbox_closures, unbox_closures_factor(20)
 
 # Include paths
 <src>: include

src/core/internal.ml

@@ -411,21 +411,20 @@ module Make
      their watchers, while clauses that loose their satisfied status
      have to be reattached, adding watchers. *)
   let attach_clause c =
-    Vec.push (Vec.get c.atoms 0).neg.watched c;
+    if not c.attached then begin
-    Vec.push (Vec.get c.atoms 1).neg.watched c;
+      Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c);
-    (* TODO: Learnt litterals are not really used anymre, :p *)
+      c.attached <- true;
-    if c.learnt then
+      Vec.push (Vec.get c.atoms 0).neg.watched c;
-      env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
+      Vec.push (Vec.get c.atoms 1).neg.watched c;
-    else
+    end
-      env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
 
   let detach_clause c =
-    Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
+    if c.attached then begin
-    c.removed <- true;
+      c.attached <- false;
-    if c.learnt then
+      Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
-      env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
+      Vec.remove (Vec.get c.atoms 0).neg.watched c;
-    else
+      Vec.remove (Vec.get c.atoms 1).neg.watched c;
-      env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
+    end
 
   (* Is a clause satisfied ? *)
   let satisfied c = Vec.exists (fun atom -> atom.is_true) c.atoms
@@ -437,6 +436,7 @@ module Make
   let cancel_until lvl =
     (* Nothing to do if we try to backtrack to a non-existent level. *)
     if decision_level () > lvl then begin
+      Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl);
       (* We set the head of the solver and theory queue to what it was. *)
       env.elt_head <- Vec.get env.elt_levels lvl;
       env.th_head <- env.elt_head;
@@ -494,7 +494,8 @@ module Make
      be able to build a correct proof at the end of proof search. *)
   let simpl_reason = function
     | (Bcp cl) as r ->
-      let l, history = partition (Vec.to_list cl.atoms) in
+      let atoms = Vec.to_list cl.atoms in
+      let l, history = partition atoms in
       begin match l with
         | [ a ] ->
           if history = [] then r
@@ -505,8 +506,7 @@ module Make
                with only one formula (which is [a]). So we explicitly create that clause
                and set it as the cause for the propagation of [a], that way we can
                rebuild the whole resolution tree when we want to prove [a]. *)
-            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in
+            Bcp (make_clause (fresh_tname ()) l 1 (History (cl :: history)))
-            Bcp tmp_cl
         | _ -> assert false
       end
     | r -> r
@@ -603,7 +603,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
 
@@ -623,7 +624,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
@@ -682,13 +686,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;
@@ -711,43 +715,47 @@ module Make
     record_learnt_clause confl blevel learnt (History history) is_uip
 
   (* Add a new clause *)
-  let add_clause ?(force=false) init0 =
+  let add_clause ?(force=false) init =
-    Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init0);
+    Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init);
-    let vec = match init0.cpremise with
+    let vec = match init.cpremise with
+      | Hyp _ -> env.clauses_hyps
       | Lemma _ -> env.clauses_learnt
-      | 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 (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 clause
-        report_unsat init0
       | 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
+          Vec.sort clause.atoms (fun a b ->
-          cancel_until lvl;
+              compare b.var.v_level a.var.v_level);
-          add_boolean_conflict clause
+          attach_clause clause;
-        end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
+          add_boolean_conflict init
-          let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
+        end else begin
-          cancel_until lvl;
+          attach_clause clause;
-          enqueue_bool a lvl (Bcp 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);
         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
@@ -761,8 +769,7 @@ module Make
       (* true clause, keep it in watched *)
       Vec.set watched !new_sz c;
       incr new_sz;
-    end
+    end else
-    else
       try (* look for another watch lit *)
         for k = 2 to Vec.size atoms - 1 do
           let ak = Vec.get atoms k in
@@ -798,7 +805,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);
@@ -825,7 +832,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
     Log.debugf 10 "Pushing clause %a" (fun k->k St.pp_clause c);
     Stack.push c env.clauses_pushed
 
@@ -864,7 +871,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
 
@@ -1050,8 +1057,8 @@ module Make
 
   let add_clauses ?tag cnf =
     let aux cl =
-      let c = make_clause ?tag ~lvl:(current_level ())
+      let c = make_clause ?tag (fresh_hname ())
-          (fresh_hname ()) cl (List.length cl) false (History []) 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.
@@ -1215,6 +1222,7 @@ module Make
         if c.c_level > l then begin
           detach_clause c;
           match c.cpremise with
+          | Lemma _ -> Stack.push c s
           | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s
           | _ -> () (* Only simplified clauses can have a level > 0 *)
         end else begin

src/core/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
+            let new_clause = St.make_clause (fresh_pcl_name ())
-                (St.History [c; d]) in
+                l (List.length l) (St.History [c; d]) in
             chain_res (new_clause, l) r
         end
       | _ -> assert false
@@ -139,9 +139,10 @@ module Make(St : Solver_types.S) = struct
     match conclusion.St.cpremise with
     | St.Lemma l ->
       {conclusion; step = Lemma l; }
-    | St.History [] ->
+    | St.Hyp _ ->
-      assert (not conclusion.St.learnt);
       { conclusion; step = Hypothesis; }
+    | St.History [] ->
+      assert false
     | St.History [ c ] ->
       assert (cmp c conclusion = 0);
       expand c
@@ -156,18 +157,27 @@ module Make(St : Solver_types.S) = struct
       { conclusion; step = Resolution (c', d', a); }
 
   (* Compute unsat-core
-     TODO: the uniq sort at the end may be costly, maybe remove it,
+     TODO: replace visited bool by a int unique to each call
-           or compare the clauses faster ? *)
+     of unsat_core, so that the cleanup can be removed ? *)
   let unsat_core proof =
-    let rec aux acc = function
+    let rec aux res acc = function
-      | [] -> acc
+      | [] -> res, acc
       | c :: r ->
-        begin match c.St.cpremise with
+        if not c.St.visited then begin
-          | St.History [] | St.Lemma _ -> aux (c :: acc) r
+          c.St.visited <- true;
-          | St.History l -> aux acc (l @ r)
+          match c.St.cpremise with
-        end
+            | St.Hyp _ | St.Lemma _ -> aux (c :: res) acc r
+            | St.History h ->
+              let l = List.fold_left (fun acc c ->
+                  if not c.St.visited then c :: acc else acc) r h in
+              aux res (c :: acc) l
+        end else
+          aux res acc r
     in
-    sort_uniq cmp (aux [] [proof])
+    let res, tmp = aux [] [] [proof] in
+    List.iter (fun c -> c.St.visited <- false) res;
+    List.iter (fun c -> c.St.visited <- false) tmp;
+    res
 
   (* Iter on proofs *)
   module H = Hashtbl.Make(struct

src/core/solver_types.ml

@@ -58,11 +58,11 @@ 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;
-    mutable removed : bool;
+    mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =
@@ -71,6 +71,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     | Semantic of int
 
   and premise =
+    | Hyp of int
     | Lemma of proof
     | History of clause list
 
@@ -102,9 +103,9 @@ 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;
+      visited = false;
       cpremise = History [] }
 
   let () =
@@ -182,25 +183,24 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       | Formula_intf.Negated -> var.na
       | Formula_intf.Same_sign -> var.pa
 
-  let make_clause ?tag ?lvl 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 lvl, premise with
+      match premise with
-      | Some lvl, History [] -> lvl
+      | Hyp lvl -> lvl
-      | Some _, _ -> assert false
+      | Lemma _ -> 0
-      | None, History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
+      | History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
-      | None, Lemma _ -> 0
     in
     { name  = name;
       tag = tag;
       atoms = atoms;
-      removed = false;
+      attached = false;
-      learnt = is_learnt;
+      visited = false;
       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
@@ -263,7 +263,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
 
   (* Complete debug printing *)
-  let sign a = if a == a.var.pa then "" else "-"
+  let sign a = if a == a.var.pa then "+" else "-"
 
   let level a =
     match a.var.v_level, a.var.reason with
@@ -279,27 +279,28 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     else "[]"
 
   let pp_premise out = function
-    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
+    | Hyp _ -> Format.fprintf out "hyp"
     | Lemma _ -> Format.fprintf out "th_lemma"
+    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v
 
   let pp_assign out = function
     | None -> ()
-    | Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t
+    | Some t -> Format.fprintf out " ->@ %a" E.Term.print t
 
   let pp_lit out v =
-    Format.fprintf out "%d [lit:%a]%a"
+    Format.fprintf out "%d [lit:%a%a]"
       (v.lid+1) E.Term.print v.term pp_assign v.assigned
 
   let pp_atom out a =
-    Format.fprintf out "%s%d%s[lit:%a]"
+    Format.fprintf out "%s%d%s[atom:%a]@ "
       (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
 
   let pp_atoms_vec out vec =
-    Vec.print ~sep:"; " pp_atom out vec
+    Vec.print ~sep:"" pp_atom out vec
 
-  let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
+  let pp_clause out {name=name; atoms=arr; cpremise=cp; } =
-    Format.fprintf out "%s%s{ %a} cpremise={{%a}}"
+    Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
-      name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
+      name pp_atoms_vec arr pp_premise cp
 
 end
 

src/core/solver_types_intf.ml

@@ -53,11 +53,11 @@ module type S = sig
     name : string;
     tag : int option;
     atoms : atom Vec.t;
-    learnt : bool;
     c_level : int;
     mutable cpremise : premise;
     mutable activity : float;
-    mutable removed : bool;
+    mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =
@@ -66,6 +66,7 @@ module type S = sig
     | Semantic of int
 
   and premise =
+    | Hyp of int
     | Lemma of proof
     | History of clause list
 
@@ -115,8 +116,8 @@ module type S = sig
 
   val empty_clause : clause
   (** The empty clause *)
-  val make_clause : ?tag:int -> ?lvl: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. *)
+  (** [make_clause name atoms size premise] creates a clause with the given attributes. *)
 
   (** {2 Clause names} *)