Merge branch 'wip-analyze'

src/core/internal.ml

@@ -464,8 +464,6 @@ module Make
   (* Boolean propagation.
      Wrapper function for adding a new propagated formula. *)
   let enqueue_bool a ~level:lvl reason : unit =
-    Log.debugf 99 "Trying to enqueue: @[<hov>%a@\n%a@]"
-      (fun k -> k St.pp_atom a St.pp_reason (lvl, Some reason));
     if a.neg.is_true then begin
       Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a);
       assert false
@@ -523,22 +521,19 @@ module Make
      and a boolean stating whether it is
      a UIP ("Unique Implication Point")
      precond: the atom list is sorted by decreasing decision level *)
-  let backtrack_lvl ~is_uip : atom list -> int = function
+  let backtrack_lvl : atom list -> int * bool = function
-    | [] -> 0
+    | [] | [_] ->
-    | [a] ->
+      0, true
-      assert is_uip;
-      0
     | a :: b :: r ->
       assert(a.var.v_level > base_level ());
-      if is_uip then (
+      if a.var.v_level > b.var.v_level then begin
         (* backtrack below [a], so we can propagate [not a] *)
-        assert(a.var.v_level > b.var.v_level);
+        b.var.v_level, true
-        b.var.v_level
+      end else begin
-      ) else (
         assert (a.var.v_level = b.var.v_level);
         assert (a.var.v_level >= base_level ());
-        max (a.var.v_level - 1) (base_level ())
+        max (a.var.v_level - 1) (base_level ()), false
-      )
+      end
 
   (* result of conflict analysis, containing the learnt clause and some
      additional info.
@@ -558,7 +553,7 @@ module Make
      atom, and perform resolution steps with each propagation reason, until
      the First UIP clause is found, or we get semantic propagations
      at the highest level (see mcsat paper for more explications).
-  *)
+  *) (*
   let analyze_mcsat c_clause : conflict_res =
     let tr_ind  = ref (Vec.size env.elt_queue) in
     let is_uip  = ref false in
@@ -612,6 +607,7 @@ module Make
         cr_history = List.rev !history;
         cr_is_uip = !is_uip;
       }
+  *)
 
   let get_atom i =
     match Vec.get env.elt_queue i with
@@ -629,7 +625,6 @@ module Make
     let seen   = ref [] in
     let c      = ref c_clause in
     let tr_ind = ref (Vec.size env.elt_queue - 1) in
-    let size   = ref 1 in
     let history = ref [] in
     assert (decision_level () > 0);
     let conflict_level =
@@ -660,7 +655,6 @@ module Make
               incr pathC;
             end else begin
               learnt := q :: !learnt;
-              incr size;
               blevel := max !blevel q.var.v_level
             end
           end
@@ -682,6 +676,9 @@ module Make
       | 0, _ ->
         cond := false;
         learnt := p.neg :: (List.rev !learnt)
+      | n, Some Semantic _ ->
+        assert (n > 0);
+        learnt := p.neg :: !learnt
       | n, Some Bcp cl ->
         assert (n > 0);
         assert (p.var.v_level >= conflict_level);
@@ -689,16 +686,21 @@ module Make
       | n, _ -> assert false
     done;
     List.iter (fun q -> q.var.seen <- false) !seen;
-    { cr_backtrack_lvl= !blevel;
+    let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in
-      cr_learnt= !learnt;
+    let level, is_uip = backtrack_lvl l in
+    { cr_backtrack_lvl = level;
+      cr_learnt = l;
       cr_history = List.rev !history;
-      cr_is_uip = true;
+      cr_is_uip = is_uip;
     }
 
   let analyze c_clause : conflict_res =
+    analyze_sat c_clause
+      (*
     if St.mcsat
     then analyze_mcsat c_clause
     else analyze_sat c_clause
+         *)
 
   (* add the learnt clause to the clause database, propagate, etc. *)
   let record_learnt_clause (confl:clause) (cr:conflict_res): unit =
@@ -766,7 +768,7 @@ module Make
         )
         else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history))
       in
-      Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
+      Log.debugf 4 "New clause: @[<hov>%a@]" (fun k->k St.pp_clause clause);
       Array.iter (fun x -> insert_var_order (elt_of_var x.var)) clause.atoms;
       Vec.push vec clause;
       match atoms with

src/core/solver_types.ml

@@ -280,11 +280,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   let pp_value fmt a =
     if a.is_true then
-      Format.fprintf fmt "[T%a]" pp_level a
+      Format.fprintf fmt "T%a" pp_level a
     else if a.neg.is_true then
-      Format.fprintf fmt "[F%a]" pp_level a
+      Format.fprintf fmt "F%a" pp_level a
     else
-      Format.fprintf fmt "[]"
+      Format.fprintf fmt ""
 
   let pp_premise out = function
     | Hyp -> Format.fprintf out "hyp"
@@ -292,16 +292,19 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     | Lemma _ -> Format.fprintf out "th_lemma"
     | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v
 
-  let pp_assign out = function
+  let pp_assign fmt v =
-    | None -> ()
+    match v.assigned with
-    | Some t -> Format.fprintf out " ->@ @[<hov>%a@]" E.Term.print t
+    | None ->
+      Format.fprintf fmt ""
+    | Some t ->
+      Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
 
   let pp_lit out v =
-    Format.fprintf out "%d [lit:@[<hov>%a%a@]]"
+    Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
-      (v.lid+1) E.Term.print v.term pp_assign v.assigned
+      (v.lid+1) pp_assign v E.Term.print v.term
 
   let pp_atom out a =
-    Format.fprintf out "%s%d%a[atom:@[<hov>%a@]]@ "
+    Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]@ "
       (sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit
 
   let pp_atoms_vec out vec =

src/mcsat/plugin_mcsat.ml

@@ -150,7 +150,7 @@ let eval = function
   | { Expr_smt.atom = Expr_smt.Equal (a, b); sign } ->
     begin try
         let v_a, a_lvl = H.find map a in
-        let v_b, b_lvl = H.find map a in
+        let v_b, b_lvl = H.find map b in
         if Expr_smt.Term.equal v_a v_b then
           Plugin_intf.Valued(sign, max a_lvl b_lvl)
         else