From 5a61a6c8527fdd2d4b27c05ed070c9b95722fd43 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sun, 15 Mar 2015 22:00:48 +0100
Subject: [PATCH] Still in extreme debug mode

---
 solver/mcsolver.ml        |  2 +-
 solver/mcsolver_types.ml  | 10 +++++++++-
 solver/mcsolver_types.mli |  2 +-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 17d7dc8a..0c85e99b 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -7,7 +7,7 @@ Copyright 2014 Simon Cruanes
 module Make (L : Log_intf.S)(E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
 
-  module St = Mcsolver_types.Make(E)(Th)
+  module St = Mcsolver_types.Make(L)(E)(Th)
   module Proof = Mcproof.Make(L)(St)
 
   open St
diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml
index ec436745..87071248 100644
--- a/solver/mcsolver_types.ml
+++ b/solver/mcsolver_types.ml
@@ -15,7 +15,7 @@ open Printf
 
 module type S = Mcsolver_types_intf.S
 
-module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
+module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     type formula = E.Formula.t and type term = E.Term.t) = struct
 
   (* Types declarations *)
@@ -130,9 +130,11 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
 
   let make_boolean_var =
     fun lit ->
+      L.debug 100 "normalizing lit";
       let lit, negated = E.norm lit in
       try MF.find f_map lit, negated
       with Not_found ->
+        L.debug 100 "Lit not in table";
         let cpt_fois_2 = !cpt_mk_var lsl 1 in
         let rec var  =
           { vid = !cpt_mk_var;
@@ -157,16 +159,22 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
             neg = pa;
             is_true = false;
             aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
+        L.debug 100 "adding lit to table...";
         MF.add f_map lit var;
+        L.debug 100 "done";
         incr cpt_mk_var;
         Vec.push vars (Either.mk_right var);
+        L.debug 100 "iterating on new lit...";
         Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit;
+        L.debug 100 "done";
         var, negated
 
   let add_term t = make_semantic_var t
 
   let add_atom lit =
+    Log.debug 100 "entering add_atom";
     let var, negated = make_boolean_var lit in
+    Log.debug 100 "found atom";
     if negated then var.tag.na else var.tag.pa
 
   let make_clause name ali sz_ali is_learnt premise =
diff --git a/solver/mcsolver_types.mli b/solver/mcsolver_types.mli
index cca0ebe5..85276113 100644
--- a/solver/mcsolver_types.mli
+++ b/solver/mcsolver_types.mli
@@ -13,7 +13,7 @@
 
 module type S = Mcsolver_types_intf.S
 
-module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S with
+module Make : functor (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     type term = E.Term.t and type formula = E.Formula.t)
   -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for the Solver. *)