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

more stats

Browse source
This commit is contained in:
Simon Cruanes 2021-02-22 16:45:21 -05:00
parent d6aa1071d7
commit a5166fb19b
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -134,9 +134,10 @@ module Make(A : ARG) : S with module A = A = struct
mutable encoded_le: T.t Comb_map.t; (* [le] -> var encoding [le] *)
local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *)
simplex: SimpSolver.t;
stat_th_comb: int Stat.counter;
}
let create ?stat tst : state =
let create ?(stat=Stat.create()) tst : state =
{ tst;
simps=T.Tbl.create 128;
gensym=A.Gensym.create tst;
@ -144,7 +145,8 @@ module Make(A : ARG) : S with module A = A = struct
needs_th_combination=T.Tbl.create 8;
encoded_le=Comb_map.empty;
local_eqs = Backtrack_stack.create();
simplex=SimpSolver.create ?stat ();
simplex=SimpSolver.create ~stat ();
stat_th_comb=Stat.mk_int stat "lra.th-comb";
}
let push_level self =
@ -433,6 +435,9 @@ module Make(A : ARG) : S with module A = A = struct
the next decision to do *)
if not (SI.cc_are_equal si t1 t2) then (
Log.debug 50 "LRA.th-comb.must-decide-equal";
Stat.incr self.stat_th_comb;
Profile.instant "lra.th-comb-assert-eq";
let t = A.mk_eq (SI.tst si) t1 t2 in
let lit = SI.mk_lit si acts t in
SI.push_decision si acts lit