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

refactor lra

Browse source
This commit is contained in:
Simon Cruanes 2021-02-22 14:28:31 -05:00
parent 45893e92f1
commit 4d0c24f40f
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/arith/lra/sidekick_arith_lra.ml
View file

@ -259,15 +259,17 @@ module Make(A : ARG) : S with module A = A = struct
let proxy = var_encoding_comb self ~pre:"_le" le_comb in let proxy = var_encoding_comb self ~pre:"_le" le_comb in
declare_term_to_cc proxy; declare_term_to_cc proxy;
let new_t = let op =
match pred with match pred with
| Eq | Neq -> assert false (* unreachable *) | Eq | Neq -> assert false (* unreachable *)
| Leq -> A.mk_lra tst (LRA_simplex_pred (proxy, S_op.Leq, le_const)) | Leq -> S_op.Leq
| Lt -> A.mk_lra tst (LRA_simplex_pred (proxy, S_op.Lt, le_const)) | Lt -> S_op.Lt
| Geq -> A.mk_lra tst (LRA_simplex_pred (proxy, S_op.Geq, le_const)) | Geq -> S_op.Geq
| Gt -> A.mk_lra tst (LRA_simplex_pred (proxy, S_op.Gt, le_const)) | Gt -> S_op.Gt
in in
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t); Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
Some new_t Some new_t