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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
open Solver_types
type t = atom
let[@inline] equal a b = a.a_id = b.a_id
let[@inline] compare a b = CCInt.compare a.a_id b.a_id
let[@inline] hash a = CCHash.int a.a_id
let[@inline] same_term a b = a.a_term == b.a_term
let[@inline] is_pos (a:t) : bool = match a.a_term.t_var with
| Var_bool { pa; _ } -> a==pa
| Var_none | Var_semantic _ -> assert false
let[@inline] is_neg (a:t) : bool = not (is_pos a)
let[@inline] neg (a:t) : t = match a.a_term.t_var with
| Var_bool { pa; na; _ } -> if a==pa then na else pa
| Var_none | Var_semantic _ -> assert false
let[@inline] abs (a:t) : t = match a.a_term.t_var with
| Var_bool { pa; _ } -> pa
| Var_none | Var_semantic _ -> assert false
let[@inline] value (a:t): value option =
if is_pos a then Term.value a.a_term
else CCOpt.map Value.bool_neg (Term.value a.a_term)
let[@inline] is_true (a:t): bool =
if is_pos a
then Term.has_value a.a_term Value.true_
else Term.has_value a.a_term Value.false_
let[@inline] is_false (a:t): bool =
if is_pos a
then Term.has_value a.a_term Value.false_
else Term.has_value a.a_term Value.true_
let[@inline] has_some_value (a:t): bool = Term.has_some_value a.a_term
let[@inline] is_undef (a:t): bool = not (has_some_value a)
let[@inline] reason (a:t) : reason option = Term.reason a.a_term
let[@inline] reason_exn (a:t) : reason = Term.reason_exn a.a_term
let[@inline] term (a:t) = a.a_term
let[@inline] level (a:t) = Term.level a.a_term
let[@inline] watched (a:t) = a.a_watched
let[@inline] field_ (a:t) : Term_fields.field =
if is_pos a then field_t_mark_pos else field_t_mark_neg
let[@inline] mark (a:t) =
a.a_term.t_fields <- Term_fields.set (field_ a) true a.a_term.t_fields
let[@inline] unmark (a:t) =
a.a_term.t_fields <- Term_fields.set (field_ a) false a.a_term.t_fields
let[@inline] marked (a:t) : bool =
Term_fields.get (field_ a) a.a_term.t_fields
let pp_level fmt a = Reason.pp_opt fmt (level a, reason a)
let[@inline] mark_neg (a:t) = mark (neg a)
let[@inline] unmark_neg (a:t) = unmark (neg a)
let[@inline] eval (a:t) : eval_res =
begin match Term.eval (term a) with
| Eval_unknown -> Eval_unknown
| Eval_into (v, subs) ->
let v = if is_pos a then v else Value.bool_neg v in
Eval_into (v, subs)
end
let[@inline] is_absurd (a:t) : bool = match eval a with
| Eval_into (V_false,[]) -> true
| Eval_into (V_false,l) -> List.for_all (fun u -> Term.level u=0) l
| _ -> false
let[@inline] can_eval_to_false a = match eval a with
| Eval_into (V_false, _) -> true
| _ -> false
let pp_value fmt a =
if is_true a then
Format.fprintf fmt "T%a" pp_level a
else if is_true (neg a) then
Format.fprintf fmt "F%a" pp_level a
let debug out a =
let sign = if is_pos a then "" else "¬" in
let m_sign = if marked a then "[M]" else "" in
Format.fprintf out "%s%a[%a]%s"
sign Term.debug_no_val a.a_term pp_value a m_sign
let pp out a =
let sign = if is_pos a then "" else "¬" in
Format.fprintf out "%s%a" sign Term.pp a.a_term
module As_key = struct
type t = atom
let hash = hash
let equal = equal
let compare = compare
end
module Tbl = CCHashtbl.Make(As_key)
module Set = CCSet.Make(As_key)