Source file trail.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Boolean Trail} *)

open Logtk

module Lit = BBox.Lit

type bool_lit = Lit.t

type t = Lit.Set.t

let equal = Lit.Set.equal
let compare = Lit.Set.compare
let hash trail = Hash.seq Lit.hash (Lit.Set.to_iter trail)

let empty = Lit.Set.empty
let mem = Lit.Set.mem
let for_all = Lit.Set.for_all
let exists = Lit.Set.exists
let singleton = Lit.Set.singleton
let add = Lit.Set.add
let remove = Lit.Set.remove
let fold f acc t = Lit.Set.fold (fun x acc -> f acc x) t acc
let length = Lit.Set.cardinal
let map f set =
  Lit.Set.to_iter set
  |> Iter.map f
  |> Lit.Set.of_iter
let of_list = Lit.Set.of_list
let add_list = Lit.Set.add_list
let to_list = Lit.Set.to_list
let is_empty = Lit.Set.is_empty

let subsumes t1 t2 = Lit.Set.subset t1 t2

let is_trivial trail =
  Lit.Set.exists
    (fun i -> Lit.Set.mem (Lit.neg i) trail)
    trail

let merge = Lit.Set.union

let merge_l = function
  | [] -> Lit.Set.empty
  | [t] -> t
  | [t1;t2] -> Lit.Set.union t1 t2
  | t::l -> List.fold_left Lit.Set.union t l

let filter = Lit.Set.filter

type valuation = Lit.t -> bool
(** A boolean valuation *)

let is_active trail ~v =
  Lit.Set.for_all
    (fun i ->
       let j = Lit.abs i in
       (Lit.sign i) = (v j))  (* valuation match sign *)
    trail

let to_iter = Lit.Set.to_iter

let labels (t:t) =
  to_iter t
  |> Iter.map BBox.Lit.to_int
  |> Util.Int_set.of_iter

let to_s_form (t:t) =
  let module F = TypedSTerm.Form in
  begin match to_list t |> List.map BBox.to_s_form with
    | [] -> F.true_
    | [f] -> f
    | l -> F.and_ l
  end