diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index a5663bcb..8b399a31 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -178,13 +178,8 @@ module McMake (E : Expr_intf.S) = struct type t = lit let[@inline] term l = l.term let[@inline] level l = l.l_level - let[@inline] set_level l lvl = l.l_level <- lvl - let[@inline] assigned l = l.assigned - let[@inline] set_assigned l t = l.assigned <- t - let[@inline] weight l = l.l_weight - let[@inline] set_weight l w = l.l_weight <- w let make (st:state) (t:term) : t = try MT.find st.t_map t @@ -219,15 +214,11 @@ module McMake (E : Expr_intf.S) = struct type t = var let dummy = dummy_var let[@inline] level v = v.v_level - let[@inline] set_level v lvl = v.v_level <- lvl let[@inline] pos v = v.pa let[@inline] neg v = v.na let[@inline] reason v = v.reason - let[@inline] set_reason v r = v.reason <- r let[@inline] assignable v = v.v_assignable - let[@inline] set_assignable v x = v.v_assignable <- x let[@inline] weight v = v.v_weight - let[@inline] set_weight v w = v.v_weight <- w let make (st:state) (t:formula) : var * Expr_intf.negated = let lit, negated = E.Formula.norm t in diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml index 643bc06d..f073456c 100644 --- a/src/core/Solver_types_intf.ml +++ b/src/core/Solver_types_intf.ml @@ -159,12 +159,8 @@ module type S = sig (** Returns the variable associated with the term *) val level : t -> int - val set_level : t -> int -> unit - val assigned : t -> term option - val set_assigned : t -> term option -> unit val weight : t -> float - val set_weight : t -> float -> unit val pp : t printer val debug : t printer @@ -178,13 +174,9 @@ module type S = sig val neg : t -> atom val level : t -> int - val set_level : t -> int -> unit val reason : t -> reason option - val set_reason : t -> reason option -> unit val assignable : t -> lit list option - val set_assignable : t -> lit list option -> unit val weight : t -> float - val set_weight : t -> float -> unit val make : state -> formula -> t * Formula_intf.negated (** Returns the variable linked with the given formula, @@ -255,14 +247,6 @@ module type S = sig val atoms : t -> Atom.t array val tag : t -> int option val premise : t -> premise - val set_premise : t -> premise -> unit - - val visited : t -> bool - val set_visited : t -> bool -> unit - val attached : t -> bool - val set_attached : t -> bool -> unit - val activity : t -> float - val set_activity : t -> float -> unit val empty : t (** The empty clause *)