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

refactor: a bit of cleanup

Browse source
This commit is contained in:
Simon Cruanes 2021-02-11 17:17:55 -05:00
parent 75ce199bb0
commit 2a0e14a635
1 changed files with 1 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/arith/lra/sidekick_arith_lra.ml
View file

@ -7,6 +7,7 @@
open Sidekick_core open Sidekick_core
module Simplex = Simplex module Simplex = Simplex
module Simplex2 = Simplex2
module Predicate = Predicate module Predicate = Predicate
module Linear_expr = Linear_expr module Linear_expr = Linear_expr
@ -123,7 +124,6 @@ module Make(A : ARG) : S with module A = A = struct
module LE = SimpSolver.L.Expr module LE = SimpSolver.L.Expr
module LConstr = SimpSolver.L.Constr module LConstr = SimpSolver.L.Constr
type proxy = T.t
type state = { type state = {
tst: T.state; tst: T.state;
simps: T.t T.Tbl.t; (* cache *) simps: T.t T.Tbl.t; (* cache *)
@ -306,12 +306,6 @@ module Make(A : ARG) : S with module A = A = struct
) )
end end
let dedup_lits lits : _ list =
let module LTbl = CCHashtbl.Make(Lit) in
let tbl = LTbl.create 16 in
List.iter (fun l -> LTbl.replace tbl l ()) lits;
LTbl.keys_list tbl
module Q_map = CCMap.Make(Q) module Q_map = CCMap.Make(Q)
let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit = let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =