You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
98 lines
2.3 KiB
98 lines
2.3 KiB
(* ============================================ |
|
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 |
|
|
|
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 : gate = (ins, op, id) |
|
let make_input value id : gate = ([], CIn value, id) |
|
|
|
let make_and_circ x y : circuit = [ |
|
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 : circuit = [ |
|
make_input x 0; |
|
make_input y 1; |
|
make_gate [0;1] COr 2; |
|
make_gate [2] COut 3 |
|
] |
|
|
|
let make_neg_circ x : circuit = [ |
|
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 : circuit = [ |
|
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 |
|
] |