diff options
| author | Alasdair Armstrong | 2019-05-08 18:14:51 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-08 18:23:08 +0100 |
| commit | ff4b53fba32ebdb6cb587fac0bc5f4a523304a55 (patch) | |
| tree | f6f1ce39709836e6ad3d988e96ab69327f897f8d /src/smtlib.ml | |
| parent | 611748f32de5269eb3d56bb3098cf07c9a89a0ba (diff) | |
SMT: Add reals and strings to SMT backend
Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.
Strings are likewise encoded as SMTLIB strings, for similar reasons.
Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.
Diffstat (limited to 'src/smtlib.ml')
| -rw-r--r-- | src/smtlib.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/smtlib.ml b/src/smtlib.ml index 72421b8a..7f485447 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -54,6 +54,8 @@ open Ast_util type smt_typ = | Bitvec of int | Bool + | String + | Real | Datatype of string * (string * (string * smt_typ) list) list | Tuple of smt_typ list | Array of smt_typ * smt_typ @@ -89,6 +91,8 @@ type smt_exp = | Bool_lit of bool | Hex of string | Bin of string + | Real_lit of string + | String_lit of string | Var of string | Fn of string * smt_exp list | Ite of smt_exp * smt_exp * smt_exp @@ -145,7 +149,7 @@ let rec simp_smt_exp vars = function | Some exp -> simp_smt_exp vars exp | None -> Var v end - | (Hex _ | Bin _ | Bool_lit _ as exp) -> exp + | (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)) @@ -184,6 +188,8 @@ let rec pp_smt_exp = let open PPrint in function | Bool_lit b -> string (string_of_bool b) + | Real_lit str -> string str + | String_lit str -> string ("\"" ^ str ^ "\"") | Hex str -> string ("#x" ^ str) | Bin str -> string ("#b" ^ str) | Var str -> string str @@ -201,6 +207,8 @@ let rec pp_smt_typ = let open PPrint in function | Bool -> string "Bool" + | String -> string "String" + | Real -> string "Real" | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n) | Datatype (name, _) -> string name | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys) |