Here's how to do that in our framework:
type clause_op = bool dpm -> bool dpm set;;
+
+ (* filter out which bool dpms in a set are true when receiving (r, h) as input *)
+ let extensions set (r, h) = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set;;
let negate_op (phi : clause_op) : clause_op =
fun one_dpm -> unit_set (
fun (r, h) ->
- let extensions set = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set
- in let truth_value' = extensions (phi one_dpm) = []
+ let truth_value' = extensions (phi one_dpm) (r, h) = []
in (truth_value', r, h)
)
(* NOT: negate_op (and_op (negate_op phi) (negate_op psi)) *)
fun one_dpm -> unit_set (
fun (r, h) ->
- let extensions set = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set
- in let truth_value' = extensions (phi one_dpm) <> [] || extensions (bind_set (negate_op phi one_dpm) psi) <> []
+ in let truth_value' = extensions (phi one_dpm) (r, h) <> [] || extensions (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
in (truth_value', r, h))
let if_op (phi : clause_op) (psi : clause_op) : clause_op =
(* NOT: negate_op (and_op phi (negate_op psi)) *)
fun one_dpm -> unit_set (
fun (r, h) ->
- let extensions set = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set
- in let truth_value' = List.for_all (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value = false || extensions (psi one_dpm) <> []) (phi one_dpm)
+ in let truth_value' = List.for_all (fun one_dpm ->
+ let (truth_value, _, _) = one_dpm (r, h)
+ in truth_value = false || extensions (psi one_dpm) (r, h) <> []
+ ) (phi one_dpm)
in (truth_value', r, h));;