diff options
Diffstat (limited to 'src/smtlib.ml')
| -rw-r--r-- | src/smtlib.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smtlib.ml b/src/smtlib.ml index 1665419c..a252ea4a 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -182,6 +182,8 @@ type smt_def = | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp | Declare_const of string * smt_typ | Define_const of string * smt_typ * smt_exp + | Write_mem of smt_exp * smt_exp * smt_exp + | Read_mem of string * smt_exp * smt_exp | Declare_datatypes of string * (string * (string * smt_typ) list) list | Declare_tuple of int | Assert of smt_exp @@ -242,6 +244,12 @@ let pp_smt_def = | Define_const (name, ty, exp) -> pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp] + | Write_mem (wk, addr, data) -> + pp_sfun "write-mem" [pp_smt_exp wk; pp_smt_exp addr; pp_smt_exp data] + + | Read_mem (name, rk, addr) -> + pp_sfun "read-mem" [string name; pp_smt_exp rk; pp_smt_exp addr] + | Declare_datatypes (name, ctors) -> let pp_ctor (ctor_name, fields) = match fields with |