New: add 3 new pre-defined Lutin operators: 'nor', '#', and n-ary xor

nb: the infix binary 'xor' already existed.
nb2: xor (and so #) can be costly

_oasis

@@ -33,6 +33,24 @@ Executable lutin
   CompiledObject: native
   CClib: -lcamlidl
 
+Executable "lutin.dbg"
+  Path:   lutin/src
+  MainIs: main.ml
+  BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp
+  NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
+  Build: true
+  Install:false
+  CompiledObject: byte
+  CClib: -lcamlidl
+# to use ocamldebug:
+#  - here: set CompiledObject from native to byte
+#  - from emacs: [M-x ocamldebug] ~/lus2lic/_build/src/main.byte
+#  - from ocamldebug prompt: 
+#      cd test
+#      set arg blabla
+#      dir ~/lurette/lutin/src ~/lurette/_build/src ~/rdbg/src ~/rdbg/_build/src ~/lutils/src ~/lutils/_build/src
+
+
 Library lutin
    XMETADescription: Provides an API to call Lutin from ocaml (and rdbg)
    Path:    lutin/src

_tags

 # OASIS_START
-# DO NOT EDIT (digest: 71d84d7cf0a80c1b7d8a7d1353354192)
+# DO NOT EDIT (digest: e206596fa32c72a65d0b3f6b19835f56)
 # Ignore VCS directories, you can use the same kind of rule outside
 # OASIS_START/STOP if you want to exclude directories that contains
 # useless stuff for the build process
@@ -156,6 +156,21 @@ true: annot, bin_annot
 <lurette-nocaml/src/*.ml{,i,y}>: use_lutin
 <lurette-nocaml/src/*.ml{,i,y}>: use_lutin-utils
 <lurette-nocaml/src/*.ml{,i,y}>: use_polka
+# Executable lutin.dbg
+"lutin/src/main.byte": oasis_executable_lutin_dbg_cclib
+"lutin/src/main.byte": oasis_executable_lutin_dbg_native
+<lutin/src/*.ml{,i,y}>: oasis_executable_lutin_dbg_native
+"lutin/src/main.byte": package(camlidl)
+"lutin/src/main.byte": package(camlp4)
+"lutin/src/main.byte": package(gmp)
+"lutin/src/main.byte": package(num)
+"lutin/src/main.byte": package(rdbg-plugin)
+"lutin/src/main.byte": package(str)
+"lutin/src/main.byte": package(unix)
+"lutin/src/main.byte": use_ezdl
+"lutin/src/main.byte": use_gbddml
+"lutin/src/main.byte": use_lutin-utils
+"lutin/src/main.byte": use_polka
 # Executable lutin
 "lutin/src/main.native": oasis_executable_lutin_cclib
 "lutin/src/main.native": oasis_executable_lutin_native

examples/xor/nary.lut

+
+
+node Xor()
+returns(
+   X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100
+   :bool) =
+loop
+   xor(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+
+node Nor()
+returns(
+   X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100
+   :bool) =
+loop
+   nor(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100) 
+   
+node Diese()
+returns(
+   X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100
+   :bool) =
+   xor (X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+    fby
+    -- to check that a nor id generated from times to times
+    loop
+   #(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+   and (xor(pre X0, pre X1, pre X2, pre X3, pre X4, pre X5, pre X6, pre X7, pre X8, pre X9,
+   pre X10, pre X11, pre X12, pre X13, pre X14, pre X15, pre X16, pre X17, pre X18, pre X19,
+   pre X20, pre X21, pre X22, pre X23, pre X24, pre X25, pre X26, pre X27, pre X28, pre X29,
+   pre X30, pre X31, pre X32, pre X33, pre X34, pre X35, pre X36, pre X37, pre X38, pre X39,
+   pre X40, pre X41, pre X42, pre X43, pre X44, pre X45, pre X46, pre X47, pre X48, pre X49,
+   pre X50, pre X51, pre X52, pre X53, pre X54, pre X55, pre X56, pre X57, pre X58, pre X59,
+   pre X60, pre X61, pre X62, pre X63, pre X64, pre X65, pre X66, pre X67, pre X68, pre X69,
+   pre X70, pre X71, pre X72, pre X73, pre X74, pre X75, pre X76, pre X77, pre X78, pre X79,
+   pre X80, pre X81, pre X82, pre X83, pre X84, pre X85, pre X86, pre X87, pre X88, pre X89,
+   pre X90, pre X91, pre X92, pre X93, pre X94, pre X95, pre X96, pre X97, pre X98, pre X99, pre X100))
+   
+(*
+node nary() returns(
+   X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+   X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+   X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+   X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+   X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+   X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+   X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+   X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+   X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+   X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100
+   :bool) =
+   loop {
+     | Nor(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+           X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+           X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+           X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+           X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+           X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+           X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+           X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+           X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+           X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+     | Xor(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+           X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+           X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+           X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+           X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+           X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+           X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+           X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+           X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+           X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+     | Diese(X0, X1, X2, X3, X4, X5, X6, X7, X8, X9,
+         X10, X11, X12, X13, X14, X15, X16, X17, X18, X19,
+         X20, X21, X22, X23, X24, X25, X26, X27, X28, X29,
+         X30, X31, X32, X33, X34, X35, X36, X37, X38, X39,
+         X40, X41, X42, X43, X44, X45, X46, X47, X48, X49,
+         X50, X51, X52, X53, X54, X55, X56, X57, X58, X59,
+         X60, X61, X62, X63, X64, X65, X66, X67, X68, X69,
+         X70, X71, X72, X73, X74, X75, X76, X77, X78, X79,
+         X80, X81, X82, X83, X84, X85, X86, X87, X88, X89,
+         X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100)
+         }
+         *)
\ No newline at end of file

lutin/src/ckTypeEff.ml

@@ -29,6 +29,7 @@ type t =
 |  TEFF_except
 |  TEFF_trace
 |  TEFF_data of basic
+|  TEFF_list of basic
 |  TEFF_tuple of basic list
 |	TEFF_any of string * any_cond
 |	TEFF_ref of basic
@@ -73,24 +74,25 @@ function
 )
 (* pretty-print des types *)
 let rec to_string = ( function
- 	TEFF_data d -> (basic_to_string d)
-| 	TEFF_tuple l -> String.concat "*" (List.map basic_to_string l)
-|	TEFF_ref x -> (basic_to_string x)^" ref"
-|	TEFF_trace -> "trace"
-|	TEFF_weight -> "weight"
-|	TEFF_except -> "exception"
-|	TEFF_any (s, _) -> s
-) and prof_to_string = ( function
-	(tl, t) -> (
-		sprintf "%s->%s"
-			(list_to_string tl)
-			(list_to_string t)
-	)
-) and list_to_string = ( function
-	[] -> ""
-|	t::[] -> to_string t
-|	t::l -> sprintf "%s*%s" (to_string t) (list_to_string l)
-)
+ 	 | TEFF_data d -> (basic_to_string d)
+    |	TEFF_list d -> (basic_to_string d)^ " list"
+    |	TEFF_tuple l -> String.concat "*" (List.map basic_to_string l)
+    |	TEFF_ref x -> (basic_to_string x)^" ref"
+    |	TEFF_trace -> "trace"
+    |	TEFF_weight -> "weight"
+    |	TEFF_except -> "exception"
+    |	TEFF_any (s, _) -> s
+  ) and prof_to_string = ( function
+	   (tl, t) -> (
+		  sprintf "%s->%s"
+			 (list_to_string tl)
+			 (list_to_string t)
+	   )
+  ) and list_to_string = ( function
+	   [] -> ""
+    |	t::[] -> to_string t
+    |	t::l -> sprintf "%s*%s" (to_string t) (list_to_string l)
+  )
 
 let ref_of = function
 	TEFF_data x -> TEFF_ref x 
@@ -137,6 +139,7 @@ let get_prof tinl tout = (tinl, tout)
 
 (* TYPE USUELS *)
 let boolean  = TEFF_data Bool
+let booleans = TEFF_list Bool
 let boolref  = TEFF_ref Bool
 let intref  = TEFF_ref Int
 let integer   = TEFF_data Int
@@ -163,6 +166,8 @@ let prof_bt_t = ([boolean;trace], [trace])
 let prof_iit_t = ([integer;integer;trace], [trace])
 let prof_b_b = ([boolean], [boolean])
 let prof_bb_b = ([boolean;boolean], [boolean])
+let prof_bl_b = ([booleans], [boolean])
+                
 let prof_ii_i = ([integer;integer], [integer])
 let prof_iii_i = ([integer;integer;integer], [integer])
 let prof_et_t = ([except;trace], [trace])
@@ -211,23 +216,30 @@ let lifts_to t1 t2 = (
 	Failure OU Invalid_argument (on fait dans le dtail ?)
 *)
 let rec match_prof tel prof = (
-	(* table locale pour les types any *)
-	let anytab = Hashtbl.create 2 in
-	match prof with (txl, tres) ->
-	let doit tc tx = (
-		match_in_type anytab tc tx
-	) in
-	let _tins = List.map2 doit tel txl in
-	let _tout = List.map (match_out_type anytab) tres in
-	(* ICI : on a le profil effectif, 
-		est-ce que ca peut etre utile ??? *)
-	Verbose.exe ~flag:dbg (fun _ ->
-		Printf.fprintf stderr "CkTypeEff.match [%s] with (%s) gives %s\n"
-			(list_to_string tel)
-			(prof_to_string prof)
-			(list_to_string _tout)
-	);
-	_tout
+  (* table locale pour les types any *)
+  let anytab = Hashtbl.create 2 in
+  match prof with
+  | ([TEFF_list Bool], [TEFF_data Bool]) -> (* a special case for xor/nor/# *)
+	 let doit tc =
+      try match_in_type anytab tc (TEFF_ref Bool)
+      with _ -> match_in_type anytab tc boolean
+    in
+	 let _tins = List.map doit tel in
+	 let _tout = List.map (match_out_type anytab) [TEFF_data Bool] in
+    _tout
+  | (txl, tres) ->
+	 let doit tc tx = match_in_type anytab tc tx in
+	 let _tins = List.map2 doit tel txl in
+	 let _tout = List.map (match_out_type anytab) tres in
+	 (* ICI : on a le profil effectif, 
+		 est-ce que ca peut etre utile ??? *)
+	 Verbose.exe ~flag:dbg (fun _ ->
+		  Printf.fprintf stderr "CkTypeEff.match [%s] with (%s) gives %s\n"
+			 (list_to_string tel)
+			 (prof_to_string prof)
+			 (list_to_string _tout)
+	   );
+	 _tout
 )
 (*
 Vrifie la compatibilit :
@@ -235,34 +247,30 @@ V
 - d'un type attendu (texptd)
 - dans un table d'assoc. des any (anytab)
 *)
-and match_in_type anytab tobtd texptd = (
-	match (tobtd, texptd) with
-	(_ , TEFF_any (k, cond)) -> (
+and match_in_type anytab tobtd texptd =
+  match (tobtd, texptd) with
+  | (_ , TEFF_any (k, cond)) -> (
 		try (
-			let tprev = Util.hfind anytab k in
-			match_in_type anytab tobtd tprev
-		) with Not_found -> (
-			match (cond tobtd) with
-			Some t -> (
-				Hashtbl.add anytab k t ;
-				t
-			) |
-			None -> (
-				failwith "uncompatible types"
-			)
-		)	
-	) |
-	_ -> (
+		  let tprev = Util.hfind anytab k in
+		  match_in_type anytab tobtd tprev
+      )
+      with Not_found -> (
+			 match (cond tobtd) with
+		    | Some t -> (Hashtbl.add anytab k t ; t)
+          | None -> failwith "uncompatible types"
+		  )
+	 )
+  | _ -> (
 		if (lifts_to tobtd texptd) then texptd
 		else failwith "uncompatible types"
-	)
-) and match_out_type anytab tres = (
-	match tres with
-		TEFF_any (k, _) -> (
-			try (
-				Util.hfind anytab k
-			) with Not_found -> (
-				failwith "uncompatible types"					
-			)
-		) | _ -> tres
+	 )
+and match_out_type anytab tres = (
+  match tres with
+	 TEFF_any (k, _) -> (
+		try (
+		  Util.hfind anytab k
+		) with Not_found -> (
+			 failwith "uncompatible types"					
+		  )
+	 ) | _ -> tres
 )

lutin/src/ckTypeEff.mli

@@ -25,6 +25,7 @@ type t =
 |  TEFF_except
 |  TEFF_trace
 |  TEFF_data of basic
+|  TEFF_list of basic
 |  TEFF_tuple of basic list
 |	TEFF_any of string * any_cond
 |	TEFF_ref of basic
@@ -97,6 +98,7 @@ val prof_bt_t  : profile
 val prof_iit_t  : profile
 val prof_b_b  : profile
 val prof_bb_b  : profile
+val prof_bl_b  : profile
 val prof_ii_i  : profile
 val prof_iii_i  : profile
 

lutin/src/exp.ml

@@ -59,6 +59,9 @@ and formula =
   | And  of formula * formula
   | Or   of formula * formula
   | Xor  of formula * formula
+  | NXor of formula list
+  | Nor  of formula list
+  | Diese of formula list
   | Impl of formula * formula
   | IteB of formula * formula * formula
   | Not  of formula
@@ -251,8 +254,12 @@ let rec (simplifie_a_little : formula -> formula) =
 	         else
 	           f12'
       | Xor(f1, f2) -> Xor(simplifie_a_little f1, simplifie_a_little f2)
+      | NXor fl -> NXor(List.map simplifie_a_little fl)
+      | Nor fl -> Nor(List.map simplifie_a_little fl)
+      | Diese fl -> Diese(List.map simplifie_a_little fl)
       | Impl(f1, f2) -> Impl(simplifie_a_little f1, simplifie_a_little f2)
-      | IteB(f1, f2, f3) -> IteB(simplifie_a_little f1, simplifie_a_little f2, simplifie_a_little f3)
+      | IteB(f1, f2, f3) -> IteB(simplifie_a_little f1, simplifie_a_little f2,
+                                 simplifie_a_little f3)
       | Not(f1) -> Not(simplifie_a_little f1)
       | EqB(f1, f2) -> EqB(simplifie_a_little f1, simplifie_a_little f2)
 
@@ -293,7 +300,9 @@ and (f2s : int -> formula -> string) =
 	           (i2tab i)  ^ "xor \n" ^ 
 	           (f2s i f2) ^ "\n" ^ 
 	           (i2tab i)  ^ ")"
-
+        | NXor fl -> (i2tab i) ^ "xor(" ^ (String.concat "," (List.map (f2s i) fl)) ^ ")" 
+        | Nor fl -> (i2tab i) ^ "nor(" ^ (String.concat "," (List.map (f2s i) fl)) ^ ")" 
+        | Diese fl -> (i2tab i) ^ "#(" ^ (String.concat "," (List.map (f2s i) fl)) ^ ")" 
         | Impl(f1, f2) ->
 	         (i2tab i)  ^ "(\n" ^ 
 	           (f2s i f1) ^ "\n" ^

lutin/src/exp.mli

@@ -25,6 +25,9 @@ and formula =
   | And  of formula * formula
   | Or   of formula * formula
   | Xor  of formula * formula
+  | NXor of formula list
+  | Nor  of formula list
+  | Diese of formula list
   | Impl of formula * formula
   | IteB of formula * formula * formula
   | Not  of formula

lutin/src/formula_to_bdd.ml

@@ -290,6 +290,68 @@ type comp = SupZero | SupEqZero | EqZero
    it's just an heuristic anyway
 *)
 
+let rec translate_nor fl =
+  assert (fl <> []);
+  let aux facc f = And(facc, Not(f)) in
+  List.fold_left aux (Not (List.hd fl)) (List.tl fl)
+  
+let rec translate_nary_and fl = (* n-ary "and" *)
+  assert (fl <> []);
+  let aux facc f = And(facc, f) in
+  List.fold_left aux (List.hd fl) (List.tl fl)
+  
+let rec translate_nary_or fl = (* n-ary "or" *)
+  assert (fl <> []);
+  let aux facc f = Or(facc, f) in
+  List.fold_left aux (List.hd fl) (List.tl fl)
+  
+let translate_nxor fl =
+  let n = List.length fl in
+  let split i l =
+    let rec aux i acc = function
+    | [] -> assert false
+    | x::tail -> if i = 0 then x, List.rev_append acc tail else aux (i-1) (x::acc) tail
+    in
+    aux i [] l
+  in
+  let rec aux acc i =
+    if i = n then acc else
+      let cur =
+        let x,l = split i fl in
+        And(x, Nor(l))
+      in
+      let acc = Or(cur, acc) in
+      aux acc (i+1)
+  in
+  aux False 0
+    
+let translate_nxor_alt fl =
+  (* Using the following formula:
+     XOR(ϕ1,ϕ2,...,ϕn) = OR(ϕ1,ϕ2,...,ϕn) ∧ AND ¬(ϕi∧ϕj)
+                                             i<j≤n             
+
+ It uses twice less connectors than the previous one, but it happens to be 10x slower!
+*)
+  assert (fl <> []);
+  let or_part = translate_nary_or fl in
+  let gen_pairs l =
+    let rec aux acc l =
+      match l with
+      | [] -> acc
+      | x::tail ->
+        let cur_pairs = List.map (fun y -> x,y) tail in
+        let acc = List.rev_append cur_pairs acc in
+        aux acc tail 
+    in
+    aux [] l
+  in
+  let pairs: (Exp.formula * Exp.formula) list = gen_pairs fl in
+  let pairs: Exp.formula list = List.map (fun (f1, f2) -> Not(And(f1,f2))) pairs in
+  let and_part = translate_nary_and pairs in
+  And(or_part, and_part)
+
+let translate_diese fl = Or(translate_nor fl, translate_nxor fl)
+
 
 let rec (translate_do : t -> Var.env_in -> Var.env -> string -> int -> Exp.formula ->
          t * Bdd.t * bool) =
@@ -324,6 +386,9 @@ let rec (translate_do : t -> Var.env_in -> Var.env -> string -> int -> Exp.formu
           let (t, bdd2, dep2) = (translate_do t input memory ctx_msg vl f2) in 
           (t, Bdd.xor bdd1 bdd2, dep1 || dep2)
 
+        | NXor(fl) -> translate_do t input memory ctx_msg vl (translate_nxor fl)
+        | Diese(fl) -> translate_do t input memory ctx_msg vl (translate_diese fl)
+        | Nor(fl) -> translate_do t input memory ctx_msg vl (translate_nor fl)
         | IteB(f1, f2, f3) ->
           let (t, bdd1, dep1) = (translate_do t input memory ctx_msg vl f1) in
           let (t, bdd2, dep2) = (translate_do t input memory ctx_msg vl f2) in

lutin/src/glue.ml

@@ -56,151 +56,156 @@ let lucky_exp_of (eval:bool) (id2exp:id2exp) (e: CoAlgExp.t) = (
   (* recursive any type translator *) 
   let rec _lucky_exp_of e = (
 	 let t = CoAlgExp.get_type e in
-		if t = CkTypeEff.boolean then
-		  Exp.Formu (_lucky_formula_of e)
-		else if t = CkTypeEff.integer then 
-		  Exp.Numer (_lucky_numexp_of e)
-		else if t = CkTypeEff.real then
-		  Exp.Numer (_lucky_numexp_of e)
-		else  failwith ("XXX :"^(CkTypeEff.to_string t)^":"^(CoAlgExp.lus_dumps e)^"\n")
-	     
+	 if t = CkTypeEff.boolean then
+		Exp.Formu (_lucky_formula_of e)
+	 else if t = CkTypeEff.integer then 
+		Exp.Numer (_lucky_numexp_of e)
+	 else if t = CkTypeEff.real then
+		Exp.Numer (_lucky_numexp_of e)
+	 else  failwith ("XXX :"^(CkTypeEff.to_string t)^":"^(CoAlgExp.lus_dumps e)^"\n")
+
   )
-	 (* recursive bool translator *) 
+  (* recursive bool translator *) 
   and _lucky_formula_of e = (
 	 let raw_res = (
 		let nat = e.CoAlgExp.ae_val in
-		  match nat with
-			 |	CoAlgExp.AE_true -> Exp.True
-			 |	CoAlgExp.AE_false -> Exp.False
-			 |	CoAlgExp.AE_pre id 
-			 |	CoAlgExp.AE_support id
-			 |	CoAlgExp.AE_alias id -> (
-				  match id2exp eval nat with
-				    |	Exp.Formu f -> f
-				    |	e -> (
-					     let msg = "unexpected exp type for var \""^(CoIdent.to_string id)^"\""^
-					       "     bool exp is expected but get \""^(Exp.to_string e)^"\""
-					     in
-					       raise (LutErrors.Internal_error ("Glue.lucky_formula_of", msg))
-				      )
-			   )
-			 |	CoAlgExp.AE_call (id, ops) -> (
-				  match (id, ops) with
-				    |	("not", [o])     -> Exp.Not (_lucky_formula_of o)
-				    |	("and", [o1;o2]) -> Exp.And (_lucky_formula_of o1, _lucky_formula_of o2)
-				    |	("or", [o1;o2])  -> Exp.Or (_lucky_formula_of o1, _lucky_formula_of o2)
-				    |	("xor", [o1;o2]) -> Exp.Xor (_lucky_formula_of o1, _lucky_formula_of o2)
-				    |	("impl", [o1;o2])   -> Exp.Impl (_lucky_formula_of o1, _lucky_formula_of o2)
-				    |	("ite", [o1;o2;o3]) -> Exp.IteB (_lucky_formula_of o1, _lucky_formula_of o2, _lucky_formula_of o3)
-				    |	("lt", [o1;o2])   -> Exp.Inf (_lucky_numexp_of o1, _lucky_numexp_of o2)
-				    |	("lte", [o1;o2])  -> Exp.InfEq (_lucky_numexp_of o1, _lucky_numexp_of o2)
-				    |	("gt", [o1;o2])   -> Exp.Sup (_lucky_numexp_of o1, _lucky_numexp_of o2)
-				    |	("gte", [o1;o2])  -> Exp.SupEq (_lucky_numexp_of o1, _lucky_numexp_of o2)
-				    |	("neq", [o1;o2])
-				    |	("eq", [o1;o2])   -> (
-					     let ty = CoAlgExp.get_type o1 in
-					     let eqexp = if (ty = CkTypeEff.boolean ) then
-						    Exp.EqB (_lucky_formula_of o1, _lucky_formula_of o2)
-					     else if ((ty = CkTypeEff.integer) || (ty = CkTypeEff.real)) then (
-						    Exp.Eq (_lucky_numexp_of o1, _lucky_numexp_of o2)
-					     ) else (
-						    assert false
-					     ) in
-					       if (id = "neq") then Exp.Not eqexp else eqexp
-				      )
-				    | _ -> assert false	
-			   )
-			 |	CoAlgExp.AE_rconst x ->
-				  raise (LutErrors.Internal_error ( "lucky_formula_of", "unexpected AE_rconst "^x^" CoAlgExp.t" ))
-			 |	CoAlgExp.AE_iconst x ->
-				  raise (LutErrors.Internal_error ( "lucky_formula_of", "unexpected AE_iconst "^x^" CoAlgExp.t" ))
-			 |	CoAlgExp.AE_rval x ->
-				  raise (LutErrors.Internal_error ( "lucky_formula_of", "unexpected AE_rval "^(string_of_float x)^" CoAlgExp.t" ))
-			 |	CoAlgExp.AE_ival x ->
-				  raise (LutErrors.Internal_error ( "lucky_formula_of", "unexpected AE_ival "^
-                                               (string_of_int x)^" CoAlgExp.t" ))
-			 |	CoAlgExp.AE_const x ->
-				  raise (LutErrors.Internal_error ( "lucky_formula_of", "unexpected AE_const "^x^" CoAlgExp.t" ))
-			 |  CoAlgExp.AE_external_call (id, ei, prof, ops) -> (
-				   raise ( LutErrors.Internal_error (
-					          "Glue.lucky_formula_of",
-					          "sorry, bool type in external function not yet implemented"))
-			    )
+		match nat with
+		|	CoAlgExp.AE_true -> Exp.True
+		|	CoAlgExp.AE_false -> Exp.False
+		|	CoAlgExp.AE_pre id 
+		|	CoAlgExp.AE_support id
+		|	CoAlgExp.AE_alias id -> (
+			 match id2exp eval nat with