Source file Mc2_propositional.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

(** {1 Propositional Literal} *)

open Mc2_core

module Fmt = CCFormat

type t = atom

let name = "propositional"
let neg = Atom.neg
let pp = Atom.pp

module F = Tseitin.Make(Atom)

(* add new case for terms *)
type term_view += Fresh of int

(* printer for terms *)
let pp out = function
  | Fresh i -> Fmt.fprintf out "_A%d" i
  | _ -> assert false

(* typeclass for terms *)
let t_tc : tc_term = Term.TC.make ~pp ()

let k_cnf = Service.Key.make "propositional.cnf"
let k_fresh = Service.Key.make "propositional.fresh"

let plugin =
  let build p_id Plugin.S_nil : Plugin.t =
    let module P : Plugin.S = struct
      let id = p_id
      let name = name
      (* term allocator *)
      module T_alloc = Term.Term_allocator(struct
          let tc = Term.TC.lazy_from_val t_tc
          let p_id = p_id
          let initial_size=64
          let[@inline] equal v1 v2 = match v1, v2 with
            | Fresh i, Fresh j -> i=j
            | _ -> assert false
          let[@inline] hash = function Fresh i -> CCHash.int i | _ -> assert false
        end)

      let check_if_sat _ = Sat

      let gc_all = T_alloc.gc_all
      let iter_terms = T_alloc.iter_terms

      let fresh : unit -> t =
        let n = ref 0 in
        fun () ->
          let view = Fresh !n in
          incr n;
          let t = T_alloc.make view Type.bool in
          Term.Bool.pa t

      let[@inline] cnf ?simplify (f:F.t) : t list list = F.cnf ~fresh ?simplify f

      let provided_services =
        [ Service.Any (k_fresh, fresh);
          Service.Any (k_cnf, cnf);
        ]
    end
    in
    (module P : Plugin.S)
  in
  Plugin.Factory.make ~priority:5 ~name ~requires:Plugin.K_nil ~build ()