Update: monadisation of Lutin, part 7

Rationale: make rdbg time traveling work.

_oasis

@@ -27,7 +27,7 @@ Executable lutin
   Path:   lutin/src
   MainIs: main.ml
   BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp
-  NativeOpt: -warn-error "+26" -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
+  NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
   Build: true
   Install:true
   CompiledObject: native

examples/up_and_down/ud.lut

@@ -17,3 +17,4 @@ node up_and_down(min, max, delta : real) returns (x : real) =
 
 node main () returns (x :  real) =
     run x:= up_and_down(0.0, 100.0, 5.0)
+

lutin/src/bddd.mli

@@ -17,6 +17,8 @@
 
 type t  
 
+exception No_numeric_solution	of t
+
 val draw_in_bdd : t -> Var.env_in -> Var.env -> int -> string -> Exp.var list ->
   Bdd.t -> Bdd.t -> t * Var.env * Store.t' * Store.p
   (** [draw_in_bdd memory verbose_level ctx_msg state vars bdd comb]
@@ -31,7 +33,17 @@ val draw_in_bdd : t -> Var.env_in -> Var.env -> int -> string -> Exp.var list ->
 
 open Sol_nb
 
+val formula_to_bdd : t -> Var.env_in -> Var.env -> string -> int ->
+  Exp.formula -> t * Bdd.t
+
+val index_to_linear_constraint : t -> int -> Constraint.t
+val get_index_from_linear_constraint : t -> Constraint.t -> int
+val num_to_gne: t -> Var.env_in -> Var.env -> string -> int -> Exp.num -> t * Gne.t
+val eval_int_expr: t -> Exp.num -> string -> Var.env_in -> Var.env  -> int -> int option
+
 
+val clear : t -> t
+  
 val sol_number : t -> Bdd.t -> sol_nb * sol_nb
   (** [sol_number bdd] returns the solution number in the [then] and [else]
     branches of [bdd]. *)

lutin/src/exprUtil.ml

 open Expr
 open Constraint
 
-let (index_to_exp : int -> Expr.t * bool) =
-  fun i ->
+let (index_to_exp : Bddd.t -> int -> Expr.t * bool) =
+  fun bddt i ->
     let aux ne = 
       [Ne.to_expr ne; if Ne.is_int ne then Ival (Num.Int 0) else Fval 0.0]
     in
-    match Formula_to_bdd.index_to_linear_constraint i with
+    match Bddd.index_to_linear_constraint bddt i with
       | Bv(v)   -> Var (Var.name v), false
       | EqZ(ne) -> Op (Eq, aux ne), true
       | Ineq(GZ(ne))   -> Op (Sup, aux ne), true
@@ -14,8 +14,8 @@ let (index_to_exp : int -> Expr.t * bool) =
 
 let impl a b = not a || b
 
-let (collect : bool -> Bdd.t -> Expr.t) =
-  fun num bdd ->
+let (collect : Bddd.t -> bool -> Bdd.t -> Expr.t) =
+  fun bddt num bdd ->
     (* Collect the set of paths leading to true.  If the [num] flag is
        true, collect only the numeric constraints.  *)
     let rec (aux: Bdd.t -> Expr.t list list) =
@@ -24,7 +24,7 @@ let (collect : bool -> Bdd.t -> Expr.t) =
         assert(not(Bdd.is_true bdd));
         assert(not(Bdd.is_false bdd));
         let t,e = Bdd.dthen bdd, Bdd.delse bdd in
-        let v,is_num =  index_to_exp (Bdd.topvar bdd) in
+        let v,is_num = index_to_exp bddt (Bdd.topvar bdd) in
         let not_v = Op(Not,[v]) in
         let res_t =
           if (Bdd.is_true t) then (if (impl num is_num) then [[v]] else []) else 
@@ -51,11 +51,11 @@ let (collect : bool -> Bdd.t -> Expr.t) =
 let lminus l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
 
 (* exported *)
-let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Expr.t) =
-  fun bdd bdd1 (expr2,bdd2) ->
+let (get_info : Bddd.t -> Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Expr.t) =
+  fun bddt bdd bdd1 (expr2,bdd2) ->
     assert (not(Bdd.is_false bdd1));
     let is_sat = not (Bdd.is_false bdd) in
-    if is_sat then collect true bdd
+    if is_sat then collect bddt true bdd
     else if Bdd.is_false bdd2 then expr2 else
       (* try to simplify the formula associated to bdd by projet *)
       let s1 = Bdd.list_of_support (Bdd.support bdd1)
@@ -67,6 +67,6 @@ let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Expr.t) =
       assert (not(Bdd.is_false bdd1));
       assert (not(Bdd.is_false bdd2));
       assert (Bdd.is_false (Bdd.dand bdd1 bdd2));        
-      Expr.Op(Expr.And, [collect false bdd1; collect false bdd2])
+      Expr.Op(Expr.And, [collect bddt false bdd1; collect bddt false bdd2])
 
 

lutin/src/exprUtil.mli

@@ -19,4 +19,4 @@
    - bdd=bdd1^bdd2 has no sol 
    - bdd2=to_bdd(e2).
 *)
-val get_info : Bdd.t -> Bdd.t ->  (Expr.t * Bdd.t) -> Expr.t
+val get_info : Bddd.t -> Bdd.t -> Bdd.t ->  (Expr.t * Bdd.t) -> Expr.t

lutin/src/fGen.ml

@@ -5,7 +5,6 @@
 **-----------------------------------------------------------------------
 **
 ** File: fGen.ml
-** Author: erwan.jahier@univ-grenoble-alpes.fr
 **
 *)
 
@@ -15,8 +14,8 @@
 *)
 
 type t = {
-   choose_one_formula: unit -> t * Exp.formula * Prog.ctrl_state ;
-   get_all_formula: unit -> Exp.formula list
+	choose_one_formula :  unit ->  t * Exp.formula  * Prog.ctrl_state;
+	get_all_formula : unit -> Exp.formula list
 }
 
 (*** Exceptions *)
@@ -29,5 +28,5 @@ exception NormalStop of string
    "x.choose_one_formula" instead of "choose_one_formula x" 
    "x.get_all_formula"    instead of "get_all_formula x" 
 *)
-let choose_one_formula (x:t) = x.choose_one_formula ()
-let get_all_formula (x:t) = x.get_all_formula ()
+(* let choose_one_formula st (x:t) = x.choose_one_formula st *)
+(* let get_all_formula st (x:t) = x.get_all_formula st *)

lutin/src/fGen.mli

@@ -17,7 +17,7 @@ new abstract interface:
 *)
 
 type t = {
-	choose_one_formula : unit -> t * Exp.formula * Prog.ctrl_state;
+	choose_one_formula :  unit ->  t * Exp.formula * Prog.ctrl_state;
 	get_all_formula : unit -> Exp.formula list
 }
 

lutin/src/formula_to_bdd.mli

@@ -11,8 +11,10 @@
 (**)
 (**  Encoding formula and expressions into bdds. *)
 
-
-val f : Var.env_in -> Var.env -> string -> int -> Exp.formula -> Bdd.t
+type t
+val init : unit -> t
+  
+val f : t -> Var.env_in -> Var.env -> string -> int -> Exp.formula -> t * Bdd.t
   (** [Formula_to_bdd.f input memory ctx_msg verbosity_level f]
       returns the bdd of [f] where [input] and pre variables have
       been repaced by their values. [ctx_msg] is used for printing
@@ -24,25 +26,25 @@ val f : Var.env_in -> Var.env -> string -> int -> Exp.formula -> Bdd.t
   *)
 
 
-val num_to_gne : Var.env_in -> Var.env -> string -> int -> Exp.num -> Gne.t
-  (** The same as f but for numeric expressions *)
+val num_to_gne: t -> Var.env_in -> Var.env -> string -> int -> Exp.num -> t * Gne.t
+
+val eval_int_expr: t -> Exp.num -> string -> Var.env_in -> Var.env  -> int -> int option
+
 
 (** Clean-up all the internal tables that migth have been filled
   by (non-regression) assertions.
 *)
-val clear_all : unit -> unit
+val clear_all : t -> t
 
 (** Clean-up the cache tables that contain information that
     depends on input or pre. Indeed, this information is very likely
     to change (especially because floats) at each step, therefore we do
     not keep that information to avoid memory problems.
 *)
-val clear_step : unit -> unit
+val clear_step : t -> t
 
 
 (* Returns the atomic formula of an index. *)
-val index_to_linear_constraint : int -> Constraint.t
-val get_index_from_linear_constraint : Constraint.t -> int
+val index_to_linear_constraint : t -> int -> Constraint.t
+val get_index_from_linear_constraint : t -> Constraint.t -> int
 
-val bdd_manager : unit ref
-(* val bdd_manager : Manager.t ref *)

lutin/src/gne.ml

@@ -30,7 +30,7 @@ type t = (Bdd.t * bool) NeMap.t
 let (dump : t -> unit) =
   fun gne ->
     ignore (NeMap.fold
-       (fun ne (bdd, dep) acc ->
+       (fun ne (bdd, _dep) acc ->
 	       print_string ("\n\t" ^ (Ne.to_string ne) ^ "  -> ");
           flush stdout;
           Bdd.print_mons bdd;
@@ -60,7 +60,7 @@ let (add_ne : Bdd.t -> bool -> Ne.t -> t -> t) =
 let (dyn_check_gne : t  -> bool) =
   fun gne -> 
     let bddl = NeMap.fold
-	   (fun ne (c,dep) acc -> c::acc)
+	   (fun _ne (c,dep) acc -> c::acc)
 	   gne
 	   []
     in

lutin/src/lucFGen.ml

@@ -89,7 +89,7 @@ let (get_all_formula: t -> formula list) =
     
 (****************************************************************************)
 
-let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
+let rec (wt_list_to_cont : Var.env_in -> Prog.state ref -> wt_cont list ->
          formula ->  node list -> t -> t) =
   fun input state wtl facc nl fgen ->
     (* [nl] is the list of nodes that correspond to [facc] *)
@@ -112,10 +112,10 @@ let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
           in
           wt_list_to_cont input state wtl' f2 (n::nl) fgen'
 and
-  (choose_one_formula_atomic : Var.env_in -> Prog.state -> 
+  (choose_one_formula_atomic : Var.env_in -> Prog.state ref -> 
    Exp.formula -> wt_cont -> wt_cont * formula * node) = 
   fun input state facc cont ->
-    let _ = if debug then (print_string "XXX choose_one_formula_atomic\n"; flush stdout) in
+    let _ = if debug then (print_string "xxx choose_one_formula_atomic\n"; flush stdout) in
     match cont with
     | WFinish ->  WFinish, False, ""
     | WStop _ ->  cont, True, ""
@@ -129,18 +129,18 @@ and
         | f, True -> f
         | _,_ -> And(f,facc) 
       in
-      let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
+      let ctx_msg = Prog.ctrl_state_to_string_long !state.d.ctrl_state in
       Utils.time_C "is_sat";
       let snt, sat =
-        assert false;
-        Solver.is_satisfiable state.d.snt input state.d.memory state.d.verbose ctx_msg facc' ""
+        Solver.is_satisfiable !state.d.snt input !state.d.memory !state.d.verbose ctx_msg facc' ""
       in
+      state := { !state with d = { !state.d with snt = snt } } ;
       Utils.time_R "is_sat";
       if  sat then (cont', facc', n)
       else choose_one_formula_atomic input state facc cont'
 
 
-and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =
+and (wt_to_cont : Var.env_in -> Prog.state ref -> wt -> wt_cont -> wt_cont) =
   fun input state (tbl, n) cont ->
     let _ = if debug then (print_string ("XXX wt_to_cont "^ n ^"\n"); flush stdout) in
     let children = Util.StringMap.find n tbl in
@@ -201,14 +201,14 @@ and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =
       
 (****************************************************************************)
 (* NO LONGER EXPORTED *)
-let (_internal_get : Var.env_in -> Prog.state -> t list) =
+let (_internal_get : Var.env_in -> Prog.state ref -> t list) =
   fun input state ->
     let _ = if debug then (print_string "XXX get\n"; flush stdout) in
-    let nll = state.d.ctrl_state in
+    let nll = !state.d.ctrl_state in
     List.map 
     (fun nl -> 
 Utils.time_C "get_wtl";
-       let wtl = state.s.get_wtl input state nl in
+       let wtl = !state.s.get_wtl input !state nl in
 Utils.time_R "get_wtl";
        let _ = if debug then List.iter Prog.print_wt wtl in
 Utils.time_C "wt_to_cont";
@@ -225,7 +225,7 @@ Utils.time_R "wt_list_to_cont";
 (* EXPORTED *)
 
 let rec (fgen_of_t : t -> FGen.t) =
-  fun t ->
+  fun t  ->
     {
       FGen.choose_one_formula = (
         fun () ->

lutin/src/lucFGen.mli

@@ -5,14 +5,13 @@
 **-----------------------------------------------------------------------
 **
 ** File: fGen.mli
-** Author: erwan.jahier@univ-grenoble-alpes.fr
 
 --> modified to fit the FGgen interface
     the only exported thing is the "get" whihch creates a FGen.t
 *)
 
 
-val get : Var.env_in -> Prog.state -> FGen.t list
+val get : Var.env_in -> Prog.state ref -> FGen.t list
 
 (* NO LONGER EXPORTED ------- 
 (** Runtime Automaton. *)

lutin/src/lucky.ml

@@ -41,7 +41,6 @@ let (draw_values : Var.env_in -> Prog.state -> int -> Thickness.numeric ->
       let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in 
       let vl = state.d.verbose in
       let ra, f, cs = ra.FGen.choose_one_formula () in
-      assert false;
       match
 	     Solver.solve_formula state.d.snt input state.d.memory vl ctx_msg
         state.s.output_var_names p num_thickness bool_to_gen_f num_to_gen f 
@@ -182,9 +181,10 @@ let (env_try : Thickness.t -> env_in -> Prog.state -> FGen.t list ->
 	
 (*****************************************************************************)
 (* Exported *)
-let (env_step : step_mode -> env_in -> Prog.state -> FGen.t list -> 
-     Prog.state * solution) =
-  fun step_mode input state ral ->
+let (env_step : step_mode -> env_in -> Prog.state ref -> FGen.t list -> 
+     solution) =
+  fun step_mode input state_ref ral ->
+    let state = !state_ref in
     let thick =
       match step_mode with
 	   | StepInside -> (1, 0, Thickness.AtMost 0)
@@ -202,17 +202,16 @@ let (env_step : step_mode -> env_in -> Prog.state -> FGen.t list ->
 	     last_input = input;
 	     last_output = output;
 	     last_local  = local;
-        snt = state.d.snt;
+        snt = Bddd.clear state.d.snt;
 	     verbose = state.d.verbose
 	   }
 	   in	
 	   let new_state = { d = new_state_dyn ; s = state.s } in
-	   (* Clean-up cached info that depends on pre or inputs *)
-	   Formula_to_bdd.clear_step ();
 
 	   previous_output := Some output;
-	   previous_local := Some local;  
-	   (new_state, (output, local))
+	   previous_local := Some local;
+      state_ref:= new_state;
+	   (output, local)
     with
 	   FGen.NoMoreFormula  -> 
 	   match (!previous_output, !previous_local) with
@@ -224,7 +223,7 @@ let (env_step : step_mode -> env_in -> Prog.state -> FGen.t list ->
 			       "### No transition is available; " ^ 
 			       "values of the previous cycle are used.\n");
 		      flush stdout;
-		      (state, (out, loc))
+		      (out, loc)
 		    ) 
 		  else
 		    (

lutin/src/lucky.mli

@@ -32,8 +32,8 @@ type step_mode =  StepInside | StepEdges | StepVertices
 
     Raises FGen.NoMoreFormula when no more step can be done
 *)
-val env_step : step_mode -> Var.env_in -> Prog.state -> FGen.t list -> 
-  Prog.state * solution
+val env_step : step_mode -> Var.env_in -> Prog.state ref -> FGen.t list -> 
+  solution
 
 
   (** [env_try thickness input state] does basically the same things

lutin/src/luckyDraw.ml

@@ -354,7 +354,7 @@ let (draw : ?mode:(draw_mode) -> ?verbose:(int) -> solutions_set -> solution lis
 	      num_subst_ll
 	in
 	  subst_ll
-      with Store.No_numeric_solution -> []
+      with Store.No_polyedral_solution -> []
 
 
 (** nb: the default step mode is StepInside 

lutin/src/lutExe.mli

@@ -72,15 +72,17 @@ type behavior_gen =
 
 
 val get_init_state: t -> control_state
+val clear: t -> t
 
 val get_init_pres: t -> Value.OfIdent.t
 
-val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> (unit -> behavior_gen)
+val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state ->
+  (unit -> t * behavior_gen)
 
 val find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard ->
-  guard * (Var.env_out * Var.env_loc) list
+  t * guard * (Var.env_out * Var.env_loc) list
 
-val find_one_sol : t -> guard -> guard * (Var.env_out * Var.env_loc)
+val find_one_sol : t -> guard -> t * guard * (Var.env_out * Var.env_loc)
 
 val make_pre : Var.env_in -> Var.env_out -> Var.env_loc -> Var.env 
 
@@ -89,9 +91,9 @@ val make_pre : Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
 *)
 type ctx = Event.t
 type e = Event.t
-val step: t -> control_state -> data_state -> control_state * data_state
+val step: t -> control_state -> data_state -> t * control_state * data_state
 val step_ldbg: ctx -> string -> t -> control_state -> data_state ->
-  (ctx -> control_state ->  data_state -> e) -> e
+  (ctx -> t -> control_state -> data_state -> e) -> e
 
 
 (***** Interface for building simple step main loop (e.g. for run statements *)

lutin/src/lutinRun.ml

-(* Time-stamp: <modified the 12/04/2019 (at 11:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/04/2019 (at 16:36) by Erwan Jahier> *)
 (**********************************************************************************)
 type vars = (string * Data.t) list
 
@@ -43,6 +43,7 @@ let make argv =
     (*     else *)
     Value.OfIdent.empty
   in
+  let tables = ref lut_mach in 
   let ctrl_state = ref (LutExe.get_init_state lut_mach) in
   let data_state = ref
       { LutExe.ins = Value.OfIdent.empty;
@@ -54,7 +55,8 @@ let make argv =
 
   let lut_step sl =
     let _ = data_state := { !data_state with LutExe.ins = to_vals sl } in
-    let new_cs, new_ds =  LutExe.step lut_mach !ctrl_state !data_state in
+    let new_tables, new_cs, new_ds = LutExe.step !tables !ctrl_state !data_state in
+    tables := new_tables;
     ctrl_state := new_cs;
     data_state := new_ds;
     to_subst_list lut_out new_ds.LutExe.outs
@@ -64,13 +66,14 @@ let make argv =
        (Data.subst list -> ctx -> Event.t) -> Event.t) =
     fun sl ctx cont -> 
       let cont_lut_step ctx = 
-        fun new_cs new_ds -> 
+        fun new_tables new_cs new_ds -> 
+          tables := new_tables;
           ctrl_state := new_cs;
           data_state := new_ds;
           cont (to_subst_list lut_out new_ds.LutExe.outs) ctx
       in
       data_state := { !data_state with LutExe.ins = to_vals sl };
-      LutExe.step_ldbg ctx node lut_mach !ctrl_state !data_state cont_lut_step
+      LutExe.step_ldbg ctx node !tables !ctrl_state !data_state cont_lut_step
   in
   let mems_in = 
     List.fold_left

lutin/src/main.ml

@@ -5,14 +5,6 @@ open Lexeme
 open Filename
 open MainArg
 open LutErrors
-(*
-open Parsing;;
-open Parsers;;
-open Format;;
-open SyntaxeDump;;
-open Expand;;
-open Auto2Lucky;;
-*)
 
 exception Stop
 
@@ -118,7 +110,7 @@ let dump_prog p = (
 let gnuplot_pid_ref = ref None
 let gnuplot_oc = ref None
 
-(* simu : old lutin main *)
+(* simu : old lutin main XXX obselete !*)
 let rec to_simu oc infile mnode opt = (
   (* Parse and build the internal structure *)
   let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs opt) infile mnode in 
@@ -182,16 +174,21 @@ and main_loop_core oc opt t init_state init_pre_lut_output  state pre_lut_output
         Rif.read (Verbose.level()>0) stdin (if noo then Some oc else None)
           state.Prog.s.Prog.in_vars     
   in
-  let generator = LucFGen.get lut_input state in
+  let state_ref = ref state in
+  let generator = LucFGen.get lut_input state_ref in
+  
   (*
     Call Lucky explorer/solver
     env_step : step_mode -> Var.env_in -> Prog.state -> FGen.t list -> Prog.state * solution
     where type solution = Var.env_out * Var.env_loc
   *)
   let (next_state, (lut_output, loc)) = try (
-    Lucky.env_step (MainArg.step_mode opt) lut_input state generator
+    let sol = Lucky.env_step (MainArg.step_mode opt) lut_input state_ref generator in
+    !state_ref, sol
+    
   ) with
-    | FGen.NoMoreFormula ->
+  | FGen.NoMoreFormula ->
+    let state = !state_ref in
       Rif.write oc ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
       Rif.write oc "# No transition is labelled by a satisfiable formula.\n" ;
       Rif.write oc "# The Lutin program is blocked.\n";
@@ -224,8 +221,10 @@ and main_loop_core oc opt t init_state init_pre_lut_output  state pre_lut_output
   Rif.write oc "\n";
   Rif.flush oc;
 
-    (* Clean-up cached info that depend on pre or inputs *)
-  Formula_to_bdd.clear_step ();
+  (* Clean-up cached info that depend on pre or inputs *)
+  let next_state = { state with
+                     d = { next_state.d with snt = Bddd.clear next_state.d.snt } }
+  in
 
   match MainArg.max_steps opt with
   |  None -> main_loop oc opt (t+1) init_state init_pre_lut_output
@@ -247,7 +246,6 @@ let dbgexe = Verbose.get_flag "LutExe"
 let quit oc = Rif.write oc "q\n"; Rif.flush oc
 
 
-
 (* simu with LutExe *)
 let to_exe oc infile mnode opt = (
   let exe = LutExe.make opt  infile mnode in
@@ -266,23 +264,22 @@ let to_exe oc infile mnode opt = (
   let rec do_step cpt init_ctrl init_ins init_pres ctrl ins pres = (
 
     (* Clean-up cached info that depend on pre or inputs *)
-    Formula_to_bdd.clear_step ();
-
+    (*     let exe = LutExe.clear exe in *)
     Verbose.put "#Main.to_exe: step %d\n" cpt;
     let bg = LutExe.get_behavior_gen exe ins pres ctrl in
     match bg () with
-      | LutExe.NoMoreBehavior i -> ( 
+      | _, LutExe.NoMoreBehavior i -> ( 
         Rif.write oc ("#end.\n# Simulation ended with uncaught Deadlock " ^
                          (if i=0 then "" else ("at event " ^ (string_of_int i)))^ "\n");
         Rif.flush oc;
         exit 2
       )
-      | LutExe.SomeBehavior (b, bg') -> (
+      | exe, LutExe.SomeBehavior (b, bg') -> (
         match b with
           | LutExe.Goto (zeguard, ctrl') -> (
             (* THIS IS THE NORMAL BEHAVIOR *)
             MainArg.event_incr opt;
-            let zeguard, (outs, locs) = try LutExe.find_one_sol exe zeguard
+            let exe, zeguard, (outs, locs) = try LutExe.find_one_sol exe zeguard
               with Not_found -> assert false
             in
             (* Try to display more useful source level info with -vl

lutin/src/prog.ml

@@ -107,23 +107,19 @@ let (ctrl_state_to_string_long : ctrl_state list -> string) =
 let (compute_weight : Exp.weight -> Var.env_in -> state -> dyn_weight) =
   fun w input state ->
     match w with
-	Exp.Wint(i) -> V i
-      | Exp.Infinity -> Infin
-      | Exp.Wexpr(e) ->
-
-          let ctx_msg = ctrl_state_to_string_long state.d.ctrl_state in 
-	(* Utils.time_C "compute_weight (num_to_gne)"; *)
-	  let gne = Formula_to_bdd.num_to_gne input state.d.memory ctx_msg state.d.verbose e in
-	(* Utils.time_R "compute_weight (num_to_gne)"; *)
-	    match Gne.get_constant gne with
-		None ->
-		  print_string (
-		    "*** The weight expression " ^ (Exp.weight_to_string w) ^
-		    " ougth to depend only on pre and input vars\n");
-		  exit 2
-	      | Some (Value.I i) -> V (Util.int_of_num i)
-
-	      | Some (Value.F _) -> assert false
+	   Exp.Wint(i) -> V i
+    | Exp.Infinity -> Infin
+    | Exp.Wexpr(e) ->
+      let ctx_msg = ctrl_state_to_string_long state.d.ctrl_state in 
+      match Solver.eval_int_expr state.d.snt e ctx_msg input
+              state.d.memory state.d.verbose
+      with
+      | Some v -> V v
+      | None -> 
+        print_string (
+          "*** The weight expression " ^ (Exp.weight_to_string w) ^
+          " ougth to depend only on pre and input vars\n");
+        exit 2
 
 
 

lutin/src/solver.mli

@@ -28,7 +28,7 @@
 *)
 
 (* The solver monad *)
-type t
+type t = Bddd.t (* should be abstract! *)
 val init : unit -> t
 val is_satisfiable : t -> 
   Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> t * bool
@@ -64,6 +64,9 @@ val solve_formula : t -> Var.env_in -> Var.env -> int -> string ->
       Side effect: fills in the solution number table
   *)
 
+val eval_int_expr:  t -> Exp.num -> string -> Var.env_in -> Var.env -> int
+     -> int option
+
 (**/**)
 
 (** The bool flag can be set to true to remove path to the false node.

lutin/src/store.ml

@@ -19,13 +19,8 @@ open List
 let debug_store = false
 let debug_store2 = false
 
-(* let debug_store = true *)
-(* let debug_store2 = true  *)
-
-
-(* exported *)
-exception No_numeric_solution	
-
+(*  let debug_store = true  *)
+(*  let debug_store2 = true   *)
 
 type p = (Var.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list
 
@@ -299,6 +294,8 @@ let (print_store : t -> unit) =
    forever, which is really bad.
 *)
 
+(* exported *)
+exception No_polyedral_solution
 
 let (switch_to_polyhedron_representation_do : int -> t -> t' * p) =
   fun verb store ->
@@ -307,7 +304,7 @@ let (switch_to_polyhedron_representation_do : int -> t -> t' * p) =
 	     Unsat(_,_) ->
 	       print_string ("\nZZZ Dead code reached, oups...\n") ;
           flush stdout;
-	       raise No_numeric_solution (* this ougth to be dead code ... *)
+	       raise No_polyedral_solution (* this ougth to be dead code ... *)
       | Range tbl ->
 	       if
 	         store.delay = []
@@ -330,8 +327,8 @@ let (switch_to_polyhedron_representation_do : int -> t -> t' * p) =
 		                 print_string (to_string  store);
 		                 print_string "\n The polyhedron is empty .\n";
 		                 flush stdout );
-		               raise No_numeric_solution
-		             )
+		           raise No_polyedral_solution
+               )
 		          )
 		          poly_l;
 
@@ -579,15 +576,15 @@ let (make_subst : Var.name -> Value.num -> Ne.subst) =
 
 
 (* exported *)
-let rec (add_constraint : t -> Constraint.t -> t) =
-  fun store cstr0 ->
+let rec (add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t) =
+  fun store bddt cstr0 ->
     let cstr = Constraint.apply_substl store.substl cstr0 in
     let _ =
       if debug_store2 then (
 	     print_string (
 	       "add_constraint (" ^
 	         (string_of_int 
-	            (Formula_to_bdd.get_index_from_linear_constraint cstr0)) ^
+	            (Formula_to_bdd.get_index_from_linear_constraint bddt cstr0)) ^
 	         ") " ^
 	         (Constraint.to_string cstr) ^ " \n");
 	     flush stdout
@@ -610,7 +607,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
 	     dim = 0
       then
 	     ( match cstr with
-	           EqZ(ne) -> add_eq_to_store store ne
+	           EqZ(ne) -> add_eq_to_store store bddt ne
 	         | Bv _ -> assert false
 	         | Ineq(GZ(ne)) ->
 		          if
@@ -656,7 +653,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
 	       What is the better solution really ???
 	     *)
 	     ( match cstr with
-	           EqZ(ne) -> add_eq_to_store store ne
+	           EqZ(ne) -> add_eq_to_store store bddt ne
 	         | Bv _ -> assert false
 	         | Ineq ineq ->
 		          if debug_store then (
@@ -679,7 +676,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
 	           unsat_store cstr store
 	       | Range(tbl) ->
 	           ( match cstr with
-		              EqZ(ne) -> add_eq_to_store store ne
+		              EqZ(ne) -> add_eq_to_store store bddt ne
 		            | Bv _ -> assert false
 		            | Ineq ineq ->
 		                let (vn, nac) = normalise ineq in
@@ -760,7 +757,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
 					                              (Constraint.ineq_to_string cstr);
 					                            flush stdout
 					                          );
-					                          add_constraint acc (Ineq cstr)
+					                          add_constraint acc bddt (Ineq cstr)
 				                          )
 				                          { var=Range(tbl1) ; substl=sl1 ; delay=d1 ;
 					                         untouched = rm uvars vn}
@@ -808,7 +805,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
 					                           print_string (Constraint.ineq_to_string cstr);