From 0c8ac354e015c60ca92163a7ea75067e6368b1d8 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Wed, 11 Aug 2010 16:22:44 +0000 Subject: [PATCH] get rid of ps_neq (no citizen is special!) --- drivers/alt_ergo.drv | 1 - drivers/coq.drv | 1 - drivers/cvc3.drv | 1 - drivers/gappa.drv | 1 - drivers/simplify.drv | 1 - drivers/tptp.drv | 1 - drivers/tptp_simple.drv | 1 - drivers/why3.drv | 1 - drivers/why3_encoding_decorate.drv | 1 - drivers/why3_inline_all.drv | 1 - drivers/why3_total_elimination.drv | 1 - drivers/z3.drv | 1 - src/core/pretty.ml | 1 - src/core/term.ml | 10 +--------- src/core/term.mli | 2 -- src/core/theory.ml | 1 - src/parser/lexer.mll | 2 ++ src/parser/parser.mly | 8 +++++--- src/transform/encoding_simple.ml | 4 ++-- src/transform/explicit_polymorphism.ml | 4 ++-- src/transform/simplify_formula.ml | 11 ----------- 21 files changed, 12 insertions(+), 43 deletions(-) diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv index 53339c539..5f7349de5 100644 --- a/drivers/alt_ergo.drv +++ b/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 diff --git a/drivers/coq.drv b/drivers/coq.drv index 8e78e2306..4fb59163f 100644 --- a/drivers/coq.drv +++ b/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 diff --git a/drivers/cvc3.drv b/drivers/cvc3.drv index 5beee0d12..4748262ad 100644 --- a/drivers/cvc3.drv +++ b/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 diff --git a/drivers/gappa.drv b/drivers/gappa.drv index 5bcb1ce73..2e6407517 100644 --- a/drivers/gappa.drv +++ b/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 diff --git a/drivers/simplify.drv b/drivers/simplify.drv index 949b93737..82667b8ef 100644 --- a/drivers/simplify.drv +++ b/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 diff --git a/drivers/tptp.drv b/drivers/tptp.drv index 9cb86469a..26c0b8a5b 100644 --- a/drivers/tptp.drv +++ b/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 (* diff --git a/drivers/tptp_simple.drv b/drivers/tptp_simple.drv index 853b631c9..39d4c0913 100644 --- a/drivers/tptp_simple.drv +++ b/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 (* diff --git a/drivers/why3.drv b/drivers/why3.drv index e9fe598cf..7d7aa7e19 100644 --- a/drivers/why3.drv +++ b/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 diff --git a/drivers/why3_encoding_decorate.drv b/drivers/why3_encoding_decorate.drv index f9ee35e1e..53076db6b 100644 --- a/drivers/why3_encoding_decorate.drv +++ b/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 diff --git a/drivers/why3_inline_all.drv b/drivers/why3_inline_all.drv index 1aba27b0c..951803c3f 100644 --- a/drivers/why3_inline_all.drv +++ b/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 diff --git a/drivers/why3_total_elimination.drv b/drivers/why3_total_elimination.drv index e088ab9c3..9429fd97e 100644 --- a/drivers/why3_total_elimination.drv +++ b/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 diff --git a/drivers/z3.drv b/drivers/z3.drv index 7ee3d62f9..8a3b7d238 100644 --- a/drivers/z3.drv +++ b/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 diff --git a/src/core/pretty.ml b/src/core/pretty.ml index 23692a8e2..4ceeb293f 100644 --- a/src/core/pretty.ml +++ b/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 = diff --git a/src/core/term.ml b/src/core/term.ml index 58e968560..cb4c01ac4 100644 --- a/src/core/term.ml +++ b/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 diff --git a/src/core/term.mli b/src/core/term.mli index d9fbf0179..fb7c80290 100644 --- a/src/core/term.mli +++ b/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 diff --git a/src/core/theory.ml b/src/core/theory.ml index 137241e61..b0b5d6e97 100644 --- a/src/core/theory.ml +++ b/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 diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index 204554847..c295a6ee7 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -199,6 +199,8 @@ rule token = parse { BAR } | "=" { EQUAL } + | "<>" + { LTGT } | "[" { LEFTSQ } | "]" diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 1bda08073..755872ad1 100644 --- a/src/parser/parser.mly +++ b/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)) } diff --git a/src/transform/encoding_simple.ml b/src/transform/encoding_simple.ml index fc207c742..24e6fe9ce 100644 --- a/src/transform/encoding_simple.ml +++ b/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 diff --git a/src/transform/explicit_polymorphism.ml b/src/transform/explicit_polymorphism.ml index dd3c39ca7..35c86d6e0 100644 --- a/src/transform/explicit_polymorphism.ml +++ b/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 *) diff --git a/src/transform/simplify_formula.ml b/src/transform/simplify_formula.ml index 9e791dd7f..12897f315 100644 --- a/src/transform/simplify_formula.ml +++ b/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 -> -- GitLab