simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 13:14:09 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

missing lra file

Browse source
This commit is contained in:
Simon Cruanes 2020-09-08 22:29:36 -04:00
parent f59a5d9fce
commit 216cbe762f
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/smtlib/lra.ml Normal file
View file

@ -0,0 +1,23 @@
open Sidekick_base_term
module T = Sidekick_base_term.Term
let id_leq = ID.make "<="
let id_lt = ID.make "<"
let id_plus = ID.make "+"
let id_uminus = ID.make "-"
let id_mult = ID.make "*"
let fun_leq = Fun.mk_undef id_leq Ty.(Fun.mk [real; real] bool)
let fun_lt = Fun.mk_undef id_lt Ty.(Fun.mk [real; real] bool)
let fun_plus = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
let fun_uminus = Fun.mk_undef id_plus Ty.(Fun.mk [real] real)
let fun_times = Fun.mk_undef id_plus Ty.(Fun.mk [real; real] real)
let leq st a b = T.app_fun st fun_leq (IArray.of_array_unsafe [|a; b|])
let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
let lt st a b = T.app_fun st fun_lt (IArray.of_array_unsafe [|a; b|])
let view_as_lra _ = assert false (* TODO *)
let mk_lra _ = assert false