(* ============================================ Boolean circuits ============================================ *) (* _________ Types _________ *) type var = string type id = int type op = | CIn of int | COut | CShare | CAnd | COr | CNeg type input = id type gate = input list * op * id type circuit = gate list (* _________ Getters _________ *) let get_node_info circ node = let (ins, op, i) = List.hd (List.filter (fun (_, _, i) -> i = node) circ) in (ins, op) let get_inputs circ node = let (ins, _) = get_node_info circ node in ins let get_op circ node = let (_, op) = get_node_info circ node in op (* extracts the two first inputs in a list of inputs *) let extract_bin_ins = function | [] -> failwith "Error extract_bin_ins: no input." | h1::h2::t -> (h1, h2) | _ -> failwith "Error extract_bin_ins: inputs do not match." (* _________ Evaluation _________ *) (* provides the boolean value of the node 'concl' in a circuit 'circ' *) let rec value circ concl = match get_op circ concl with | CIn i -> i | CShare | COut -> let x = List.hd (get_inputs circ concl) in value circ x | CAnd -> let (x, y) = extract_bin_ins (get_inputs circ concl) in let vx = value circ x in let vy = value circ y in min vx vy | COr -> let (x, y) = extract_bin_ins (get_inputs circ concl) in let vx = value circ x in let vy = value circ y in max vx vy | CNeg -> let x = List.hd (get_inputs circ concl) in let vx = value circ x in 1 - vx | _ -> -1 let rec eval (circ : circuit) : int = let (_, _, concl) = List.hd (List.filter (fun (_, o, _) -> o = COut) circ) in value circ concl (* _________ Examples _________ *) let make_gate ins op id = (ins, op, id) let make_input value id = ([], CIn value, id) let make_and_circ x y = [ make_input x 0; make_input y 1; make_gate [0;1] CAnd 2; make_gate [2] COut 3 ] let make_or_circ x y = [ make_input x 0; make_input y 1; make_gate [0;1] COr 2; make_gate [2] COut 3 ] let make_neg_circ x = [ make_input x 0; make_gate [0] CNeg 1; make_gate [1] COut 2 ] (* corresponds to the excluded middle x v ~x *) let make_em_circ x = [ make_input x 0; make_gate [0] CShare 1; make_gate [1] CNeg 2; make_gate [1;2] COr 3; make_gate [3] COut 4 ]