package mc2

  1. Overview
  2. Docs

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

open Solver_types

type t = reason

let pp out = function
  | n, _ when n < 0 ->
    Format.fprintf out "%%"
  | n, Decision ->
    Format.fprintf out "@@%d" n
  | n, Bcp c ->
    Format.fprintf out "#%d@<1>←%s%d" n (Premise.prefix c.c_premise) c.c_name
  | n, Bcp_lazy c ->
    if Lazy.is_val c
    then (
      let lazy c = c in
      Format.fprintf out "#%d@<1>←%s%d" n (Premise.prefix c.c_premise) c.c_name
    ) else Format.fprintf out "#%d@<1>←<lazy>" n
  | n, Eval _ ->
    Format.fprintf out "$%d" n

let pp_opt out = function
  | n, _ when n < 0 ->
    Format.fprintf out "%%"
  | n, None ->
    Format.fprintf out "%d" n
  | n, Some r -> pp out (n,r)