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

perf(cc): only assign model values to term present in CC

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 21:20:17 -05:00
parent 6e941683a2
commit da18ba3620
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/cc/Sidekick_cc.ml
View file

@ -1112,9 +1112,10 @@ module Make (A: CC_ARG)
merge cc (add_term cc t1) (add_term cc t2) expl merge cc (add_term cc t1) (add_term cc t2) expl
let set_model_value (self:t) (t:term) (v:value) : unit = let set_model_value (self:t) (t:term) (v:value) : unit =
assert (self.model_mode); (* only valid there *) assert (self.model_mode); (* only valid in model mode *)
let n = add_term self t in match T_tbl.find_opt self.tbl t with
Vec.push self.combine (CT_set_val (n,v)) | None -> () (* ignore, th combination not needed *)
| Some n -> Vec.push self.combine (CT_set_val (n,v))
let explain_eq cc n1 n2 : Resolved_expl.t = let explain_eq cc n1 n2 : Resolved_expl.t =
let st = Expl_state.create() in let st = Expl_state.create() in