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

fix(lra): preprocessing of linexps with non-zero constants

Browse source
This commit is contained in:
Simon Cruanes 2022-02-04 16:16:00 -05:00
parent cbc9c5ac6f
commit ab74b1a792
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 16 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/lra/sidekick_arith_lra.ml
View file

@ -365,6 +365,9 @@ module Make(A : ARG) : S with module A = A = struct
| LRA_op _ | LRA_mult _ -> | LRA_op _ | LRA_mult _ ->
let steps = ref [] in let steps = ref [] in
let le = as_linexp t in let le = as_linexp t in
(* [t] is [le_comb + le_const], where [le_comb] is a linear expression
without constant. *)
let le_comb, le_const = LE.comb le, LE.const le in let le_comb, le_const = LE.comb le, LE.const le in
if A.Q.(le_const = zero) then ( if A.Q.(le_const = zero) then (
@ -372,39 +375,35 @@ module Make(A : ARG) : S with module A = A = struct
declare_term_to_cc t; declare_term_to_cc t;
) else ( ) else (
(* a bit more complicated: we cannot just define [t := le_comb] (* a bit more complicated: we cannot just define [t := le_comb]
because of the coefficient. because of the coefficient, and the simplex doesn't like offsets.
Instead we assert [t - le_comb = le_const] using a secondary Instead we assert [t := le_comb + proxy2] using a secondary
variable [proxy2 := t - le_comb] variable [proxy2] and asserting [proxy2 = le_const] *)
and asserting [proxy2 = le_const] *)
let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
(* TODO
let pr_def2 = let pr_def2 =
SI.P.define_term proxy2 SI.P.define_term proxy2 (A.mk_lra tst (LRA_const le_const)) PA.proof
(A.mk_lra tst (LRA_op (Minus, t, A.mk_lra tst (LRA_const le_const)))) PA.proof
in in
SimpSolver.add_var self.simplex proxy; SimpSolver.add_var self.simplex proxy2;
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy2 SimpSolver.define self.simplex t
((A.Q.minus_one, proxy) :: LE_.Comb.to_list le_comb); ((A.Q.one, proxy2) :: LE_.Comb.to_list le_comb);
Log.debugf 50 Log.debugf 50
(fun k->k "(@[lra.encode-linexp.with-offset@ %a@ :var %a@ :diff-var %a@])" (fun k->k "(@[lra.encode-linexp.with-offset@ %a@ :var %a@ :const-var %a@])"
LE_.Comb.pp le_comb T.pp proxy T.pp proxy2); LE_.Comb.pp le_comb T.pp t T.pp proxy2);
declare_term_to_cc proxy; declare_term_to_cc t;
declare_term_to_cc proxy2; declare_term_to_cc proxy2;
(* now assert [proxy2 = le_const] *)
add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, le_const)))
]; ];
add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, le_const)))
]; ];
Some (proxy, Iter.of_list !steps)
*)
() ()
) )