67 lines
1.7 KiB
OCaml
67 lines
1.7 KiB
OCaml
type formule =
|
|
| Var of int
|
|
| Not of formule
|
|
| Imply of formule*formule
|
|
| Equiv of formule*formule
|
|
| And of formule list
|
|
| Or of formule list;;
|
|
|
|
let f = And [Or [Var 0; Var 1; Var 2]; Not (Var 0)];;
|
|
let g = Equiv (Var 0, And [Var 1; Var 2]);;
|
|
let rec evaluer_tab t form = match form with
|
|
| Var i -> t.(i)
|
|
| Not f -> not (evaluer_tab t f)
|
|
| Imply (f1,f2) -> (not (evaluer_tab t f1)) || (evaluer_tab t f2)
|
|
| Equiv (f1,f2) -> (evaluer_tab t f1) = (evaluer_tab t f2)
|
|
| And [] -> true
|
|
| And (h::tail) -> (evaluer_tab t h) && (evaluer_tab t (And tail))
|
|
| Or [] -> false
|
|
| Or (h::tail) -> (evaluer_tab t h) || (evaluer_tab t (Or tail));;
|
|
5 lsr 1;;
|
|
|
|
let contexte_from_int n c =
|
|
let contexte = Array.make n false in
|
|
let j = ref c in
|
|
for i = 0 to n-1 do
|
|
contexte.(i) <- !j mod 2 <> 0;
|
|
j := !j lsr 1
|
|
done;
|
|
contexte;;
|
|
|
|
let evaluer n c f =
|
|
let contexte = contexte_from_int n c in
|
|
evaluer_tab contexte f;;
|
|
|
|
evaluer 3 3 g;;
|
|
|
|
let table_de_verite n f =
|
|
let rec puis n a = match n with
|
|
| 0 -> 1
|
|
| _ -> a * (puis (n-1) a) in
|
|
let res = Array.make (puis n 2) false in
|
|
for c=0 to ((Array.length res) -1) do
|
|
res.(c) <- evaluer n c f
|
|
done;
|
|
res;;
|
|
table_de_verite 3 g;;
|
|
|
|
let forme_normale_disjonctive n f =
|
|
let rec puis n a = match n with
|
|
| 0 -> 1
|
|
| _ -> a * (puis (n-1) a) in
|
|
|
|
let rec disjonction c conjs =
|
|
|
|
let rec conjonction cont conj n = match n with
|
|
| -1 -> And conj
|
|
| _ -> conjonction cont ((if cont.(n) then (Var n) else Not (Var n))::conj) (n-1) in
|
|
|
|
match c with
|
|
| -1 -> Or conjs
|
|
| _ -> let contexte = context_from_int n c in
|
|
if evaluer_tab contexte f then
|
|
disjonction (c-1) ((conjonction contexte [] (n-1))::conjs)
|
|
else
|
|
disjonction (c-1) conjs in
|
|
disjonction ((puis n 2) -1) [];;
|
|
forme_normale_disjonctive 3 g;; |