Smtlib Printer

CHANGES.md

@@ -2,6 +2,18 @@
 next
 ----
 
+### UI
+
+- Add the export feature to the `dolmen` binary (PR#211)
+
+### Typing
+
+- Add a logic detection mechanism (PR#211)
+
+### Printing
+
+- Add printers for the SMT-LIB format (PR#211)
+
 ### Models
 
 - Fix a bug where the condition on evaluated goals was incorrect.

Makefile

@@ -17,7 +17,7 @@ top:
 doc:
 	dune build $(FLAGS) @doc
 
-gentests: $(filter-out $(wildcard tests/**/*.t/**/*),$(wildcard tests/**/*))
+gentests: tools/gentests.ml $(filter-out $(wildcard tests/**/*.t/**/*),$(wildcard tests/**/*))
 	dune exec -- tools/gentests.exe tests/
 
 test: gentests

TODO

@@ -0,0 +1,20 @@
+
+# Printing
+
+- Add comments
+- generate headers when printing to smtlib ?
+
+
+# Normalisation / transformation
+
+- add implicit base type decl (tptp's $i)
+- expand some unavailable builtins (i.e. pow/exponentiation is not available in smtlib)
+- scan terms and create and insert a set-logic
+- renaming of unused variables ? (insert a `_` at the start of the name)
+- simplify corner case of some translations (e.g. ae's `goal` is translated as push/assert-not/check-sat/pop,
+  but when there is only one in a problem, the pushs/pops are not needed)
+
+
+# Misc
+
+- maintain stack of locations for included files for error messages

dolmen_loop.opam

@@ -14,6 +14,7 @@ depends: [
   "dolmen_type" {= version }
   "dune" { >= "3.0" }
   "gen"
+  "zarith" { >= "1.10" }
   "pp_loc" { >= "2.0.0" }
   "odoc" { with-doc }
   "mdx" { with-test & >= "2.0.0" }

src/bin/loop.ml

@@ -10,3 +10,5 @@ module Flow = Dolmen_loop.Flow.Make(State)
 module Typer = Dolmen_loop.Typer.Typer(State)
 module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Typer)
 module Check = Dolmen_model.Loop.Make(State)(Parser)(Typer)(Typer_Pipe)
+module Export = Dolmen_loop.Export.Make(Dolmen.Std.Expr)(Dolmen_std.Term.View.Sexpr)(Dolmen_std.Expr.View.TFF)(State)(Typer_Pipe)
+module Transform = Dolmen_loop.Transform.Make(State)(Typer_Pipe)

src/bin/main.ml

@@ -59,15 +59,15 @@ let run st preludes logic_file =
           @>>> (op ~name:"typecheck" Loop.Typer_Pipe.typecheck)
           @>|> (op ~name:"debug-typed" debug_typed_pipe)
           @>>> (op ~name:"check" Loop.Check.check)
+          @>>> (op ~name:"transform" Loop.Transform.transform)
+          @>>> (op ~name:"export" Loop.Export.export)
           @>>> (op (fun st _ -> st, ())) @>>> _end
         )
       )
     )
   in
-  let st = Loop.Flow.finalise st in
-  let st = Loop.Header.check st in
-  let _st = Dolmen_loop.State.flush st () in
-  ()
+  let st = Dolmen_loop.State.flush st () in
+  ignore st
 
 (* Warning/Error list *)
 (* ****************** *)

src/bin/options.ml

@@ -28,6 +28,8 @@ let () =
     Dolmen_loop.Headers.code, 5;
     Dolmen_model.Loop.code, 6;
     Dolmen_loop.Flow.code, 7;
+    Dolmen_loop.Transform.code, 8;
+    Dolmen_loop.Export.code, 9;
   ]
 
 (* Main commands *)
@@ -36,8 +38,8 @@ let () =
 type cmd =
   | Run of {
       state : Loop.State.t;
-      preludes: Dolmen_loop.Logic.language Loop.State.file list;
-      logic_file : Dolmen_loop.Logic.language Loop.State.file;
+      preludes: Dolmen_loop.Logic.language Loop.State.input_file list;
+      logic_file : Dolmen_loop.Logic.language Loop.State.input_file;
     }
   | List_reports of {
       conf : Dolmen_loop.Report.Conf.t;
@@ -73,16 +75,19 @@ let set_color file_descr formatter color =
   Fmt.set_style_renderer formatter style
 
 
-(* Input format converter *)
+(* Input/Output format converter *)
 (* ************************************************************************* *)
 
 let input_format_conv = Arg.enum Dolmen_loop.Logic.enum
+let output_format_conv = Arg.enum Dolmen_loop.Export.enum
 let response_format_conv = Arg.enum Dolmen_loop.Response.enum
 
 
-(* Input source converter *)
+(* Input/Output source converter *)
 (* ************************************************************************* *)
 
+let output_dest_conv = Arg.string
+
 (* Converter for input file/stdin *)
 let input_to_string = function
   | `Stdin -> "<stdin>"
@@ -358,12 +363,29 @@ let reports_opts strict warn_modifiers =
   in
   `Ok res
 
+let split_input = function
+  | `Stdin ->
+    Sys.getcwd (), `Stdin
+  | `File f ->
+    Filename.dirname f, `File (Filename.basename f)
+
+let mk_output_file lang filename : Dolmen_loop.Export.file option =
+  match filename, lang with
+  | None, None -> None
+  | None, Some _ -> Some { lang; sink = `Stdout; }
+  | Some filename, _ -> Some { lang; sink = `File filename; }
+
+let mk_input_file lang mode input : _ Dolmen_loop.State.input_file =
+  let dir, source = split_input input in
+  { lang; mode; dir; source ;
+    loc = Dolmen.Std.Loc.mk_file ""; }
+
 let mk_run_state
     () gc gc_opt bt colors
     abort_on_bug
     time_limit size_limit
-    response_file
-    flow_check
+    response_file output_file
+    flow_check compute_logic
     header_check header_licenses header_lang_version
     smtlib2_forced_logic smtlib2_exts
     type_check extension_builtins
@@ -383,6 +405,13 @@ let mk_run_state
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
   let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
   let () = Hints.model ~check_model (* ~check_model_mode *) in
+  (* compute logic by default, but only do so if we are also exporting.
+     TODO: more control over this. (e.g. compute logic and emit warning/error
+     even without exporting, and also enable exporting without computing the logic). *)
+  let compute_logic =
+    compute_logic ||
+    (match output_file with Some _ -> true | None -> false)
+  in
   (* State creation *)
   Loop.State.empty
   |> Loop.State.init
@@ -400,6 +429,8 @@ let mk_run_state
     ~check_model
     (* ~check_model_mode *)
   |> Loop.Flow.init ~flow_check
+  |> Loop.Export.init ?output_file
+  |> Loop.Transform.init ~compute_logic
   |> Loop.Header.init
     ~header_check
     ~header_licenses
@@ -494,7 +525,7 @@ let logic_file =
         "Set the input language to $(docv); must be %s."
         (Arg.doc_alts_enum ~quoted:true Dolmen_loop.Logic.enum) in
     Arg.(value & opt (some input_format_conv) None &
-         info ["i"; "input"; "lang"] ~docv:"INPUT" ~doc ~docs)
+         info ["i"; "input"] ~docv:"INPUT" ~doc ~docs)
   in
   let in_mode =
     let doc = Format.asprintf
@@ -510,7 +541,7 @@ let logic_file =
                dolmen will enter interactive mode and read on stdin." in
     Arg.(value & pos 0 input_source_conv `Stdin & info [] ~docv:"FILE" ~doc)
   in
-  Term.(const mk_file $ in_lang $ in_mode $ input)
+  Term.(const mk_input_file $ in_lang $ in_mode $ input)
 
 let response_file =
   let docs = model_section in
@@ -534,7 +565,22 @@ let response_file =
     let doc = "Response file." in
     Arg.(value & opt input_source_conv `Stdin & info ["r"; "response"] ~doc ~docs)
   in
-  Term.(const mk_file $ response_lang $ response_mode $ response)
+  Term.(const mk_input_file $ response_lang $ response_mode $ response)
+
+let output_file =
+  let docs = common_section in
+  let lang =
+    let doc = Format.asprintf
+        "Set the export language to $(docv); must be %s."
+        (Arg.doc_alts_enum ~quoted:true Dolmen_loop.Export.enum) in
+    Arg.(value & opt (some output_format_conv) None &
+         info ["o"; "output"] ~docv:"OUTPUT" ~doc ~docs)
+  in
+  let output =
+    let doc = "Export file. If no file is specified, no export will be performed." in
+    Arg.(value & pos 1 (some output_dest_conv) None & info [] ~docv:"FILE" ~doc)
+  in
+  Term.(const mk_output_file $ lang $ output)
 
 let mk_preludes =
   List.map (fun f -> mk_file None None (`File f))
@@ -590,6 +636,13 @@ let state =
                This is mainly useful for the smtlib language." in
     Arg.(value & opt bool false & info ["check-flow"] ~doc ~docs:flow_section)
   in
+  let compute_logic =
+    let doc = "If true, then Dolmen will compute the minimal logic needed to typecheck \
+               all of the statements it has read, and emit a warning if that minimal logic \
+               is smaller than the logic used by the problem. This new logic will also be \
+               used during export to the smtlib2 format." in
+    Arg.(value & opt bool false & info ["compute-logic"] ~doc) (* TODO: new doc section *)
+  in
   let header_check =
     let doc = "If true, then the presence of headers will be checked in the
                input file (and errors raised if they are not present)." in
@@ -693,8 +746,8 @@ let state =
         gc $ gc_t $ bt $ colors $
         abort_on_bug $
         time $ size $
-        response_file $
-        flow_check $
+        response_file $ output_file $
+        flow_check $ compute_logic $
         header_check $ header_licenses $ header_lang_version $
         force_smtlib2_logic $ smtlib2_extensions $
         typing $ typing_ext $

src/interface/builtin.ml

@@ -0,0 +1,5 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+type 'a t = .. constraint 'a = < .. >
+

src/interface/dune

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

src/interface/env.ml

@@ -0,0 +1,40 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+module type Print_id = sig
+
+  type id
+  type env
+  type name
+
+  val bind : env -> id -> env
+  val name : env -> id -> name
+
+end
+
+module type Print = sig
+
+  type name
+
+  type ty
+  type ty_var
+  type ty_cst
+  type term
+  type term_var
+  type term_cst
+  type formula
+
+  type t
+
+  type 'a key
+
+  val key : unit -> 'a key
+  val get : t -> 'a key -> 'a option
+  val set : t -> 'a key -> 'a -> t
+
+  module Ty_var : Print_id with type env := t and type id := ty_var and type name := name
+  module Ty_cst : Print_id with type env := t and type id := ty_cst and type name := name
+  module Term_var : Print_id with type env := t and type id := term_var and type name := name
+  module Term_cst : Print_id with type env := t and type id := term_cst and type name := name
+
+end

src/interface/id.ml

@@ -58,18 +58,34 @@ end
 
 module type Response = Logic
 
-module type Escape = sig
+module type Scope = sig
 
   type t
   (** The type of identifiers. *)
 
-  val hash : t -> int
-  (** Hash function *)
+  type path
+  (** Names for identifiers. *)
 
   val equal : t -> t -> bool
   (** Equality function *)
 
-  val name : t -> string
-  (** The name / string to print for the identifier *)
+  val path : t -> path
+  (** Identifier name. *)
+
+  module Map : Map.S with type key = t
+  (** A module for Maps on ids. *)
+
+end
+
+module type Scope_Full = sig
+
+  include Scope
+  (** We extend the regular `Scope` module. *)
+
+  type namespace
+  (** Namespaces for identifiers. *)
+
+  val namespace : t -> namespace
+  (** Return the namespace of an identifier. *)
 
 end

src/interface/map.ml

@@ -7,6 +7,7 @@ module type S = sig
   type 'a t
 
   val empty : _ t
+  (** The empty map *)
 
   val find_exn : key -> 'a t -> 'a
   (** Exception-raising find function.
@@ -16,7 +17,7 @@ module type S = sig
   (** Option-returning find function. *)
 
   val add : key -> 'a -> 'a t -> 'a t
-  (** Add a new binding, shadowing any earlier bdingin to the same key. *)
+  (** Add a new binding, shadowing any earlier binding to the same key. *)
 
   val find_add : key -> ('a option -> 'a) -> 'a t -> 'a t
   (** Update the value bound to a key. *)
@@ -28,3 +29,4 @@ module type S = sig
   (** Fold on the map. *)
 
 end
+