Many things, sorry for the mess.

- Implement two new enumeration domains (they don't bring us much) :
    multi valuation for variables ;
    multi valuation for variables and pairs of variables (not really sure it works)
- Make it so that the number of init/time variables is reduced
      (do not create new init/time variables on node instanciation, only
      inside activate blocks and automaton states)
- Some work on EDD (it is currently broken and does not compile)

1 files changed, 6 insertions, 4 deletions

diff --git a/main.ml b/main.ml
index 667ffed..5956b9e 100644
--- a/main.ml
+++ b/main.ml
@@ -9,10 +9,12 @@ module Interpret = Interpret.I
 
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
 
-module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND)
-module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND)
+module AI_Itv = Abs_interp.I(Enum_domain.MultiValuationCCons)(ItvND)
+module AI_Rel = Abs_interp.I(Enum_domain.MultiValuationCCons)(Apron_domain.ND)
 
+(*
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
+*)
 
 (* command line options *)
 let dump = ref false
@@ -82,8 +84,6 @@ let do_test_interpret prog verbose =
 let () =
     Arg.parse options (fun f -> ifile := f) usage;
 
-    AI_Itv_EDD.test ();
-
     if !ifile = "" then begin
         Format.eprintf "No input file...@.";
         exit 1
@@ -117,7 +117,9 @@ let () =
           
           if !ai_itv then AI_Itv.do_prog opt rp;
           if !ai_rel then AI_Rel.do_prog opt rp;
+          (*
           if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
+          *)
       end;
 
       if !vtest then do_test_interpret prog true