get rid of ps_neq (no citizen is special!)

drivers/alt_ergo.drv

@@ -28,7 +28,6 @@ theory BuiltIn
   syntax type int   "int"
   syntax type real  "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end
 
 theory int.Int

drivers/coq.drv

@@ -16,7 +16,6 @@ theory BuiltIn
   syntax type   int   "Z"
   syntax type   real  "R"
   syntax logic  (=)   "(%1 = %2)" 
-  syntax logic  (<>)  "(%1 <> %2)"
 end
 
 theory bool.Bool

drivers/cvc3.drv

@@ -26,7 +26,6 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
-  syntax logic (<>) "(not (= %1 %2))"
 end
 
 theory int.Int

drivers/gappa.drv

@@ -25,7 +25,6 @@ theory BuiltIn
   syntax type int   "int"
   syntax type real  "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end
 
 theory int.Int

drivers/simplify.drv

@@ -38,7 +38,6 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(EQ %1 %2)"
-  syntax logic (<>) "(NEQ %1 %2)"
 end
 
 theory int.Int

drivers/tptp.drv

@@ -35,7 +35,6 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 != %2)"
 end
 
 (*

drivers/tptp_simple.drv

@@ -36,7 +36,6 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 != %2)"
 end
 
 (*

drivers/why3.drv

@@ -5,5 +5,4 @@ theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end

drivers/why3_encoding_decorate.drv

@@ -14,5 +14,4 @@ theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end

drivers/why3_inline_all.drv

@@ -9,5 +9,4 @@ theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end

drivers/why3_total_elimination.drv

@@ -14,5 +14,4 @@ theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
-  syntax logic (<>) "(%1 <> %2)"
 end

drivers/z3.drv

@@ -27,7 +27,6 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
-  syntax logic (<>) "(not (= %1 %2))"
 end
 
 

src/core/pretty.ml

@@ -397,7 +397,6 @@ module NsTree = struct
       Leaf (sprint_pkind k ^ " " ^ s) :: acc in
     let add_ls s ls acc =
       if s = "infix ="  && ls_equal ls ps_equ then acc else
-      if s = "infix <>" && ls_equal ls ps_neq then acc else
         Leaf ("logic " ^ s) :: acc
     in
     let add_ts s ts acc =

src/core/term.ml

@@ -577,15 +577,8 @@ let ps_equ =
   let v = ty_var (create_tvsymbol (id_fresh "a")) in
   create_psymbol (id_fresh "infix =") [v; v]
 
-let ps_neq =
-  let v = ty_var (create_tvsymbol (id_fresh "a")) in
-  create_psymbol (id_fresh "infix <>") [v; v]
-
-let f_app p tl =
-  if ls_equal p ps_neq then f_not (f_app ps_equ tl) else f_app p tl
-
 let f_equ t1 t2 = f_app ps_equ [t1; t2]
-let f_neq t1 t2 = f_app ps_neq [t1; t2]
+let f_neq t1 t2 = f_not (f_app ps_equ [t1; t2])
 
 let fs_tuple n =
   let tyl = ref [] in
@@ -1763,7 +1756,6 @@ let f_branch fn b = let p,f,close = f_open_branch_cb b in close p (fn f)
 
 let f_map_simp fnT fnF f = f_label_copy f (match f.f_node with
   | Fapp (p, [t1;t2]) when ls_equal p ps_equ -> f_equ_simp (fnT t1) (fnT t2)
-  | Fapp (p, [t1;t2]) when ls_equal p ps_neq -> f_neq_simp (fnT t1) (fnT t2)
   | Fapp (p, tl) -> f_app p (List.map fnT tl)
   | Fquant (q, b) ->
       let vl, tl, f1, close = f_open_quant_cb b in

src/core/term.mli

@@ -337,8 +337,6 @@ val f_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
 
 (* equality predicate *)
 val ps_equ : lsymbol
-(* inequality predicate *)
-val ps_neq : lsymbol
 
 val f_equ : term -> term -> fmla
 val f_neq : term -> term -> fmla

src/core/theory.ml

@@ -678,7 +678,6 @@ let builtin_theory =
   let uc = add_ty_decl uc [ts_int, Tabstract] in
   let uc = add_ty_decl uc [ts_real, Tabstract] in
   let uc = add_logic_decl uc [ps_equ, None] in
-  let uc = add_logic_decl uc [ps_neq, None] in
   close_theory uc
 
 let create_theory n = use_export (empty_theory n) builtin_theory

src/parser/lexer.mll

@@ -199,6 +199,8 @@ rule token = parse
       { BAR }
   | "="
       { EQUAL }
+  | "<>"
+      { LTGT }
   | "["
       { LEFTSQ }
   | "]"

src/parser/parser.mly

@@ -70,7 +70,7 @@
 %token ARROW ASYM_AND ASYM_OR
 %token BAR
 %token COLON COMMA
-%token DOT EQUAL
+%token DOT EQUAL LTGT
 %token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
 %token LRARROW
 %token QUOTE
@@ -79,7 +79,6 @@
 
 %token EOF
 
-
 /* Precedences */
 
 %nonassoc prec_decls
@@ -93,7 +92,7 @@
 %right OR ASYM_OR
 %right AND ASYM_AND
 %nonassoc NOT
-%left EQUAL OP1
+%left EQUAL LTGT OP1
 %left OP2
 %left OP3
 %left OP4
@@ -358,6 +357,9 @@ lexpr:
 | lexpr EQUAL lexpr
    { let id = { id = infix "="; id_loc = loc_i 2 } in
      mk_pp (PPinfix ($1, id, $3)) }
+| lexpr LTGT lexpr
+   { let id = { id = infix "="; id_loc = loc_i 2 } in
+     prefix_pp PPnot (mk_pp (PPinfix ($1, id, $3))) }
 | lexpr OP1 lexpr
    { let id = { id = infix $2; id_loc = loc_i 2 } in
      mk_pp (PPinfix ($1, id, $3)) }

src/transform/encoding_simple.ml

@@ -92,7 +92,7 @@ let conv_vs tenv vs =
 
 (* Convert a logic symbol to the encoded one *)
 let conv_ls tenv ls =
-  if ls_equal ls ps_equ || ls_equal ls ps_neq then ls
+  if ls_equal ls ps_equ then ls
   else try Hls.find tenv.trans_lsymbol ls with Not_found ->
   let ty_res = Util.option_map (conv_ty tenv) ls.ls_value in
   let ty_arg = List.map (conv_ty tenv) ls.ls_args in
@@ -146,7 +146,7 @@ and rewrite_fmla tenv vm f =
   let fnT = rewrite_term tenv in
   let fnF = rewrite_fmla tenv in
   match f.f_node with
-  | Fapp (ps,tl) when ls_equal ps ps_equ || ls_equal ps ps_neq ->
+  | Fapp (ps,tl) when ls_equal ps ps_equ ->
       f_app ps (List.map (fnT vm) tl)
   | Fapp (ps,tl) ->
       let ps = conv_ls tenv ps in

src/transform/explicit_polymorphism.ml

@@ -67,7 +67,7 @@ module Transform = struct
   (** creates a new logic symbol, with a different type if the
   given symbol was polymorphic *)
   let logic_to_logic lsymbol =
-    if ls_equal lsymbol ps_equ || ls_equal lsymbol ps_neq then lsymbol else
+    if ls_equal lsymbol ps_equ then lsymbol else
     let new_ty = ls_ty_freevars lsymbol in
     (* as many t as type vars *)
     if Stv.is_empty new_ty then lsymbol (* same type *) else
@@ -113,7 +113,7 @@ module Transform = struct
   (** translation of formulae *)
   and fmla_transform tblT tblL varM f = match f.f_node with
       (* first case : predicate (not =), we must translate it and its args *)
-    | Fapp(p,terms) when not (ls_equal p ps_equ || ls_equal p ps_neq) ->
+    | Fapp(p,terms) when not (ls_equal p ps_equ) ->
       let terms = args_transform tblT tblL varM p terms None in
       f_app (findL tblL p) terms
     | _ -> (* otherwise : just traverse and translate *)

src/transform/simplify_formula.ml

@@ -64,21 +64,10 @@ let rec fmla_find_subst boundvars var sign f =
   let fnF = fmla_find_subst boundvars var in
   match f.f_node with
     | Fapp (ls,[{t_node=Tvar vs} as tv;t])
-        when sign && ls_equal ls ps_equ && vs_equal vs var 
-          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
-        raise (Subst_found t)
     | Fapp (ls,[t;{t_node=Tvar vs} as tv])         
         when sign && ls_equal ls ps_equ && vs_equal vs var 
           && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
         raise (Subst_found t)
-    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
-        when not sign && ls_equal ls ps_neq && vs_equal vs var 
-          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
-        raise (Subst_found t)
-    | Fapp (ls,[t;{t_node=Tvar vs} as tv]) 
-        when not sign && ls_equal ls ps_neq && vs_equal vs var 
-          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
-        raise (Subst_found t)
     | Fbinop (For, f1, f2)  when not sign -> (fnF sign f1); (fnF sign f2) 
     | Fbinop (Fand, f1, f2) when sign ->  (fnF sign f1); (fnF sign f2)
     | Fbinop (Fimplies, f1, f2) when not sign ->