From 93806220963838831fa362cbcba9241e9f0a5245 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 3 May 2021 10:35:55 -0400 Subject: [PATCH] small refactor --- src/cc/Sidekick_cc.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 811e4dce..e434ed22 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -573,7 +573,8 @@ module Make (A: CC_ARG) on_backtrack cc (fun () -> n.n_as_lit <- None); 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) (* 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 keep values as representative *) let r_from, r_into = - if n_is_bool cc ra then rb, ra - else if n_is_bool cc rb then ra, rb + if n_is_bool_value cc ra then rb, ra + else if n_is_bool_value cc rb then ra, rb else if size_ ra > size_ rb then rb, ra else ra, rb in