let smtlib_string_symbol_list = [("not", Symbol.mk_symbol `NOT); ("=>", Symbol.mk_symbol `IMPLIES); ("and", Symbol.mk_symbol `AND); ("or", Symbol.mk_symbol `OR); ("xor", Symbol.mk_symbol `XOR); ("=", Symbol.mk_symbol `EQ); ("distinct", Symbol.mk_symbol `DISTINCT); ("ite", Symbol.mk_symbol `ITE); ("-", Symbol.mk_symbol `MINUS); ("+", Symbol.mk_symbol `PLUS); ("*", Symbol.mk_symbol `TIMES); ("/", Symbol.mk_symbol `DIV); ("div", Symbol.mk_symbol `INTDIV); ("mod", Symbol.mk_symbol `MOD); ("abs", Symbol.mk_symbol `ABS); ("<=", Symbol.mk_symbol `LEQ); ("<", Symbol.mk_symbol `LT); (">=", Symbol.mk_symbol `GEQ); (">", Symbol.mk_symbol `GT); ("to_real", Symbol.mk_symbol `TO_REAL); ("to_int", Symbol.mk_symbol `TO_INT); ("is_int", Symbol.mk_symbol `IS_INT); (* ("concat", Symbol.mk_symbol `CONCAT); ("bvnot", Symbol.mk_symbol `BVNOT); ("bvneg", Symbol.mk_symbol `BVNEG); ("bvand", Symbol.mk_symbol `BVAND); ("bvor", Symbol.mk_symbol `BVOR); ("bvadd", Symbol.mk_symbol `BVADD); ("bvmul", Symbol.mk_symbol `BVMUL); ("bvdiv", Symbol.mk_symbol `BVDIV); ("bvurem", Symbol.mk_symbol `BVUREM); ("bvshl", Symbol.mk_symbol `BVSHL); ("bvlshr", Symbol.mk_symbol `BVLSHR); ("bvult", Symbol.mk_symbol `BVULT); *) ("select", Symbol.mk_symbol (`SELECT (Type.mk_array Type.t_int Type.t_int))); (* placeholder *) (* uninterpreted select *) (* ("uselect", Symbol.mk_symbol (`SELECT Type.t_int)); *) ("store", Symbol.mk_symbol `STORE) ]