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

feat(dyn-trans): track activity of terms to guide instantiation

Browse source
This commit is contained in:
Simon Cruanes 2021-09-20 06:30:39 -04:00
parent 3840fefb0e
commit 5f51863cd3
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 40 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/th-dyn-trans/Sidekick_th_dyn_trans.ml
View file

@ -59,6 +59,7 @@ module Make(A: ARG)
tstore: Term.store;
cc: CC.t;
sat: SAT.t;
activity: float Term.Tbl.t;
cpool: SAT.clause_pool_id;
done_inst: unit Inst_tbl.t;
stat_cc_confl: int Stat.counter;
@ -67,13 +68,19 @@ module Make(A: ARG)
(* CONFIG *)
let cpool_size = (try int_of_string (Sys.getenv "CPOOL_SIZE") with _ -> 100)
let cpool_size = (try int_of_string (Sys.getenv "CPOOL_SIZE") with _ -> 400)
(* only do dyn-trans if conflict has more than this many lits *)
let min_confl_len = (try int_of_string (Sys.getenv "MIN_CONFL_LEN") with _ -> 6)
let min_confl_len = (try int_of_string (Sys.getenv "MIN_CONFL_LEN") with _ -> 4)
let max_batch_size = (try int_of_string (Sys.getenv "MAX_BATCH_SIZE") with _ -> 2)
let activity_bump = (try float_of_string (Sys.getenv "ACTIVITY_BUMP") with _ -> 1.1)
let min_activity = (try float_of_string (Sys.getenv "MIN_ACTIVITY") with _ -> 1e12)
let max_activity = min_activity *. (activity_bump ** 15.)
let activity_decay = activity_bump ** (-13.)
(* RULES *)
(* TODO: some rate limiting system (a counter that goes up when cc conflict,
@ -120,6 +127,12 @@ module Make(A: ARG)
match A.term_as_eqn self.tstore (Lit.term lit) with
| Some (t,u) when not (Term.equal t u) -> Some (t,u,lit)
| _ -> None)
|> Iter.filter
(fun (t,u,_) ->
let act_t = Term.Tbl.get_or self.activity t ~default:1. in
let act_u = Term.Tbl.get_or self.activity u ~default:1. in
let keep = act_t >= min_activity || act_u >= min_activity in
keep)
|> Iter.iter
(fun (t,u,lit) ->
on_eqn t u lit;
@ -149,7 +162,31 @@ module Make(A: ARG)
end;
()
(* bump activity of all terms involved in CC conflict *)
let update_activity_from_cc_confl (self:t) (lits:Lit.t list) : unit =
let update_term t : unit =
let f = Term.Tbl.get_or ~default:1. self.activity t in
let f = f *. activity_bump in
Term.Tbl.replace self.activity t f;
(* decay all *)
if f > max_activity then (
Term.Tbl.iter
(fun t f -> Term.Tbl.replace self.activity t (max 1. (f *. activity_decay)))
self.activity;
);
in
let update_lit lit =
let t = Lit.term lit in
match A.term_as_eqn self.tstore t with
| None -> ()
| Some (t,u) ->
update_term t;
update_term u
in
List.iter update_lit lits
let on_conflict (self:t) (cc:CC.t) ~th lits : unit =
update_activity_from_cc_confl self lits;
if not th && List.length lits >= min_confl_len then (
inst_from_conflict self cc lits
)
@ -160,6 +197,7 @@ module Make(A: ARG)
tstore=SI.tst si;
cc=SI.cc si;
sat;
activity=Term.Tbl.create 16;
done_inst=Inst_tbl.create 32;
cpool=SAT.new_clause_pool_gc_fixed_size
~descr:"cp.dyn-trans" ~size:cpool_size sat;