1 files changed, 66 insertions, 0 deletions
diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
index cce4625..7317b60 100644
--- a/src/smtlib2/smtlib2_ast.ml
+++ b/src/smtlib2/smtlib2_ast.ml
@@ -15,6 +15,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+
 open Smtlib2_util
 
 type loc = Lexing.position * Lexing.position
@@ -187,3 +188,68 @@ let loc_varbinding = function
 let loc_couple = fst
 
 let loc_of e = loc_commands e;;
+
+
+
+let print_specconstant fmt = function
+  | SpecConstsDec (_, s)
+  | SpecConstNum (_, s)
+  | SpecConstString (_, s)
+  | SpecConstsHex (_, s)
+  | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s
+
+
+let print_symbol fmt = function
+  | Symbol (_, s)
+  | SymbolWithOr (_, s) -> Format.pp_print_string fmt s
+
+
+let print_identifier fmt = function
+  | IdSymbol (_, s) -> print_symbol fmt s
+  | IdUnderscoreSymNum (_, s, (_, l)) ->
+    Format.fprintf fmt "(_ %a" print_symbol s;
+    List.iter (Format.fprintf fmt " %s") l;
+    Format.fprintf fmt ")"  
+    
+let rec print_sort fmt = function
+  | SortIdentifier (_, i) -> print_identifier fmt i
+  | SortIdSortMulti (_, i, (_, ls)) ->
+    Format.fprintf fmt "(%a" print_identifier i;
+    List.iter (Format.fprintf fmt " %a" print_sort) ls;
+    Format.fprintf fmt ")"  
+
+let print_qualidentifier fmt = function
+  | QualIdentifierId (_, i) -> print_identifier fmt i
+  | QualIdentifierAs (_, i, s) ->
+    Format.fprintf fmt "(%a as %a)"
+      print_identifier i print_sort s 
+
+let print_sortedvar fmt = function
+  | SortedVarSymSort (_, v, s) ->
+    Format.fprintf fmt "(%a %a)" print_symbol v print_sort s
+
+let rec print_varbinding fmt = function
+  | VarBindingSymTerm (_, s, t) ->
+    Format.fprintf fmt "(%a %a)" print_symbol s print_term t
+
+and print_term fmt = function
+  | TermSpecConst (_, c) -> print_specconstant fmt c
+  | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
+  | TermQualIdTerm (_, i, (_, tl)) ->
+    Format.fprintf fmt "(%a" print_qualidentifier i;
+    List.iter (Format.fprintf fmt " %a" print_term) tl;
+    Format.fprintf fmt ")"  
+  | TermLetTerm (_, (_, vb), t) ->
+    Format.fprintf fmt "(let (";
+    List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
+    Format.fprintf fmt ") %a)" print_term t
+  | TermForAllTerm (_, (_, sv), t) ->
+    Format.fprintf fmt "(forall (";
+    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+    Format.fprintf fmt ") %a)" print_term t
+  | TermExistsTerm (_, (_, sv), t) ->
+    Format.fprintf fmt "(exists (";
+    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+    Format.fprintf fmt ") %a)" print_term t
+  | TermExclimationPt (_, t, _) -> print_term fmt t
+