From 20ecdd6c1f24edab72ead74d51d55b961ce1195e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 28 May 2018 01:31:34 -0500 Subject: [PATCH] remove useless fields --- src/smt/Equiv_class.ml | 5 ----- src/smt/Equiv_class.mli | 18 ------------------ 2 files changed, 23 deletions(-) diff --git a/src/smt/Equiv_class.ml b/src/smt/Equiv_class.ml index 33488346..ca534589 100644 --- a/src/smt/Equiv_class.ml +++ b/src/smt/Equiv_class.ml @@ -4,11 +4,6 @@ open Solver_types type t = cc_node type payload = cc_node_payload = .. -let field_expanded = Node_bits.mk_field () -let field_has_expansion_lit = Node_bits.mk_field () -let field_is_lit = Node_bits.mk_field () -let field_is_split = Node_bits.mk_field () -let field_add_level_0 = Node_bits.mk_field() let field_is_active = Node_bits.mk_field() let () = Node_bits.freeze() diff --git a/src/smt/Equiv_class.mli b/src/smt/Equiv_class.mli index 482574a7..22677578 100644 --- a/src/smt/Equiv_class.mli +++ b/src/smt/Equiv_class.mli @@ -23,24 +23,6 @@ open Solver_types type t = cc_node type payload = cc_node_payload = .. -val field_expanded : Node_bits.field -(** Term is expanded? *) - -val field_has_expansion_lit : Node_bits.field -(** Upon expansion, does this term have a special literal [Lit_expanded t] - that should be asserted? *) - -val field_is_lit : Node_bits.field -(** Is this term a boolean literal? *) - -val field_is_split : Node_bits.field -(** Did we perform case split (Split 1) on this term? - This is only relevant for terms whose type is a datatype. *) - -val field_add_level_0 : Node_bits.field -(** Is the corresponding term to be re-added upon backtracking, - down to level 0? *) - val field_is_active : Node_bits.field (** The term is needed for evaluation. We must try to evaluate it or to find a value for it using the theory *)