open Printf
       
type boolform = V of string
              | Neg of boolform
              | And of boolform * boolform 
              | Or of boolform * boolform 

type lit = P of string | N of string                                    

(*********************** Exercitii ajutatoare **********************)

(* 1. doar numaram operatorii -- tema 6 *)                
let cntoplast =
  let rec cntop n = function
    | V s -> n
    | Neg e -> 1 + cntop n e
    | And (e1, e2) | Or (e1, e2) -> 1 + cntop (cntop n e1) e2
  in cntop 0

(* 2. tiparim operatorii si numele/numerele subexpresiilor -- tema 7 *)
let cntname =                (* tiparim la fiecare operator si subformulele *)
  let rec cntn n =
    let oneexp e1 =        (* obtinem numele expresiei si tratam o subexpresie *)
      ("_" ^ (string_of_int n), cntn (n+1) e1)
    in let binop op e1 e2 =        (* partea comuna pentru operatorii binari *)
         let (s, (n1, s1)) = oneexp e1 in        (* prima subexpresie *)
         let (n2, s2) = cntn n1 e2 in
         printf "%s = %s %c %s\n" s s1 op s2; (n2, s)
       in function        (* definitia lui cntn *)
       | V s -> (n, s)
       | Neg e -> let (s, (n1, s1)) = oneexp e in
                  printf "%s = ~%s\n" s s1; (n1, s)
       | And (e1, e2) -> binop '+' e1 e2
       | Or (e1, e2) -> binop '*' e1 e2
  in cntn 1

(************************** Solutia propriu-zisa ********************)

let tseitin e =                (* acum returnam si o lista *)
  let rec ts1 n lst =
    let s = "_" ^ (string_of_int n)
    in function
    | V s -> (n, s, lst)
    | Neg e -> let (n1, s1, lst1) = ts1 (n+1) lst e
               in (n1, s, [P s; P s1]::[N s; N s1] :: lst1)
    | And (e1, e2) -> let (n1, s1, lst1) = ts1 (n+1) lst e1 in
                      let (n2, s2, lst2) = ts1 n1 lst1 e2 in
                      (n2, s, [P s; N s1; N s2]::[N s; P s1]::[N s; P s2]::lst2)
    | Or (e1, e2) -> let (n1, s1, lst1) = ts1 (n+1) lst e1 in
                     let (n2, s2, lst2) = ts1 n1 lst1 e2 in
                     (n2, s, [N s; P s1; P s2]::[P s; N s1]::[P s; N s2]::lst2)
  in let (_, s, lst) = ts1 0 [] e in [P s]::lst
;;
tseitin (And (Or (V "a", V "b"), Neg (V "c")))

This document was generated using caml2html