(* ========================================================================= *) (* Nelson-Oppen combined decision procedure. *) (* *) (* Copyright (c) 2003, John Harrison. (See "LICENSE.txt" for details.) *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* Real language with decision procedure. *) (* ------------------------------------------------------------------------- *) let real_lang = let fn = ["-",1; "+",2; "-",2; "*",2; "^",2] and pr = ["<=",2; "<",2; ">=",2; ">",2] in (fun (s,n) -> n = 0 & is_numeral(Fn(s,[])) or mem (s,n) fn), (fun sn -> mem sn pr), (fun fm -> real_qelim(generalize fm) = True);; (* ------------------------------------------------------------------------- *) (* Integer language with decision procedure. *) (* ------------------------------------------------------------------------- *) let int_lang = let fn = ["-",1; "+",2; "-",2; "*",2] and pr = ["<=",2; "<",2; ">=",2; ">",2] in (fun (s,n) -> n = 0 & is_numeral(Fn(s,[])) or mem (s,n) fn), (fun sn -> mem sn pr), (fun fm -> integer_qelim(generalize fm) = True);; (* ------------------------------------------------------------------------- *) (* Add any uninterpreted symbols to a list of languages. *) (* ------------------------------------------------------------------------- *) let add_default langs = langs @ [(fun sn -> not (exists (fun (f,p,d) -> f sn) langs)), (fun sn -> not (exists (fun (f,p,d) -> p sn) langs)), ccvalid];; (* ------------------------------------------------------------------------- *) (* Choose a language for homogenization of an atom. *) (* ------------------------------------------------------------------------- *) let chooselang langs fm = match fm with Atom(R("=",[Fn(f,args);_])) | Atom(R("=",[_;Fn(f,args)])) -> find (fun (fn,pr,dp) -> fn(f,length args)) langs | Atom(R(p,args)) -> find (fun (fn,pr,dp) -> pr(p,length args)) langs;; (* ------------------------------------------------------------------------- *) (* Make a variable. *) (* ------------------------------------------------------------------------- *) let mkvar n = Var("v_"^(string_of_num n));; (* ------------------------------------------------------------------------- *) (* General listification for CPS-style function. *) (* ------------------------------------------------------------------------- *) let rec listify f l cont = match l with [] -> cont [] | h::t -> f h (fun h' -> listify f t (fun t' -> cont(h'::t')));; (* ------------------------------------------------------------------------- *) (* Homogenize a term. *) (* ------------------------------------------------------------------------- *) let rec homot (fn,pr,dp) tm cont n defs = match tm with Var x -> cont tm n defs | Fn(f,args) -> if fn(f,length args) then listify (homot (fn,pr,dp)) args (fun a -> cont (Fn(f,a))) n defs else cont (mkvar n) (n +/ Int 1) (Atom(R("=",[mkvar n;tm]))::defs);; (* ------------------------------------------------------------------------- *) (* Homogenize a literal. *) (* ------------------------------------------------------------------------- *) let rec homol langs fm cont n defs = match fm with Not(f) -> homol langs f (fun p -> cont(Not(p))) n defs | Atom(R(p,args)) -> let lang = chooselang langs fm in listify (homot lang) args (fun a -> cont (Atom(R(p,a)))) n defs | _ -> failwith "homol: not a literal";; (* ------------------------------------------------------------------------- *) (* Fully homogenize a list of literals. *) (* ------------------------------------------------------------------------- *) let rec homo langs fms cont = listify (homol langs) fms (fun dun n defs -> if defs = [] then cont dun n defs else homo langs defs (fun res -> cont (dun@res)) n []);; (* ------------------------------------------------------------------------- *) (* Overall homogenization. *) (* ------------------------------------------------------------------------- *) let homogenize langs fms = let fvs = unions(map fv fms) in let n = Int 1 +/ itlist (max_varindex "v_") fvs (Int 0) in homo langs fms (fun res n defs -> res) n [];; (* ------------------------------------------------------------------------- *) (* Whether a formula belongs to a language. *) (* ------------------------------------------------------------------------- *) let belongs (fn,pr,dp) fm = forall fn (functions fm) & forall pr (subtract (predicates fm) ["=",2]);; (* ------------------------------------------------------------------------- *) (* Partition formulas among a list of languages. *) (* ------------------------------------------------------------------------- *) let rec langpartition langs fms = match langs with [] -> if fms = [] then [] else failwith "langpartition" | l::ls -> let fms1,fms2 = partition (belongs l) fms in fms1::langpartition ls fms2;; (* ------------------------------------------------------------------------- *) (* Turn an arrangement (partition) of variables into corresponding formula. *) (* ------------------------------------------------------------------------- *) let rec arreq l = match l with v1::v2::rest -> mk_eq (Var v1) (Var v2) :: (arreq (v2::rest)) | _ -> [];; let arrangement part = itlist (union ** arreq) part (map (fun (v,w) -> Not(mk_eq (Var v) (Var w))) (distinctpairs (map hd part)));; (* ------------------------------------------------------------------------- *) (* Attempt to substitute with trivial equations. *) (* ------------------------------------------------------------------------- *) let dest_def fm = match fm with Atom(R("=",[Var x;t])) when not(mem x (fvt t)) -> x,t | Atom(R("=",[t; Var x])) when not(mem x (fvt t)) -> x,t | _ -> failwith "dest_def";; let rec redeqs eqs = try let eq = find (can dest_def) eqs in let x,t = dest_def eq in redeqs (map (formsubst (x := t)) (subtract eqs [eq])) with Failure _ -> eqs;; (* ------------------------------------------------------------------------- *) (* Naive Nelson-Oppen variant trying all arrangements. *) (* ------------------------------------------------------------------------- *) let trydps ldseps fms = exists (fun ((_,_,dp),fms0) -> dp(Not(list_conj(redeqs(fms0 @ fms))))) ldseps;; let nelop_refute vars ldseps = forall (trydps ldseps ** arrangement) (allpartitions vars);; let nelop1 langs fms0 = let fms = homogenize langs fms0 in let seps = langpartition langs fms in let fvlist = map (unions ** map fv) seps in let vars = filter (fun x -> length (filter (mem x) fvlist) >= 2) (unions fvlist) in nelop_refute vars (zip langs seps);; let nelop langs fm = forall (nelop1 langs) (simpdnf(simplify(Not fm)));; (* ------------------------------------------------------------------------- *) (* Check that our example works. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; nelop (add_default [int_lang]) < false>>;; (* ------------------------------------------------------------------------- *) (* Take note of our case explosion. *) (* ------------------------------------------------------------------------- *) let bell n = length(allpartitions (1--n));; map bell (1--10);; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Find the smallest subset satisfying a predicate. *) (* ------------------------------------------------------------------------- *) let rec findasubset p m l = if m = 0 then p [] else match l with [] -> failwith "findasubset" | h::t -> try findasubset (fun s -> p(h::s)) (m - 1) t with Failure _ -> findasubset p m t;; let findsubset p l = tryfind (fun n -> findasubset (fun x -> if p x then x else failwith "") n l) (0--length l);; (* ------------------------------------------------------------------------- *) (* The "true" Nelson-Oppen method. *) (* ------------------------------------------------------------------------- *) let rec nelop_refute eqs ldseps = try let dj = findsubset (trydps ldseps ** map negate) eqs in forall (fun eq -> nelop_refute (subtract eqs [eq]) (map (fun (dps,es) -> (dps,eq::es)) ldseps)) dj with Failure _ -> false;; let nelop1 langs fms0 = let fms = homogenize langs fms0 in let seps = langpartition langs fms in let fvlist = map (unions ** map fv) seps in let vars = filter (fun x -> length (filter (mem x) fvlist) >= 2) (unions fvlist) in let eqs = map (fun (a,b) -> mk_eq (Var a) (Var b)) (distinctpairs vars) in nelop_refute eqs (zip langs seps);; let nelop langs fm = forall (nelop1 langs) (simpdnf(simplify(Not fm)));; (* ------------------------------------------------------------------------- *) (* Some additional examples (from ICS paper and Shostak's "A practical..." *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; nelop (add_default [int_lang]) <= x + z /\ z >= 0 ==> f(f(x) - f(y)) = f(z)>>;; nelop (add_default [int_lang]) <= z /\ z >= x ==> f(z) = f(x)>>;; nelop (add_default [int_lang]) < a + b <= 1 \/ b + f(b) <= 1 \/ f(f(b)) <= f(a)>>;; (* ------------------------------------------------------------------------- *) (* Confirmation of non-convexity. *) (* ------------------------------------------------------------------------- *) map (real_qelim ** generalize) [< x = z \/ y = z>>; < x = z>>; < y = z>>];; map (integer_qelim ** generalize) [<<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = y \/ x = z>>; <<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = y>>; <<0 <= x /\ x < 2 /\ y = 0 /\ z = 1 ==> x = z>>];; (* ------------------------------------------------------------------------- *) (* Failures of original Shostak procedure. *) (* ------------------------------------------------------------------------- *) nelop (add_default [int_lang]) < false>>;; nelop (add_default [int_lang]) < false>>;; (* ------------------------------------------------------------------------- *) (* Additional examples. *) (* ------------------------------------------------------------------------- *) time (nelop (add_default [int_lang])) < false>>;; time (nelop (add_default [int_lang])) <<(x = y /\ z = 1 ==> f(f((x+z))) = f(f((1+y))))>>;; time (nelop (add_default [int_lang])) < f(x) = f(y)>>;; time (nelop (add_default [int_lang])) <<~(f(f(x) - f(y)) = f(z)) /\ y <= x /\ y >= x + z /\ z >= 0 ==> false>>;; time (nelop (add_default [int_lang])) < (P(x,y) <=> P(f(y),y))>>;; time (nelop (add_default [int_lang])) <<(x >= y ==> MAX(x,y) = x) /\ (y >= x ==> MAX(x,y) = y) ==> x = y + 2 ==> MAX(x,y) = x>>;; time (nelop (add_default [int_lang])) <= g(x) ==> x = g(g(g(g(x))))>>;; time (nelop (add_default [real_lang])) < (f(x) = f(-(x))) ==> (f(x) = f(1))>>;; time (nelop (add_default [int_lang])) <<2 * f(x + y) = 3 * y /\ 2 * x = y ==> f(f(x + y)) = 3 * x>>;; END_INTERACTIVE;;