Fixes + psmt2 printing

TODO

@@ -4,6 +4,7 @@
 - Add comments
 - generate headers when printing to smtlib ?
 
+
 # Normalisation / transformation
 
 - add implicit base type decl (tptp's $i)

src/bin/options.ml

@@ -28,6 +28,7 @@ let () =
     Dolmen_loop.Headers.code, 5;
     Dolmen_model.Loop.code, 6;
     Dolmen_loop.Flow.code, 7;
+    Dolmen_loop.Export.code, 8;
   ]
 
 (* Main commands *)

src/interface/dune

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

src/interface/print.ml

@@ -0,0 +1,145 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+(* Smtlib2 printing *)
+(* ************************************************************************* *)
+
+module type Smtlib2 = sig
+
+  type env
+  type sexpr
+  type ty
+  type ty_var
+  type ty_cst
+  type term
+  type term_var
+  type term_cst
+
+  (** {2 Helpers} *)
+
+    val match_prop_literal : term -> [
+        | `Cst of term_cst
+        | `Neg of term_cst
+        | `Not_a_prop_literal ]
+  (** Match against prop literals. *)
+
+
+  (** {2 Types and terms} *)
+
+  val ty : env -> Format.formatter -> ty -> unit
+  (** Printer for types *)
+
+  val term : env -> Format.formatter -> term -> unit
+  (** Printer for terms *)
+
+
+  (** {2 Statements} *)
+
+  val echo : env -> Format.formatter -> string -> unit
+  (** *)
+
+  val set_logic : env -> Format.formatter -> string -> unit
+  (** Print a set-logic statement. *)
+
+  val set_info : env -> Format.formatter -> sexpr -> unit
+  (** *)
+
+  val set_option : env -> Format.formatter-> sexpr -> unit
+  (** *)
+
+  val get_info : env -> Format.formatter -> sexpr -> unit
+  (** *)
+
+  val get_option : env -> Format.formatter -> sexpr -> unit
+  (** *)
+
+  val get_value : env -> Format.formatter -> term list -> unit
+  (** *)
+
+  val pop : env -> Format.formatter -> int -> unit
+  (** [pop fmt n] prints a statement that pops `n` levels.
+      @raise Cannot_print if the provided level is non-positive *)
+
+  val push : env -> Format.formatter -> int -> unit
+  (** [push fmt n] prints a statement that pushes `n` levels.
+      @raise Cannot_print if the provided level is non-positive *)
+
+  val declare_sort : env -> Format.formatter -> ty_cst -> unit
+  (** Declare a sort, i.e. a type constant. *)
+
+  val declare_datatype :
+    env -> Format.formatter ->
+    ty_cst * ty_var list *
+    (term_cst * (ty * term_cst) list) list ->
+    unit
+  (** Declare a single datatype. *)
+
+  val declare_datatypes :
+    env -> Format.formatter ->
+    (ty_cst * ty_var list * (term_cst * (ty * term_cst) list) list) list ->
+    unit
+  (** Declare multiple mutually recursive datatypes. *)
+
+  val declare_fun : env -> Format.formatter -> term_cst -> unit
+  (** Declare a function, i.e. a term constant. This will use
+      either the `declare-fun` or the `declare-const` statement
+      depending on the actualy type of the function. *)
+
+  val define_sort :
+    env -> Format.formatter ->
+    (ty_cst * ty_var list * ty) -> unit
+  (** *)
+
+  val define_fun :
+    env -> Format.formatter ->
+    (term_cst * ty_var list * term_var list * term) -> unit
+  (** *)
+
+  val define_fun_rec :
+    env -> Format.formatter ->
+    (term_cst * ty_var list * term_var list * term) -> unit
+  (** *)
+
+  val define_funs_rec :
+    env -> Format.formatter ->
+    (term_cst * ty_var list * term_var list * term) list -> unit
+  (** *)
+
+  val assert_ : env -> Format.formatter -> term -> unit
+  (** *)
+
+  val check_sat : env -> Format.formatter -> unit -> unit
+  (** *)
+
+  val check_sat_assuming : env -> Format.formatter -> term list -> unit
+  (** *)
+
+  val reset : env -> Format.formatter -> unit -> unit
+  (** Print a `reset` statement. *)
+
+  val reset_assertions : env -> Format.formatter -> unit -> unit
+  (** Print a `reset-assertion` statement. *)
+
+  val get_unsat_core : env -> Format.formatter -> unit -> unit
+  (** Print a `get-unsat-core` statement. *)
+
+  val get_unsat_assumptions : env -> Format.formatter -> unit -> unit
+  (** Print a `get-unsat-assumptions` statement. *)
+
+  val get_proof : env -> Format.formatter -> unit -> unit
+  (** Print a `get-proof` statement. *)
+
+  val get_model : env -> Format.formatter -> unit -> unit
+  (** Print a `get-model` statement. *)
+
+  val get_assertions : env -> Format.formatter -> unit -> unit
+  (** Print a `get-assertions` statement. *)
+
+  val get_assignment : env -> Format.formatter -> unit -> unit
+  (** Print a `get-assignment` statement. *)
+
+  val exit : env -> Format.formatter -> unit -> unit
+  (** Print an `exit` statement. *)
+
+end
+

src/languages/smtlib2/poly/lexer.mll

@@ -147,6 +147,7 @@
     done;
     (* Quoted symbols allow to use reserved words as symbols *)
     SYMBOL s
+
 }
 
 let white_space_char = ['\t' '\n' '\r' ' ']
@@ -206,3 +207,33 @@ and string newline b = parse
       Buffer.add_char b c; string newline b lexbuf }
   | _                   { raise Error }
 
+(* these are there to simplify the task of printers, by allowing to
+   check strings against some lexical categories *)
+and check_simple_symbol = parse
+  | simple_symbol eof { true }
+  | _ | eof           { false }
+
+and check_quoted_symbol = parse
+  | quoted_symbol_char* eof { true }
+  | _ | eof                 { false }
+
+and check_keyword = parse
+  | keyword eof { true }
+  | _ | eof     { false }
+
+and check_num = parse
+  | numeral eof { true }
+  | _ | eof     { false }
+
+and check_dec = parse
+  | decimal eof { true }
+  | _ | eof     { false }
+
+and check_hex = parse
+  | hexadecimal eof   { true }
+  | _ | eof           { false }
+
+and check_bin = parse
+  | binary eof  { true }
+  | _ | eof     { false }
+