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

warnings and comments

Browse source
This commit is contained in:
Simon Cruanes 2023-06-23 21:23:42 -04:00
parent c64bebaf6f
commit c4d3c44c49
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -8,12 +8,13 @@ include Intf
module SI = SMT.Solver_internal module SI = SMT.Solver_internal
module Tag = struct module Tag = struct
type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t | By_def
let pp out = function let pp out = function
| Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
| CC_eq (n1, n2) -> | CC_eq (n1, n2) ->
Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" E_node.pp n1 E_node.pp n2 Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" E_node.pp n1 E_node.pp n2
| By_def -> Fmt.string out "by-def"
let to_lits si = function let to_lits si = function
| Lit l -> [ l ] | Lit l -> [ l ]
@ -23,6 +24,7 @@ module Tag = struct
assert (not (SI.CC.Resolved_expl.is_semantic r)); assert (not (SI.CC.Resolved_expl.is_semantic r));
*) *)
r.lits r.lits
| By_def -> []
end end
module SimpVar : Linear_expr.VAR with type t = Term.t and type lit = Tag.t = module SimpVar : Linear_expr.VAR with type t = Term.t and type lit = Tag.t =
@ -129,14 +131,14 @@ module Make (A : ARG) = (* : S with module A = A *) struct
gensym: Gensym.t; gensym: Gensym.t;
in_model: unit Term.Tbl.t; (* terms to add to model *) in_model: unit Term.Tbl.t; (* terms to add to model *)
encoded_eqs: unit Term.Tbl.t; encoded_eqs: unit Term.Tbl.t;
(* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) (** [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
encoded_lits: Term.t Term.Tbl.t; (** [t => lit for t], using gensym *) encoded_lits: Term.t Term.Tbl.t; (** [t => lit for t], using gensym *)
simp_preds: (Term.t * S_op.t * A.Q.t) Term.Tbl.t; simp_preds: (Term.t * S_op.t * A.Q.t) Term.Tbl.t;
(* term -> its simplex meaning *) (** term -> its simplex meaning *)
simp_defined: (Term.t * LE.t) Term.Tbl.t; simp_defined: (Term.t * LE.t) Term.Tbl.t;
(* (rational) terms that are equal to a linexp *) (** (rational) terms that are equal to a linexp *)
st_exprs: ST_exprs.t; st_exprs: ST_exprs.t;
mutable encoded_le: Term.t Comb_map.t; (* [le] -> var encoding [le] *) mutable encoded_le: Term.t Comb_map.t; (** [le] -> var encoding [le] *)
simplex: SimpSolver.t; simplex: SimpSolver.t;
mutable last_res: SimpSolver.result option; mutable last_res: SimpSolver.result option;
n_propagate: int Stat.counter; n_propagate: int Stat.counter;
@ -387,6 +389,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
Some box_t Some box_t
| LRA_op _ | LRA_mult _ -> | LRA_op _ | LRA_mult _ ->
(* define term *)
(match Term.Tbl.find_opt self.simp_defined t with (match Term.Tbl.find_opt self.simp_defined t with
| Some (t, _le) -> Some t | Some (t, _le) -> Some t
| None -> | None ->