diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 14 | ||||
| -rw-r--r-- | src/smtlib.ml | 40 |
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 *) |