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

fix(lra): preprocess in the right order

Browse source 
- relate `a=b` to `[[ a >= b ]]` and `[[ a <= b ]]`
- keep `a=b` as is, for CC
This commit is contained in:
Simon Cruanes 2022-09-12 22:45:07 -04:00
parent 2764882f50
commit e9eab74b1e
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -326,19 +326,14 @@ module Make (A : ARG) = (* : S with module A = A *) struct
(* TODO: box [t], recurse on [t1 <= t2] and [t1 >= t2], (* TODO: box [t], recurse on [t1 <= t2] and [t1 >= t2],
add 3 atomic clauses, return [box t] *) add 3 atomic clauses, return [box t] *)
let _, t = Term.abs self.tst t in let _, t = Term.abs self.tst t in
let box_t = Box.box self.tst t in if not (Term.Tbl.mem self.encoded_eqs t) then (
if not (Term.Tbl.mem self.encoded_eqs box_t) then ( let u1 = recurse @@ A.mk_lra tst (LRA_pred (Leq, t1, t2)) in
(* preprocess t1, t2 recursively *) let u2 = recurse @@ A.mk_lra tst (LRA_pred (Geq, t1, t2)) in
let t1 = recurse t1 in
let t2 = recurse t2 in
let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in Term.Tbl.add self.encoded_eqs t ();
let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in
Term.Tbl.add self.encoded_eqs box_t ();
(* encode [t <=> (u1 /\ u2)] *) (* encode [t <=> (u1 /\ u2)] *)
let lit_t = PA.mk_lit box_t in let lit_t = PA.mk_lit t in
let lit_u1 = PA.mk_lit u1 in let lit_u1 = PA.mk_lit u1 in
let lit_u2 = PA.mk_lit u2 in let lit_u2 = PA.mk_lit u2 in
add_clause_lra_ (module PA) [ Lit.neg lit_t; lit_u1 ]; add_clause_lra_ (module PA) [ Lit.neg lit_t; lit_u1 ];