take care of the sign of the subformula

src/core/term.ml

@@ -436,7 +436,8 @@ let t_bvar n ty = Hsterm.hashcons (mk_term (Tbvar n) ty)
 let t_var v = Hsterm.hashcons (mk_term (Tvar v) v.vs_ty)
 let t_const c ty = Hsterm.hashcons (mk_term (Tconst c) ty)
 let t_int_const s = Hsterm.hashcons (mk_term (Tconst (ConstInt s)) Ty.ty_int)
-let t_real_const r = Hsterm.hashcons (mk_term (Tconst (ConstReal r)) Ty.ty_real)
+let t_real_const r = 
+  Hsterm.hashcons (mk_term (Tconst (ConstReal r)) Ty.ty_real)
 let t_app f tl ty = Hsterm.hashcons (mk_term (Tapp (f, tl)) ty)
 let t_if f t1 t2 = Hsterm.hashcons (mk_term (Tif (f, t1, t2)) t2.t_ty)
 let t_let v t1 t2 = Hsterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
@@ -946,6 +947,46 @@ let f_map fnT fnF f = f_label_copy f (match f.f_node with
       let blbl,bl' = map_fold_left (f_branch fnF) true bl in
       if tltl && blbl then f else f_case tl' bl')
 
+(* true pos, false neg *)
+let f_map_sign fnT fnF sign f = f_label_copy f (match f.f_node with
+  | Fapp (p, tl) -> f_app_unsafe p (List.map fnT tl)
+  | Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
+    (* TODO : the sign in a trigger ? *)
+      let f1' = fnF sign f1 in let tl' = tr_map fnT (fnF true) tl in
+      if f1' == f1 && tr_equal tl' tl then f
+      else f_quant q vl tl' f1'
+  | Fbinop (Fimplies, f1, f2) -> f_implies (fnF (not sign) f1) (fnF sign f2)
+  | Fbinop (Fiff, f1, f2) -> 
+      let f1p = fnF sign f1 in
+      let f1n = fnF (not sign) f1 in
+      let f2p = fnF sign f2 in
+      let f2n = fnF (not sign) f2 in
+      if f1p == f1n && f2p == f2n then f_iff f1p f2p else
+        if sign 
+        then f_and (f_implies f1n f2p) (f_implies f2n f1p)
+        else f_or  (f_and     f1p f2p) (f_and     f1n f2n)
+  | Fbinop (op, f1, f2) -> f_binary op (fnF sign f1) (fnF sign f2)
+  | Fnot f1 -> f_not (fnF (not sign) f1)
+  | Ftrue | Ffalse -> f
+  | Fif (f1, f2, f3) -> 
+      let f1p = fnF sign f1 in
+      let f1n = fnF (not sign) f1 in
+      let f2 = fnF sign f2 in
+      let f3 = fnF sign f3 in
+      if f1p == f1n then f_if f1p f2 f3
+      else if sign
+      then f_and (f_implies f1p f2) (f_implies (f_not f1n) f3)
+      else f_or (f_and (fnF sign f1) f2) (f_and (f_not f1n) f3)
+  | Flet (t, b) -> let u,f1 = f_open_bound b in
+      let t' = fnT t in let f1' = fnF sign f1 in
+      if t' == t && f1' == f1 then f else f_let u t' f1'
+  | Fcase (tl, bl) -> let tl' = List.map fnT tl in
+      let tltl = List.for_all2 (==) tl tl' in
+      let blbl,bl' = map_fold_left (f_branch (fnF sign)) true bl in
+      if tltl && blbl then f else f_case tl' bl')
+
+let f_map_pos fnT fnF f = f_map_sign fnT fnF true f
+
 let protect fn t =
   let res = fn t in
   if res.t_ty != t.t_ty then raise TypeMismatch;

src/core/term.mli

@@ -276,6 +276,16 @@ val f_neq : term -> term -> fmla
 val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
 val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
 
+val f_map_sign : 
+  (term -> term) -> (bool -> fmla -> fmla) -> bool -> fmla -> fmla
+(** give the sign of the sub_formula :
+    - true positive 
+    - false negative
+
+    nb : if_then_else, implies, iff are translated if needed *)
+val f_map_pos : 
+  (term -> term) -> (bool -> fmla -> fmla) -> fmla -> fmla
+
 val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
 val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a
 

src/printer/smt.ml

@@ -125,11 +125,11 @@ and print_fmla drv fmt f = match f.f_node with
   | Ffalse ->
       fprintf fmt "false"
   | Fif (f1, f2, f3) ->
-      fprintf fmt "@[(if_then_else %a@ %a@ %a@]"
+      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
 	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3
   | Flet (t1, tb) ->
       let v, f2 = f_open_bound tb in
-      fprintf fmt "@[(flet (%a %a)@ %a)@]" print_var v
+      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
         (print_term drv) t1 (print_fmla drv) f2;
       forget_var v
   | Fcase _ -> unsupportedExpression (Fmla f) 

src/transform/eliminate_constructs.ml

@@ -65,11 +65,13 @@ let merge_l f tl =
     (f_and_simp_l cond, f l)::acc in
   list_fold_product_l f [] tl
 
-let and_impl_f l =
-  (* TODO :
-     Use polarity in order to choose the most efficient translation of ite *)
-  List.fold_left (fun acc (c,f) -> f_and_simp acc (f_implies_simp c f)) 
+let and_impl_f sign l =
+  if sign 
+  then List.fold_left (fun acc (c,f) -> f_and_simp acc (f_implies_simp c f))
     f_true l
+  else  List.fold_left (fun acc (c,f) -> f_or_simp acc (f_and_simp c f))
+    f_false l
+    
 
 let rec remove_ite_t t =
   match t.t_node with
@@ -92,25 +94,25 @@ let rec remove_ite_t t =
         let tbl = merge_l (fun x -> x) tbl in
         merge (fun tl tbl -> t_case tl tbl t.t_ty) tl tbl
     | Teps fb ->
-        let vs,f = f_open_bound fb in [f_true,t_eps vs (remove_ite_f f)]
-and remove_ite_f f = 
+        let vs,f = f_open_bound fb in [f_true,t_eps vs (remove_ite_f true f)]
+and remove_ite_f sign f = 
   match f.f_node with
     | Fapp (ls,tl) ->
         let l = merge_l (f_app ls) (List.map remove_ite_t tl) in
-        and_impl_f l
+        and_impl_f sign l
     | Flet (t,fb) ->
         let vs,f' = f_open_bound fb in
-        let f'' = remove_ite_f f' in
+        let f'' = remove_ite_f sign f' in
         let tl = remove_ite_t t in
         begin match tl with
           | [c,_] when f' == f'' -> assert (c == f_true); f
           | _ -> 
               let tl = List.map (fun (c,t) -> c,f_let vs t f) tl in
-              and_impl_f tl
+              and_impl_f sign tl
         end
     | Fquant (q, b) -> 
         let vl, tl, f1 = f_open_quant b in
-        let f1' = remove_ite_f f1 in
+        let f1' = remove_ite_f sign f1 in
         let tr_map (changed,acc) = function
           | Term t as e -> 
               let tl = remove_ite_t t in
@@ -121,13 +123,13 @@ and remove_ite_f f =
                     List.fold_left (fun acc (_,t) -> Term t::acc) acc tl
               end
           | Fmla f as e ->
-              let f' = remove_ite_f f in
+              let f' = remove_ite_f true f in (*TODO trigger sign *)
               if f == f' then changed,e::acc else true,(Fmla f'::acc) in
         let changed,tl' = rev_map_fold_left 
           (fun acc -> List.fold_left tr_map (acc,[])) false tl in
         if f1' == f1 && (not changed) then f
         else f_quant q vl tl' f1'
-    | _ -> f_map (fun _ -> assert false) remove_ite_f f
+    | _ -> f_map_sign (fun _ -> assert false) remove_ite_f sign f
 
 let remove_ite_decl d =
   match d.d_node with
@@ -152,13 +154,13 @@ let remove_ite_decl d =
                             (create_prop_decl Paxiom pr f)::acc in
                             List.fold_left fax acc tl,d
                     end
-                | Fmla f -> acc,make_ls_defn ls vl (Fmla (remove_ite_f f))
+                | Fmla f -> acc,make_ls_defn ls vl (Fmla (remove_ite_f true f))
               end
           | ld -> acc,ld
         in
         let axs,l = (map_fold_left fn [] l) in
         (create_logic_decl l)::axs
-    | _ -> [decl_map (fun _ -> assert false) remove_ite_f d]
+    | _ -> [decl_map (fun _ -> assert false) (remove_ite_f true) d]
 
 let eliminate_ite = Register.store (fun () -> Trans.decl remove_ite_decl None)
 

src/transform/eliminate_constructs.mli

@@ -26,7 +26,8 @@ val eliminate_let : Task.task Register.trans_reg
 
 (** eliminate ite, ie if then else in term *)
 val remove_ite_t : Term.term -> (Term.fmla * Term.term) list
-val remove_ite_f : Term.fmla -> Term.fmla
+val remove_ite_f : bool -> Term.fmla -> Term.fmla
+(* [remove_ite_f sign f] *)
 val remove_ite_decl : Decl.decl -> Decl.decl list
 
 val eliminate_ite : Task.task Register.trans_reg