<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* ========================================================================= *)
(* Definitional CNF.                                                         *)
(*                                                                           *)
(* Copyright (c) 2003, John Harrison. (See "LICENSE.txt" for details.)       *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Variant of NNF without splitting equivalences.                            *)
(* ------------------------------------------------------------------------- *)

let rec nenf fm =
  match fm with
    Not(Not p) -> nenf p
  | Not(And(p,q)) -> Or(nenf(Not p),nenf(Not q))
  | Not(Or(p,q)) -> And(nenf(Not p),nenf(Not q))
  | Not(Imp(p,q)) -> And(nenf p,nenf(Not q))
  | Not(Iff(p,q)) -> Iff(nenf p,nenf(Not q))
  | And(p,q) -> And(nenf p,nenf q)
  | Or(p,q) -> Or(nenf p,nenf q)
  | Imp(p,q) -> Or(nenf(Not p),nenf q)
  | Iff(p,q) -> Iff(nenf p,nenf q)
  | _ -> fm;;

(* ------------------------------------------------------------------------- *)
(* Make a stylized variable and update the index.                            *)
(* ------------------------------------------------------------------------- *)

let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;;

(* ------------------------------------------------------------------------- *)
(* Make n large enough that "v_m" won't clash with s for any m >= n          *)
(* ------------------------------------------------------------------------- *)

let max_varindex pfx =
  let m = String.length pfx in
  fun s n ->
    let l = String.length s in
    if l <= m or String.sub s 0 m <> pfx then n else
    let s' = String.sub s m (l - m) in
    if forall numeric (explode s') then max_num n (num_of_string s')
    else n;;

(* ------------------------------------------------------------------------- *)
(* Basic definitional CNF procedure.                                         *)
(* ------------------------------------------------------------------------- *)

let rec maincnf (fm,defs,n as trip) =
  match fm with
    And(p,q) -> defstep (fun (p,q) -> And(p,q)) (p,q) trip
  | Or(p,q) -> defstep (fun (p,q) -> Or(p,q)) (p,q) trip
  | Iff(p,q) -> defstep (fun (p,q) -> Iff(p,q)) (p,q) trip
  | _ -> trip

and defstep op (p,q) (fm,defs,n) =
  let fm1,defs1,n1 = maincnf (p,defs,n) in
  let fm2,defs2,n2 = maincnf (q,defs1,n1) in
  let fm' = op(fm1,fm2) in
  try (fst(apply defs2 fm'),defs2,n2) with Failure _ ->
  let v,n3 = mkprop n2 in (v,(fm'|->(v,Iff(v,fm'))) defs2,n3);;

let defcnf fm =
  let fm' = nenf(psimplify fm) in
  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
  let (fm'',defs,_) = maincnf (fm',undefined,n) in
  let deflist = map (snd ** snd) (funset defs) in
  let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in
  list_conj (map list_disj (setify subcnfs));;

(* ------------------------------------------------------------------------- *)
(* Example.                                                                  *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
let fm = <<(p \/ (q /\ ~r)) /\ s>>;;

defcnf fm;;

cnf fm;;

cnf <<p <=> (q <=> r)>>;;
END_INTERACTIVE;;

(* ------------------------------------------------------------------------- *)
(* Version tweaked to exploit initial structure.                             *)
(* ------------------------------------------------------------------------- *)

let subcnf sfn op (p,q) (fm,defs,n) =
  let fm1,defs1,n1 = sfn(p,defs,n) in
  let fm2,defs2,n2 = sfn(q,defs1,n1) in (op(fm1,fm2),defs2,n2);;

let rec orcnf (fm,defs,n as trip) =
  match fm with
    Or(p,q) -> subcnf orcnf (fun (p,q) -> Or(p,q)) (p,q) trip
  | _ -> maincnf trip;;

let rec andcnf (fm,defs,n as trip) =
  match fm with
    And(p,q) -> subcnf andcnf (fun (p,q) -> And(p,q)) (p,q) trip
  | _ -> orcnf trip;;

let defcnfs fm =
  let fm' = nenf(psimplify fm) in
  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
  let (fm'',defs,_) = andcnf (fm',undefined,n) in
  let deflist = map (snd ** snd) (funset defs) in
  setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;

let defcnf fm = list_conj (map list_disj (defcnfs fm));;

(* ------------------------------------------------------------------------- *)
(* Examples.                                                                 *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
defcnf fm;;
END_INTERACTIVE;;

(* ------------------------------------------------------------------------- *)
(* Version using only implication where possible.                            *)
(* ------------------------------------------------------------------------- *)

let defstep pos sfn op (p,q) (fm,defs,n) =
  let fm1,defs1,n1 = sfn (p,defs,n) in
  let fm2,defs2,n2 = sfn (q,defs1,n1) in
  let (fl,fm' as ffm') = (pos,op(fm1,fm2)) in
  try (fst(apply defs2 ffm'),defs2,n2) with Failure _ ->
  let (v,n3) = mkprop n2 in
  let cons = if pos then fun (p,q) -> Imp(p,q)
             else fun (p,q) -> Iff(p,q) in
  (v,(ffm' |-> (v,cons(v,fm'))) defs2,n3);;

let rec maincnf pos (fm,defs,n as trip) =
  match fm with
    And(p,q) ->
        defstep pos (maincnf pos) (fun (p,q) -> And(p,q)) (p,q) trip
  | Or(p,q) ->
        defstep pos (maincnf pos) (fun (p,q) -> Or(p,q)) (p,q) trip
  | Iff(p,q) ->
        defstep pos (maincnf false) (fun (p,q) -> Iff(p,q)) (p,q) trip
  | _ -> trip;;

let rec orcnf pos (fm,defs,n as trip) =
  match fm with
    Or(p,q) -> subcnf (orcnf pos) (fun (p,q) -> Or(p,q)) (p,q) trip
  | _ -> maincnf pos trip;;

let rec andcnf pos (fm,defs,n as trip) =
  match fm with
    And(p,q) -> subcnf (andcnf pos) (fun (p,q) -> And(p,q)) (p,q) trip
  | _ -> orcnf pos trip;;

let defcnfs imps fm =
  let fm' = nenf(psimplify fm) in
  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
  let (fm'',defs,_) = andcnf imps (fm',undefined,n) in
  let deflist = map (snd ** snd) (funset defs) in
  setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;

let defcnf imps fm = list_conj (map list_disj (defcnfs imps fm));;

(* ------------------------------------------------------------------------- *)
(* Example.                                                                  *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
defcnf false fm;;

defcnf true fm;;
END_INTERACTIVE;;

(* ------------------------------------------------------------------------- *)
(* Version that guarantees 3-CNF.                                            *)
(* ------------------------------------------------------------------------- *)

let rec andcnf3 pos (fm,defs,n as trip) =
  match fm with
    And(p,q) -> subcnf (andcnf3 pos) (fun (p,q) -> And(p,q)) (p,q) trip
  | _ -> maincnf pos trip;;

let defcnf3s imps fm =
  let fm' = nenf(psimplify fm) in
  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
  let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in
  let deflist = map (snd ** snd) (funset defs) in
  setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;

let defcnf3 imps fm = list_conj (map list_disj (defcnf3s imps fm));;

(* ------------------------------------------------------------------------- *)
(* Example.                                                                  *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
let fm = <<(p \/ q \/ r \/ s) /\ ~p /\ (~p \/ q)>>;;

defcnf true fm;;

defcnf3 true fm;;
END_INTERACTIVE;;