SMT: Allow printing SMT with an optional variable prefix

Allows us to mix generated SMT for two separate threads without name
clashes, however we do want to be able to share datatypes so they are
not prefixed. Currently the pretty-printer adds the prefix but we may
want a smt_def -> smt_def renaming function instead.

2 files changed, 29 insertions, 25 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 5847c99c..4fbfa589 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -244,7 +244,7 @@ let smt_value ctx vl ctyp =
   | VL_int n, CT_lint -> bvint ctx.lint_size n
   | VL_bit Sail2_values.B0, CT_bit -> Bin "0"
   | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
-  | VL_unit, _ -> Var "unit"
+  | VL_unit, _ -> Enum "unit"
   | VL_string str, _ ->
      ctx.use_string := true;
      String_lit (String.escaped str)
@@ -268,7 +268,7 @@ let rec smt_cval ctx cval =
   | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
   | V_id (Name (id, _) as ssa_id, _) ->
      begin match Type_check.Env.lookup_id id ctx.tc_env with
-     | Enum _ -> Var (zencode_id id)
+     | Enum _ -> Enum (zencode_id id)
      | _ -> Var (zencode_name ssa_id)
      end
   | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
@@ -1170,7 +1170,7 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_var kid -> CT_poly
 
-  | _ -> raise (Reporting.err_unreachable l __POS__ ("No C type for type " ^ string_of_typ typ))
+  | _ -> raise (Reporting.err_unreachable l __POS__ ("No SMT type for type " ^ string_of_typ typ))
 
 (**************************************************************************)
 (* 3. Optimization of primitives and literals                             *)
@@ -1571,7 +1571,7 @@ let optimize_smt stack =
        | Some n -> Hashtbl.replace uses var (n + 1)
        | None -> Hashtbl.add uses var 1
        end
-    | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+    | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
     | Fn (f, exps) ->
        List.iter uses_in_exp exps
     | Ite (cond, t, e) ->
@@ -1788,16 +1788,16 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           output_string out_chan "(set-option :produce-models true)\n";
 
         let header = smt_header ctx all_cdefs in
-        
+
         if !(ctx.use_string) || !(ctx.use_real) then
           output_string out_chan "(set-logic ALL)\n"
         else
           output_string out_chan "(set-logic QF_AUFBVDT)\n";
 
-        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header;
+        List.iter (fun def -> output_string out_chan (string_of_smt_def "" def); output_string out_chan "\n") header;
 
         let queue = optimize_smt stack in
-        Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
+        Queue.iter (fun def -> output_string out_chan (string_of_smt_def "" def); output_string out_chan "\n") queue;
 
         output_string out_chan "(check-sat)\n";
         if prop_type = "counterexample" then
diff --git a/src/smtlib.ml b/src/smtlib.ml
index ab6ebf55..ac8370e0 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -94,6 +94,7 @@ type smt_exp =
   | Real_lit of string
   | String_lit of string
   | Var of string
+  | Enum of string
   | Fn of string * smt_exp list
   | Ite of smt_exp * smt_exp * smt_exp
   | SignExtend of int * smt_exp
@@ -159,7 +160,7 @@ let rec simp_smt_exp vars = function
      | Some exp -> simp_smt_exp vars exp
      | None -> Var v
      end
-  | (Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | (Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
   | Fn (f, exps) ->
      let exps = List.map (simp_smt_exp vars) exps in
      simp_fn (Fn (f, exps))
@@ -196,7 +197,9 @@ let pp_sfun str docs =
   let open PPrint in
   parens (separate space (string str :: docs))
 
-let rec pp_smt_exp =
+let prefix_string pre str = PPrint.string (pre ^ str)
+
+let rec pp_smt_exp pre =
   let open PPrint in
   function
   | Bool_lit b -> string (string_of_bool b)
@@ -204,16 +207,17 @@ let rec pp_smt_exp =
   | String_lit str -> string ("\"" ^ str ^ "\"")
   | Hex str -> string ("#x" ^ str)
   | Bin str -> string ("#b" ^ str)
-  | Var str -> string str
-  | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
+  | Var str -> prefix_string pre str
+  | Enum str -> string str
+  | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space (pp_smt_exp pre) exps)
   | Ite (cond, then_exp, else_exp) ->
-     parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp])
+     parens (separate space [string "ite"; pp_smt_exp pre cond; pp_smt_exp pre then_exp; pp_smt_exp pre else_exp])
   | Extract (i, j, exp) ->
-     parens (string (Printf.sprintf "(_ extract %d %d)" i j) ^^ space ^^ pp_smt_exp exp)
+     parens (string (Printf.sprintf "(_ extract %d %d)" i j) ^^ space ^^ pp_smt_exp pre exp)
   | Tester (kind, exp) ->
-     parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp)
+     parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp pre exp)
   | SignExtend (i, exp) ->
-     parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp)
+     parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp pre exp)
 
 let rec pp_smt_typ =
   let open PPrint in
@@ -228,7 +232,7 @@ let rec pp_smt_typ =
 
 let pp_str_smt_typ (str, ty) = let open PPrint in string str ^^ space ^^ pp_smt_typ ty
 
-let pp_smt_def =
+let pp_smt_def pre =
   let open PPrint in
   let open Printf in
   function
@@ -236,19 +240,19 @@ let pp_smt_def =
      parens (string "define-fun"
              ^^ space ^^ parens (separate_map space pp_str_smt_typ args)
              ^^ space ^^ pp_smt_typ ty
-             ^//^ pp_smt_exp exp)
+             ^//^ pp_smt_exp pre exp)
 
   | Declare_const (name, ty) ->
-     pp_sfun "declare-const" [string name; pp_smt_typ ty]
+     pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ ty]
 
   | Define_const (name, ty, exp) ->
-     pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
+     pp_sfun "define-const" [prefix_string pre name; pp_smt_typ ty; pp_smt_exp pre exp]
 
   | Write_mem (name, wk, addr, data) ->
-     pp_sfun "declare-const" [string name; pp_smt_typ Bool]
+     pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ Bool]
 
   | Read_mem (name, ty, rk, addr) ->
-     pp_sfun "declare-const" [string name; pp_smt_typ ty]
+     pp_sfun "declare-const" [prefix_string pre name; pp_smt_typ ty]
 
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
@@ -271,12 +275,12 @@ let pp_smt_def =
                            parens (parens (ksprintf string "tup%d" n ^^ space ^^ fields))]))]
 
   | Assert exp ->
-     pp_sfun "assert" [pp_smt_exp exp]
+     pp_sfun "assert" [pp_smt_exp pre exp]
 
-let string_of_smt_def def = Pretty_print_sail.to_string (pp_smt_def def)
+let string_of_smt_def pre def = Pretty_print_sail.to_string (pp_smt_def pre def)
 
-let output_smt_defs out_chan smt =
-  List.iter (fun def -> output_string out_chan (string_of_smt_def def ^ "\n")) smt
+let output_smt_defs out_chan pre smt =
+  List.iter (fun def -> output_string out_chan (string_of_smt_def pre def ^ "\n")) smt
 
 (**************************************************************************)
 (* 2. Parser for SMT solver output                                        *)