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: define expressions occurring in subterms properly

Browse source 
these sub-expressions need to be registered in the Simplex, possibly
using an intermediate variable in case there's an offset.
This commit is contained in:
Simon Cruanes 2023-06-23 21:23:50 -04:00
parent c4d3c44c49
commit 3ba2583966
1 changed files with 33 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -228,13 +228,24 @@ module Make (A : ARG) = (* : S with module A = A *) struct
comb; comb;
!cur !cur
(* encode back into a term *) (** encode back into a term *)
let t_of_linexp (self : state) (le : LE.t) : Term.t = let t_of_linexp (self : state) (le : LE.t) : Term.t =
let comb = LE.comb le in let comb = LE.comb le in
let const = LE.const le in let const = LE.const le in
t_of_comb self comb ~init:(A.mk_lra self.tst (LRA_const const)) t_of_comb self comb ~init:(A.mk_lra self.tst (LRA_const const))
(* return a variable that is equal to [le_comb] in the simplex. *) (** encode that [proxy := le_comb] into the simplex. *)
let encode_def self (proxy : Term.t) (le_comb : LE_.Comb.t) : unit =
assert (not (LE_.Comb.is_empty le_comb));
Log.debugf 50 (fun k ->
k "(@[lra.encode-linexp@ `@[%a@]`@ :into-var %a@])" LE_.Comb.pp le_comb
Term.pp proxy);
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb);
()
(** return a variable that is equal to [le_comb] in the simplex. *)
let var_encoding_comb ~pre self (le_comb : LE_.Comb.t) : Term.t = let var_encoding_comb ~pre self (le_comb : LE_.Comb.t) : Term.t =
assert (not (LE_.Comb.is_empty le_comb)); assert (not (LE_.Comb.is_empty le_comb));
match LE_.Comb.as_singleton le_comb with match LE_.Comb.as_singleton le_comb with
@ -245,14 +256,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
| exception Not_found -> | exception Not_found ->
(* new variable to represent [le_comb] *) (* new variable to represent [le_comb] *)
let proxy = fresh_term self ~pre (A.ty_real self.tst) in let proxy = fresh_term self ~pre (A.ty_real self.tst) in
(* TODO: define proxy *)
self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
Log.debugf 50 (fun k -> encode_def self proxy le_comb;
k "(@[lra.encode-linexp@ `@[%a@]`@ :into-var %a@])" LE_.Comb.pp
le_comb Term.pp proxy);
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb);
proxy) proxy)
let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits = let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits =
@ -397,6 +402,25 @@ module Make (A : ARG) = (* : S with module A = A *) struct
(* we define these terms so their value in the model make sense *) (* we define these terms so their value in the model make sense *)
let le = as_linexp t |> LE.map ~f:recurse in let le = as_linexp t |> LE.map ~f:recurse in
Term.Tbl.add self.simp_defined t (box_t, le); Term.Tbl.add self.simp_defined t (box_t, le);
Log.debugf 50 (fun k -> k "COUCOU def %a as %a" Term.pp box_t LE.pp le);
let le_comb, le_const = LE.comb le, LE.const le in
if A.Q.equal le_const A.Q.zero then
(* we can directly {i define} [box_t] as equal to [le_comb] *)
encode_def self box_t le_comb
else (
let le_comb_minus_t =
var_encoding_comb ~pre:"diff_def" self
LE_.Comb.(le_comb - monomial1 box_t)
in
SimpSolver.add_constraint self.simplex
(SimpSolver.Constraint.geq le_comb_minus_t le_const) Tag.By_def
~on_propagate:(fun _ ~reason:_ -> ());
SimpSolver.add_constraint self.simplex
(SimpSolver.Constraint.leq le_comb_minus_t le_const) Tag.By_def
~on_propagate:(fun _ ~reason:_ -> ())
);
Some box_t) Some box_t)
| LRA_const _n -> None | LRA_const _n -> None
| LRA_other _ -> None | LRA_other _ -> None