Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ========================================================================= *) (* Introduction to quantifier elimination. *) (* *) (* Copyright (c) 2003, John Harrison. (See "LICENSE.txt" for details.) *) (* ========================================================================= *) let rec disjuncts fm = match fm with Or(p,q) -> disjuncts p @ disjuncts q | _ -> [fm];; let rec conjuncts fm = match fm with And(p,q) -> conjuncts p @ conjuncts q | _ -> [fm];; (* ------------------------------------------------------------------------- *) (* Lift procedure given literal modifier, formula normalizer, and a basic *) (* elimination procedure for existential formulas with conjunctive body. *) (* ------------------------------------------------------------------------- *) let lift_qelim afn nfn qfn = let rec qelift vars fm = match fm with | Atom(R(_,_)) -> afn vars fm | Not(p) -> Not(qelift vars p) | And(p,q) -> And(qelift vars p,qelift vars q) | Or(p,q) -> Or(qelift vars p,qelift vars q) | Imp(p,q) -> Imp(qelift vars p,qelift vars q) | Iff(p,q) -> Iff(qelift vars p,qelift vars q) | Forall(x,p) -> Not(qelift vars (Exists(x,Not p))) | Exists(x,p) -> let djs = disjuncts(nfn(qelift (x::vars) p)) in list_disj(map (qelim x vars) djs) | _ -> fm and qelim x vars p = let cjs = conjuncts p in let ycjs,ncjs = partition (mem x ** fv) cjs in if ycjs = [] then p else let q = qfn vars (Exists(x,list_conj ycjs)) in itlist (fun p q -> And(p,q)) ncjs q in fun fm -> simplify(qelift (fv fm) fm);; (* ------------------------------------------------------------------------- *) (* Cleverer (proposisional) NNF with conditional and literal modification. *) (* ------------------------------------------------------------------------- *) let cnnf lfn = let rec cnnf fm = match fm with And(p,q) -> And(cnnf p,cnnf q) | Or(p,q) -> Or(cnnf p,cnnf q) | Imp(p,q) -> Or(cnnf(Not p),cnnf q) | Iff(p,q) -> Or(And(cnnf p,cnnf q),And(cnnf(Not p),cnnf(Not q))) | Not(Not p) -> cnnf p | Not(And(p,q)) -> Or(cnnf(Not p),cnnf(Not q)) | Not(Or(And(p,q),And(p',r))) when p' = negate p -> Or(cnnf (And(p,Not q)),cnnf (And(p',Not r))) | Not(Or(p,q)) -> And(cnnf(Not p),cnnf(Not q)) | Not(Imp(p,q)) -> And(cnnf p,cnnf(Not q)) | Not(Iff(p,q)) -> Or(And(cnnf p,cnnf(Not q)), And(cnnf(Not p),cnnf q)) | _ -> lfn fm in simplify ** cnnf ** simplify;; (* ------------------------------------------------------------------------- *) (* Initial literal simplifier and intermediate literal modifier. *) (* ------------------------------------------------------------------------- *) let lfn_dlo fm = match fm with Not(Atom(R("<",[s;t]))) -> Or(Atom(R("=",[s;t])),Atom(R("<",[t;s]))) | Not(Atom(R("=",[s;t]))) -> Or(Atom(R("<",[s;t])),Atom(R("<",[t;s]))) | _ -> fm;; (* ------------------------------------------------------------------------- *) (* Simple example of dense linear orderings; this is the base function. *) (* ------------------------------------------------------------------------- *) let dlobasic fm = match fm with Exists(x,p) -> let cjs = subtract (conjuncts p) [Atom(R("=",[Var x;Var x]))] in try let eqn = find (function (Atom(R("=",_))) -> true | _ -> false) cjs in let (Atom(R("=",[s;t]))) = eqn in let y = if s = Var x then t else s in list_conj(map (formsubst (x := y)) (subtract cjs [eqn])) with Failure _ -> if mem (Atom(R("<",[Var x;Var x]))) cjs then False else let l,r = partition (fun (Atom(R("<",[s;t]))) -> t = Var x) cjs in let lefts = map (fun (Atom(R("<",[l;_]))) -> l) l and rights = map (fun (Atom(R("<",[_;r]))) -> r) r in list_conj(allpairs (fun l r -> Atom(R("<",[l;r]))) lefts rights) | _ -> failwith "dlobasic";; (* ------------------------------------------------------------------------- *) (* Overall quelim procedure. *) (* ------------------------------------------------------------------------- *) let afn_dlo vars fm = match fm with Atom(R("<=",[s;t])) -> Not(Atom(R("<",[t;s]))) | Atom(R(">=",[s;t])) -> Not(Atom(R("<",[s;t]))) | Atom(R(">",[s;t])) -> Atom(R("<",[t;s])) | _ -> fm;; let quelim_dlo = lift_qelim afn_dlo (dnf ** cnnf lfn_dlo) (fun v -> dlobasic);; (* ------------------------------------------------------------------------- *) (* Examples. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; quelim_dlo <>;; quelim_dlo <>;; quelim_dlo <>;; quelim_dlo <<(forall x. x < a ==> x < b)>>;; quelim_dlo < x < b) <=> a = b>>;; time quelim_dlo <>;; time quelim_dlo < x < z>>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo < exists z. x < z /\ z < y>>;; time quelim_dlo < exists u. u < x /\ (y < u \/ x < y)>>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo < w < z>>;; time quelim_dlo <>;; time quelim_dlo <>;; time quelim_dlo < x < b) <=> a <= b>>;; time quelim_dlo < x < b>>;; time quelim_dlo < x <= b>>;; time quelim_dlo <>;; time quelim_dlo < y>>;; time quelim_dlo <>;; END_INTERACTIVE;;