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

remove useless functions

Browse source
This commit is contained in:
Simon Cruanes 2017-12-29 19:12:17 +01:00
parent d47071c4f0
commit be929d056a
2 changed files with 0 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Solver_types.ml
View file

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

16
src/core/Solver_types_intf.ml
View file

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