explicit forbidden with enumeration :

TPTP/simplify : explicit not anymore the default

CHANGES

 
+  o TPTP : encoding is not anymore the default for tptp provers.
+  It is now forbidden to use explicit with enumeration.
   o [IDE] source file names are stored in database as relative paths
     to the database, so that databases are now easier to move from a
     machine to another (e.g when they are stored in source control

drivers/simplify.drv

@@ -67,12 +67,12 @@ theory int.Int
   remove prop CompatOrderAdd
 
   (* use with explicit polymorphism *)
-  meta "enco_poly" "explicit"
+  (* meta "enco_poly" "explicit" *)
   meta "encoding : base" type int
 
   (* use with encoding_decorate *)
-  (* meta "enco_poly" "decorate" *)
-  (* meta "encoding : kept" type int *)
+  meta "enco_poly" "decorate"
+  meta "encoding : kept" type int
 
 end
 

src/core/printer.ml

@@ -194,6 +194,7 @@ let query_syntax sm id = Mid.find_option id sm
 
 (** {2 exceptions to use in transformations and printers} *)
 
+exception UnsupportedTysymbol   of tysymbol   * string
 exception UnsupportedType of ty   * string
 exception UnsupportedExpr of expr * string
 exception UnsupportedDecl of decl * string
@@ -202,6 +203,7 @@ exception Unsupported     of        string
 
 (** {3 functions that catch inner error} *)
 
+let unsupportedTysymbol   e s = raise (UnsupportedTysymbol (e,s))
 let unsupportedType e s = raise (UnsupportedType (e,s))
 let unsupportedTerm e s = raise (UnsupportedExpr (Term e,s))
 let unsupportedFmla e s = raise (UnsupportedExpr (Fmla e,s))
@@ -213,6 +215,9 @@ let unsupported       s = raise (Unsupported s)
 let catch_unsupportedType f e =
   try f e with Unsupported s -> unsupportedType e s
 
+let catch_unsupportedTysymbol f e =
+  try f e with Unsupported s -> unsupportedTysymbol e s
+
 let catch_unsupportedTerm f e =
   try f e with Unsupported s -> unsupportedTerm e s
 
@@ -245,6 +250,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
   | UnsupportedType (e,s) ->
       fprintf fmt "@[<hov 3> This type isn't supported:@\n%a@\n%s@]"
         Pretty.print_ty e s
+  | UnsupportedTysymbol (e,s) ->
+      fprintf fmt "@[<hov 3> This type isn't supported:@\n%a@\n%s@]"
+        Pretty.print_ts e s
   | UnsupportedExpr (e,s) ->
       fprintf fmt "@[<hov 3> This expression isn't supported:@\n%a@\n%s@]"
         Pretty.print_expr e s

src/core/printer.mli

@@ -66,11 +66,13 @@ val syntax_arguments : string -> 'a pp -> 'a list pp
 
 (** {2 exceptions to use in transformations and printers} *)
 
+exception UnsupportedTysymbol   of tysymbol   * string
 exception UnsupportedType of ty   * string
 exception UnsupportedExpr of expr * string
 exception UnsupportedDecl of decl * string
 exception NotImplemented  of        string
 
+val unsupportedTysymbol   : tysymbol   -> string -> 'a
 val unsupportedType : ty   -> string -> 'a
 val unsupportedTerm : term -> string -> 'a
 val unsupportedFmla : fmla -> string -> 'a
@@ -91,6 +93,11 @@ val catch_unsupportedType : (ty -> 'a) -> (ty -> 'a)
     - return [f arg] if [f arg] does not raise {!Unsupported} exception
     - raise [UnsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)
 
+
+val catch_unsupportedTysymbol : (tysymbol -> 'a) -> (tysymbol -> 'a)
+(** same as {! catch_unsupportedType} but use [UnsupportedTysymbol]
+    instead of [UnsupportedType]*)
+
 val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a)
 (** same as {! catch_unsupportedType} but use [UnsupportedExpr]
     instead of [UnsupportedType]*)

src/transform/encoding.ml

@@ -45,7 +45,7 @@ let kept_opt,register_enco_kept = enco_opt "kept" "bridge"
 let poly_opt,register_enco_poly = enco_opt "poly" "decorate"
 
 let poly_smt_opt = poly_opt
-let poly_tptp_opt = { poly_opt with default = "explicit" }
+let poly_tptp_opt = poly_opt
 
 let enco_gen opt env =
   Trans.on_meta_excl opt.meta (fun alo ->
@@ -64,15 +64,29 @@ let enco_kept = enco_gen kept_opt
 let enco_poly_smt = enco_gen poly_smt_opt
 let enco_poly_tptp = enco_gen poly_tptp_opt
 
-let maybe_encoding_enumeration =
+let forbid_for_explicit =
+  Encoding_enumeration.forbid_enumeration
+    "explicit is unsound in presence of this finite type"
+
+let maybe_forbid_enumeration =
+  Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
+    let s = match alo with
+      | None -> poly_smt_opt.default
+      | Some [MAstr s] -> s
+      | _ -> assert false in
+    if s = "explicit"
+    then forbid_for_explicit
+    else Trans.identity)
+
+let forbid_enumeration =
   Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
     let s = match alo with
       | None -> poly_smt_opt.default
       | Some [MAstr s] -> s
       | _ -> assert false in
     if s = "explicit"
-    then Encoding_enumeration.encoding_enumeration
-    else identity)
+    then forbid_for_explicit
+    else Encoding_enumeration.encoding_enumeration)
 
 
 open Ty
@@ -99,13 +113,13 @@ let monomorphise_goal =
 
 let encoding_smt env =
   compose monomorphise_goal
-    (compose maybe_encoding_enumeration
+    (compose maybe_forbid_enumeration
        (compose (enco_select env)
           (compose (enco_kept env) (enco_poly_smt env))))
 
 let encoding_tptp env =
   compose monomorphise_goal
-    (compose Encoding_enumeration.encoding_enumeration
+    (compose forbid_enumeration
        (compose (enco_select env)
           (compose (enco_kept env) (enco_poly_tptp env))))
 

src/transform/encoding.mli

@@ -32,7 +32,7 @@ val register_enco_poly : string -> (env -> task trans) -> unit
 
 
 val monomorphise_goal : Task.task Trans.trans
-val maybe_encoding_enumeration : Task.task Trans.trans
+val maybe_forbid_enumeration : Task.task Trans.trans
 
 val enco_poly_smt : Env.env -> Task.task Trans.trans
 val print_kept : Task.task Trans.trans

src/transform/encoding_arrays.ml

@@ -576,7 +576,7 @@ let encoding_smt_array env =
   Trans.on_used_theory th_array (fun used ->
     if not used then Encoding.encoding_smt env else
       compose Encoding.monomorphise_goal
-        (compose Encoding.maybe_encoding_enumeration
+        (compose Encoding.maybe_forbid_enumeration
            (compose (select_subterm_array th_array)
               (compose Encoding.print_kept
                  (compose (Encoding_instantiate.t

src/transform/encoding_enumeration.ml

@@ -93,5 +93,10 @@ let encoding_enumeration =
     let tenv = { enum = enum ; projs = projs } in
     Trans.decl (decl tenv) None)
 
+let forbid_enumeration s =
+  Trans.on_tagged_ts meta_enum (fun enum ->
+    if Sts.is_empty enum then Trans.identity
+    else Printer.unsupportedTysymbol (Sts.choose enum) s)
+
 let () = Trans.register_transform "encoding_enumeration" encoding_enumeration
 

src/transform/encoding_enumeration.mli

@@ -18,3 +18,6 @@
 (**************************************************************************)
 
 val encoding_enumeration : Task.task Trans.trans
+val forbid_enumeration   : string ->Task.task Trans.trans
+(* [forbid_enumeration s] if the task contains encoded enumeration
+   unsupportedTysymbol is raised with the message [s] *)