Add language extensions in the parsing of smtlib2

CHANGES.md

@@ -2,6 +2,20 @@
 next
 ----
 
+### UI
+
+- Improved the printing of some data-structures (PR#190)
+
+### Std
+
+- Replace the `Plain` statement with the `Other` statement,
+  which is a more general version (PR#190)
+
+### Parsing
+
+- Add parsing extensions for the smtlib2 language (PR#190)
+- Better split elements of clauses in `cnf` TPTP statements (PR#190)
+
 ### Typing
 
 - Enforce some missing constraints on bitvectors

doc/parsing.md

@@ -47,6 +47,7 @@ and try to parse a file named "example.smt2" in the home of the current user:
 module P =
   Dolmen.Smtlib2.Script.Latest.Make
     (Dolmen.Std.Loc)(Dolmen.Std.Id)(Dolmen.Std.Term)(Dolmen.Std.Statement)
+    (Dolmen.Std.Extensions.Smtlib2)
 
 let _ = P.parse_file "example.smt2"
 ```

doc/tuto.md

@@ -16,7 +16,7 @@ the following code will give you a quick start:
 open Dolmen
 
 (* Instantiate a module for parsing logic languages *)
-module Logic = Class.Logic.Make(Std.Loc)(Std.Id)(Std.Term)(Std.Statement)
+module Logic = Class.Logic.Make(Std.Loc)(Std.Id)(Std.Term)(Std.Statement)(Std.Extensions)
 
 (* instantiate the modules for typechecking *)
 module State = Dolmen_loop.State

src/bin/man.ml

@@ -9,6 +9,8 @@ let cli = [
   `P "Dolmen is a tool to parse and type input files that contain problem \
       used in automated deduction.";
   `S Options.common_section;
+  `P "Generic options for CLI binaries";
+  `S Options.option_section;
   `P "Common options for the dolmen binary";
   `S Options.model_section;
   `P "Options to use dolmen to verify models output by provers";
@@ -39,6 +41,8 @@ let cli = [
      );
   `S Options.gc_section;
   `P "Options to fine-tune the gc, only experts should use these.";
+  `S Options.internal_section;
+  `P "Options for internal testing of Dolmen, use at your own risks, ^^";
   `S Cmdliner.Manpage.s_exit_status;
   `P "dolmen exits with the following status:";
   `S Cmdliner.Manpage.s_bugs;

src/bin/options.ml

@@ -11,8 +11,10 @@ let model_section = "MODEL CHECKING"
 let error_section = "ERROR HANDLING"
 let flow_section = "FLOW CHECKING"
 let header_section = "HEADER CHECKING"
-let common_section = Manpage.s_options
+let option_section = Manpage.s_options
+let common_section = Manpage.s_common_options
 let profiling_section = "PROFILING"
+let internal_section = "INTERNAL"
 
 (* Initialise error codes *)
 (* ************************************************************************* *)
@@ -119,20 +121,6 @@ let input_mode_list = [
 
 let input_mode_conv = Arg.enum input_mode_list
 
-(* Check model modes *)
-(* ************************************************************************* *)
-
-(*
-type model_mode = Dolmen_model.Loop.mode
-
-let model_mode_list = [
-    "full", Dolmen_model.Loop.Full;
-    "interleave", Dolmen_model.Loop.Interleave;
-  ]
-
-let model_mode_conv = Arg.enum model_mode_list
-*)
-
 (* Mnemonic converter *)
 (* ************************************************************************ *)
 
@@ -280,7 +268,7 @@ let report_style =
   ]
 
 
-(* Smtlib2 logic *)
+(* Smtlib2 logic and extensions *)
 (* ************************************************************************ *)
 
 let smtlib2_logic =
@@ -293,6 +281,13 @@ let smtlib2_logic =
   let print fmt _s = Format.fprintf fmt "" in
   Arg.conv (parse, print)
 
+let smtlib2_ext_list =
+  List.map
+    (fun ext -> Dolmen_std.Extensions.Smtlib2.name ext, ext)
+    (Dolmen_std.Extensions.Smtlib2.exts ())
+
+let smtlib2_ext =
+  Arg.enum smtlib2_ext_list
 
 
 (* State creation *)
@@ -359,13 +354,15 @@ let mk_run_state
     flow_check
     header_check header_licenses
     header_lang_version
-    smtlib2_forced_logic type_check check_model (* check_model_mode *)
+    smtlib2_forced_logic smtlib2_exts
+    type_check check_model (* check_model_mode *)
     debug report_style max_warn reports syntax_error_ref
   =
   (* Side-effects *)
   let () = Option.iter Gc.set gc_opt in
   let () = set_color Unix.stdout Format.std_formatter colors in
   let () = set_color Unix.stderr Format.err_formatter colors in
+  let () = List.iter Dolmen_std.Extensions.Smtlib2.enable smtlib2_exts in
   (* base (which is a transitive dependency, due to farith),
      unconditionally enables backtraces, which is fine. But that means that
      for our purpose, we need to store whether to print the backtraces somewhere
@@ -477,7 +474,7 @@ let mk_file lang mode input =
   Loop.State.mk_file ?lang ?mode dir source
 
 let logic_file =
-  let docs = common_section in
+  let docs = option_section in
   let in_lang =
     let doc = Format.asprintf
         "Set the input language to $(docv); must be %s."
@@ -529,7 +526,7 @@ let mk_preludes =
   List.map (fun f -> mk_file None None (`File f))
 
 let preludes =
-  let docs = common_section in
+  let docs = option_section in
   let preludes =
     let doc = "Optional prelude file to be loaded before the input file." in
     Arg.(value & opt_all string [] & info ["p"; "prelude"] ~doc ~docs)
@@ -540,7 +537,7 @@ let preludes =
 (* ************************************************************************* *)
 
 let state =
-  let docs = common_section in
+  let docs = option_section in
   let gc =
     let doc = "Print statistics about the gc upon exiting" in
     Arg.(value & flag & info ["g"; "gc"] ~doc ~docs:gc_section)
@@ -550,8 +547,10 @@ let state =
     Arg.(value & flag & info ["b"; "backtrace"] ~doc ~docs:error_section)
   in
   let colors =
-    let doc = "Activate coloring of output" in
-    Arg.(value & opt color_conv Auto & info ["color"] ~doc ~docs)
+    let doc =
+      "Activate coloring of output. Available options are: auto, always, never."
+    in
+    Arg.(value & opt color_conv Auto & info ["color"] ~doc ~docs:common_section)
   in
   let abort_on_bug =
     let doc = Format.asprintf
@@ -606,6 +605,14 @@ let state =
                the one given on the command line." in
     Arg.(value & opt (some smtlib2_logic) None & info ["force-smtlib2-logic"] ~doc ~docs)
   in
+  let smtlib2_extensions =
+    let doc = Format.asprintf
+        "Activate smtlib2 extension. Currently an experimental option. \
+        $(docv) must be %s" (Arg.doc_alts_enum smtlib2_ext_list)
+    in
+    Arg.(value & opt_all smtlib2_ext [] &
+         info ["internal-smtlib2-extension"] ~docs:internal_section ~doc)
+  in
   let debug =
     let doc = Format.asprintf
         "Activate debug mode. Among other things, this will make dolmen \
@@ -668,14 +675,16 @@ let state =
         flow_check $
         header_check $ header_licenses $
         header_lang_version $
-        force_smtlib2_logic $ typing $ check_model $ (* check_model_mode $ *)
+        force_smtlib2_logic $ smtlib2_extensions $
+        typing $ check_model $ (* check_model_mode $ *)
         debug $ report_style $ max_warn $ reports $ syntax_error_ref)
 
 
 (* List command term *)
 (* ************************************************************************* *)
 
 let cli =
+  let docs = option_section in
   let aux state preludes logic_file list doc =
     match list, doc with
     | false, None ->
@@ -694,10 +703,10 @@ let cli =
   let list =
     let doc = "List all reports (i.e. warnings and errors),
                that dolmen can emit." in
-    Arg.(value & flag & info ["list"] ~doc)
+    Arg.(value & flag & info ["list"] ~doc ~docs)
   in
   let doc =
     let doc = "The warning or error of which to show the documentation." in
-    Arg.(value & opt (some mnemonic_conv) None & info ["doc"] ~doc ~docv:"mnemonic")
+    Arg.(value & opt (some mnemonic_conv) None & info ["doc"] ~doc ~docv:"mnemonic" ~docs)
   in
   Term.(ret (const aux $ state $ preludes $ logic_file $ list $ doc))

src/classes/logic.ml

@@ -54,6 +54,9 @@ module Make
     (S : Dolmen_intf.Stmt.Logic with type location := L.t
                                  and type id := I.t
                                  and type term := T.t)
+    (E : Dolmen_intf.Ext.Logic with type location := L.t
+                                and type term := T.t
+                                and type statement := S.t)
   : S with type file := L.file
        and type statement := S.t
 = struct
@@ -103,9 +106,9 @@ module Make
 
     (* Smtlib2 *)
     Smtlib2 `Latest, ".smt2",
-    (module Dolmen_smtlib2.Script.Latest.Make(L)(I)(T)(S) : S);
+    (module Dolmen_smtlib2.Script.Latest.Make(L)(I)(T)(S)(E.Smtlib2) : S);
     Smtlib2 `V2_6, ".smt2",
-    (module Dolmen_smtlib2.Script.V2_6.Make(L)(I)(T)(S) : S);
+    (module Dolmen_smtlib2.Script.V2_6.Make(L)(I)(T)(S)(E.Smtlib2) : S);
     Smtlib2 `Poly, ".psmt2",
     (module Dolmen_smtlib2.Script.Poly.Make(L)(I)(T)(S) : S);
 

src/classes/logic.mli

@@ -112,5 +112,8 @@ module Make
     (S : Dolmen_intf.Stmt.Logic with type location := L.t
                                  and type id := I.t
                                  and type term := T.t)
+    (E : Dolmen_intf.Ext.Logic with type location := L.t
+                                and type term := T.t
+                                and type statement := S.t)
   : S with type statement := S.t and type file := L.file
 

src/interface/dune

@@ -4,5 +4,5 @@
   (instrumentation (backend bisect_ppx))
   (libraries      menhirLib)
   (modules        Map Msg Tok Lex Parse Location
-                  Id Tag Ty Term Stmt Language)
+                  Id Tag Ty Term Stmt Ext Language)
 )

src/interface/ext.ml

@@ -0,0 +1,25 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+(** Interfaces for Extensions *)
+
+module type Logic = sig
+
+  type location
+  (** The type of locations. *)
+
+  type term
+  (** The type of terms *)
+
+  type statement
+  (** The type of statements *)
+
+  module Smtlib2 : sig
+
+    val statement : string -> (?loc:location -> term list -> statement) option
+    (** Called on statements of the form `(<id> <term>)` where `<id>` is
+        not the name of a statement in the official smtlib specification. *)
+
+  end
+
+end

src/languages/smtlib2/v2.6/script/ast.ml

@@ -8,6 +8,23 @@
     in an interactive loop (so it includes directive for getting and setting options,
     getting information about the solver's internal model, etc...) *)
 
+module type Extension = sig
+
+  type location
+  (** The type of locations. *)
+
+  type term
+  (** The type of terms *)
+
+  type statement
+  (** The type of statements *)
+
+  val statement : string -> (?loc:location -> term list -> statement) option
+  (** Called on statements of the form `(<id> <term>)` where `<id>` is
+      not the name of a statement in the official smtlib specification. *)
+
+end
+
 module type Id = sig
 
   type t

src/languages/smtlib2/v2.6/script/dolmen_smtlib2_v6_script.ml

@@ -4,16 +4,18 @@
 module type Id = Ast.Id
 module type Term = Ast.Term
 module type Statement = Ast.Statement
+module type Extension = Ast.Extension
 
 module Make
     (L : Dolmen_intf.Location.S)
     (I : Id)
     (T : Term with type location := L.t and type id := I.t)
-    (S : Statement with type location := L.t and type id := I.t and type term := T.t) =
+    (S : Statement with type location := L.t and type id := I.t and type term := T.t)
+    (E : Extension with type location := L.t and type term := T.t and type statement := S.t) =
   Dolmen_std.Transformer.Make(L)(struct
     type token = Tokens.token
     type statement = S.t
     let env = []
     let incremental = true
     let error s = Syntax_messages.message s
-  end)(Lexer)(Parser.Make(L)(I)(T)(S))
+  end)(Lexer)(Parser.Make(L)(I)(T)(S)(E))

src/languages/smtlib2/v2.6/script/dolmen_smtlib2_v6_script.mli

@@ -6,12 +6,14 @@
 module type Id = Ast.Id
 module type Term = Ast.Term
 module type Statement = Ast.Statement
+module type Extension = Ast.Extension
 (** Implementation requirement for the Smtlib format. *)
 
 module Make
     (L : Dolmen_intf.Location.S)
     (I : Id)
     (T : Term with type location := L.t and type id := I.t)
-    (S : Statement with type location := L.t and type id := I.t and type term := T.t) :
+    (S : Statement with type location := L.t and type id := I.t and type term := T.t)
+    (E : Extension with type location := L.t and type term := T.t and type statement := S.t) :
   Dolmen_intf.Language.S with type statement = S.t and type file := L.file
 (** Functor to generate a parser for the Smtlib format. *)

src/languages/smtlib2/v2.6/script/parser.mly

@@ -5,11 +5,13 @@
 %parameter <I : Ast.Id>
 %parameter <T : Ast.Term with type location := L.t and type id := I.t>
 %parameter <S : Ast.Statement with type location := L.t and type id := I.t and type term := T.t>
+%parameter <E : Ast.Extension with type location := L.t and type term := T.t and type statement := S.t>
 
 %start <T.t> term
 %start <S.t list> file
 %start <S.t option> input
 
+
 %{
 
   let pp_num_list fmt (l, singular, plural) =
@@ -453,6 +455,23 @@ command:
     { let loc = L.mk_pos $startpos $endpos in S.set_logic ~loc s }
   | OPEN SET_OPTION c=command_option CLOSE
     { let loc = L.mk_pos $startpos $endpos in S.set_option ~loc c }
+
+  | OPEN e=extension_statement l=s_expr* CLOSE
+    { let loc = Some (L.mk_pos $startpos $endpos) in
+      e ?loc l }
+;
+
+extension_statement:
+  | s=SYMBOL
+    { match E.statement s with
+      | Some mk_ext -> mk_ext
+      | None ->
+        let loc = L.mk_pos $startpos $endpos in
+        raise (L.Syntax_error (loc, `Advanced ("115",
+          Format.dprintf "a command",
+          Format.dprintf "the symbol '%s'" s,
+          Format.dprintf "a command name")))
+    }
 ;
 
 file: