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

tmp: restore some preprocessing

Browse source
This commit is contained in:
Simon Cruanes 2022-01-03 16:15:42 -05:00
parent 6970c83ff1
commit ab4e115b32
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/lra/sidekick_arith_lra.ml
View file

@ -272,9 +272,10 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.encoded_eqs t ();
(* encode [t <=> (u1 /\ u2)] *)
let lit_t = PA.mk_lit_nopreproc t in
let lit_u1 = PA.mk_lit_nopreproc u1 in
let lit_u2 = PA.mk_lit_nopreproc u2 in
(* FIXME: add preproc proofs, with a clause_rw perhaps *)
let lit_t,_ = PA.mk_lit t in
let lit_u1,_ = PA.mk_lit u1 in
let lit_u2,_ = PA.mk_lit u2 in
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
add_clause_lra_ (module PA)
@ -310,7 +311,7 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
begin
let lit = PA.mk_lit_nopreproc new_t in
let lit,_ = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;