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

comments

Browse source
This commit is contained in:
Simon Cruanes 2022-09-16 19:51:10 -04:00
parent c49edd8d70
commit 24251399bf
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/th-lra/sidekick_th_lra.ml
View file

@ -322,9 +322,9 @@ module Make (A : ARG) = (* : S with module A = A *) struct
None
| _ -> assert false)
| LRA_pred ((Eq | Neq), t1, t2) ->
(* equality: just punt to [t1 = t2 <=> (t1 <= t2 /\ t1 >= t2)] *)
(* TODO: box [t], recurse on [t1 <= t2] and [t1 >= t2],
add 3 atomic clauses, return [box t] *)
(* Equality: just punt to [(t1 = t2) <=> (t1 <= t2 /\ t1 >= t2)].
We use [t1=t2] rather than [box (t1=t2)] because the congruence
closure must still have access to the equality. *)
let _, t = Term.abs self.tst t in
if not (Term.Tbl.mem self.encoded_eqs t) then (
let u1 = recurse @@ A.mk_lra tst (LRA_pred (Leq, t1, t2)) in