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

fix: use standard = even for LRA terms

Browse source 
the LRA_view is only useful for views, but we build =/neq using builtin
=
This commit is contained in:
Simon Cruanes 2022-08-28 00:20:06 -04:00
parent 28ad97d2b7
commit 83a4ae46c1
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 16 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/base/LRA_term.ml
View file

@ -12,8 +12,8 @@ module Pred = struct
let to_string = function let to_string = function
| Lt -> "<" | Lt -> "<"
| Leq -> "<=" | Leq -> "<="
| Neq -> "!=" | Neq -> "!=_LRA"
| Eq -> "=" | Eq -> "=_LRA"
| Gt -> ">" | Gt -> ">"
| Geq -> ">=" | Geq -> ">="
@ -127,6 +127,10 @@ let mult_by tst q t : term =
Term.app tst c t Term.app tst c t
let pred tst p t1 t2 : term = let pred tst p t1 t2 : term =
match p with
| Pred.Eq -> T.eq tst t1 t2
| Pred.Neq -> T.not tst (T.eq tst t1 t2)
| _ ->
let ty = Term.(arrow_l tst [ real tst; real tst ] (Term.bool tst)) in let ty = Term.(arrow_l tst [ real tst; real tst ] (Term.bool tst)) in
let p = Term.const tst (Const.make (Pred p) ops ~ty) in let p = Term.const tst (Const.make (Pred p) ops ~ty) in
Term.app_l tst p [ t1; t2 ] Term.app_l tst p [ t1; t2 ]
@ -151,6 +155,13 @@ let view (t : term) : _ View.t =
match T.view f, args with match T.view f, args with
| T.E_const { Const.c_view = T.C_eq; _ }, [ _; a; b ] when has_ty_real a -> | T.E_const { Const.c_view = T.C_eq; _ }, [ _; a; b ] when has_ty_real a ->
View.LRA_pred (Pred.Eq, a, b) View.LRA_pred (Pred.Eq, a, b)
| T.E_const { Const.c_view = T.C_not; _ }, [ u ] ->
(* might be not-eq *)
let f, args = Term.unfold_app u in
(match T.view f, args with
| T.E_const { Const.c_view = T.C_eq; _ }, [ _; a; b ] when has_ty_real a ->
View.LRA_pred (Pred.Neq, a, b)
| _ -> View.LRA_other t)
| T.E_const { Const.c_view = Const q; _ }, [] -> View.LRA_const q | T.E_const { Const.c_view = Const q; _ }, [] -> View.LRA_const q
| T.E_const { Const.c_view = Pred p; _ }, [ a; b ] -> View.LRA_pred (p, a, b) | T.E_const { Const.c_view = Pred p; _ }, [ a; b ] -> View.LRA_pred (p, a, b)
| T.E_const { Const.c_view = Op op; _ }, [ a; b ] -> View.LRA_op (op, a, b) | T.E_const { Const.c_view = Op op; _ }, [ a; b ] -> View.LRA_op (op, a, b)