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

remove useless fields

Browse source
This commit is contained in:
Simon Cruanes 2018-05-28 01:31:34 -05:00
parent 10d394a9c3
commit 20ecdd6c1f
2 changed files with 0 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/Equiv_class.ml
View file

@ -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()

18
src/smt/Equiv_class.mli
View file

@ -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 *)