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

small refactor

Browse source
This commit is contained in:
Simon Cruanes 2021-05-03 10:35:55 -04:00
parent 7b2b11486f
commit 9380622096
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

@ -573,7 +573,8 @@ module Make (A: CC_ARG)
on_backtrack cc (fun () -> n.n_as_lit <- None); on_backtrack cc (fun () -> n.n_as_lit <- None);
n.n_as_lit <- Some lit n.n_as_lit <- Some lit
let n_is_bool (self:t) n : bool = (* is [n] true or false? *)
let n_is_bool_value (self:t) n : bool =
N.equal n (n_true self) || N.equal n (n_false self) N.equal n (n_true self) || N.equal n (n_false self)
(* main CC algo: add terms from [pending] to the signature table, (* main CC algo: add terms from [pending] to the signature table,
@ -657,8 +658,8 @@ module Make (A: CC_ARG)
we try to ensure that [size ra <= size rb] in general, but always we try to ensure that [size ra <= size rb] in general, but always
keep values as representative *) keep values as representative *)
let r_from, r_into = let r_from, r_into =
if n_is_bool cc ra then rb, ra if n_is_bool_value cc ra then rb, ra
else if n_is_bool cc rb then ra, rb else if n_is_bool_value cc rb then ra, rb
else if size_ ra > size_ rb then rb, ra else if size_ ra > size_ rb then rb, ra
else ra, rb else ra, rb
in in