why3doc index index
module Types use Firstorder_formula_impl.Types use Firstorder_formula_list_impl.Types use Firstorder_term_impl.Types use list.List use Functions.Func use Firstorder_semantics.Sem (* ghost field: explicitly to get rid of the existential. *) type skolemization_return 'st = { skolemized : nlimpl_fo_formula ; skolem_bound : int ; free_var_list : list int ; ghost model_transformer : (model int 'st) -> (model int 'st) ; } type skolemization_list_return 'st = { skolemized_l : nlimpl_fo_formula_list ; skolem_bound_l : int ; ghost model_transformer_l : (model int 'st) -> (model int 'st) ; } type skolemization_env_return 'st = { skolemized_fv_list : nlimpl_fo_term_list ; ghost skolem_env : (list 'st) -> (int -> 'st) ; } end module Logic use Firstorder_formula_spec.Spec use Firstorder_term_spec.Spec use Firstorder_symbol_spec.Spec use Firstorder_formula_list_spec.Spec use Functions.Func use option.Option use OptionFuncs.Funcs predicate is_atom (phi:fo_formula 'ls 'b) = match phi with | PApp _ _ -> true | Not (PApp _ _) -> true | _ -> false end (* Negational normal form. *) predicate is_nnf (phi:fo_formula 'ls 'b) = match phi with | Not (PApp _ _) -> true | Not _ -> false | PApp _ _ -> true | And a b -> is_nnf a /\ is_nnf b | Or a b -> is_nnf a /\ is_nnf b | Forall a -> is_nnf a | Exists a -> is_nnf a | FTrue -> true | FFalse -> true end predicate is_nnf_list (phis:fo_formula_list 'ls 'b) = match phis with | FOFNil -> true | FOFCons x q -> is_nnf x /\ is_nnf_list q end let rec lemma is_nnf_subst (phi:fo_formula 'ls 'b) (f:'b -> (fo_term 'ls 'c)) : unit requires { is_nnf phi } ensures { is_nnf (subst_fo_formula phi subst_id_symbol f) } variant { size_fo_formula phi } = match phi with | Not (PApp p l) -> assert { subst_fo_formula phi subst_id_symbol f = Not (subst_fo_formula (PApp p l) subst_id_symbol f) = Not (PApp (subst_symbol p subst_id_symbol) (subst_fo_term_list l subst_id_symbol f)) } | Not _ -> absurd | PApp _ _ -> () | And a b -> is_nnf_subst a f ; is_nnf_subst b f | Or a b -> is_nnf_subst a f ; is_nnf_subst b f | Forall a -> is_nnf_subst a (olifts_fo_term f) ; assert { subst_fo_formula phi subst_id_symbol f = Forall (subst_fo_formula a subst_id_symbol (olifts_fo_term f)) } | Exists a -> is_nnf_subst a (olifts_fo_term f) ; assert { subst_fo_formula phi subst_id_symbol f = Exists (subst_fo_formula a subst_id_symbol (olifts_fo_term f)) } | FTrue -> () | FFalse -> () end let lemma is_nnf_renaming (phi:fo_formula 'ls 'b) (f:'b -> 'c) : unit requires { is_nnf phi } ensures { is_nnf (rename_fo_formula phi identity f) } = is_nnf_subst phi (rcompose f subst_id_fo_term) (* Simplified formula. *) predicate is_simpl (phi:fo_formula 'ls 'b) = match phi with | Not u -> is_simpl u | PApp _ _ -> true | And a b -> is_simpl a /\ is_simpl b | Or a b -> is_simpl a /\ is_simpl b | Forall a -> is_simpl a | Exists a -> is_simpl a | FTrue -> false | FFalse -> false end predicate is_simpl_list (phis:fo_formula_list 'ls 'b) = match phis with | FOFNil -> true | FOFCons x q -> is_simpl x /\ is_simpl_list q end let rec lemma is_simpl_subst (phi:fo_formula 'ls 'b) (f:'b -> (fo_term 'ls 'c)) : unit requires { is_simpl phi } ensures { is_simpl (subst_fo_formula phi subst_id_symbol f) } variant { size_fo_formula phi } = match phi with | Not u -> is_simpl_subst u f ; assert { subst_fo_formula phi subst_id_symbol f = Not (subst_fo_formula u subst_id_symbol f) } | PApp _ _ -> () | And a b -> is_simpl_subst a f ; is_simpl_subst b f | Or a b -> is_simpl_subst a f ; is_simpl_subst b f | Forall a -> is_simpl_subst a (olifts_fo_term f) ; assert { subst_fo_formula phi subst_id_symbol f = Forall (subst_fo_formula a subst_id_symbol (olifts_fo_term f)) } | Exists a -> is_simpl_subst a (olifts_fo_term f) ; assert { subst_fo_formula phi subst_id_symbol f = Exists (subst_fo_formula a subst_id_symbol (olifts_fo_term f)) } | FTrue -> absurd | FFalse -> absurd end let lemma is_simpl_renaming (phi:fo_formula 'ls 'b) (f:'b -> 'c) : unit requires { is_simpl phi } ensures { is_simpl (rename_fo_formula phi identity f) } = is_simpl_subst phi (rcompose f subst_id_fo_term) (* Simplified formula, + true/false allowed at top. *) predicate is_simpl_extended (phi:fo_formula 'ls 'b) = is_simpl phi \/ phi = FTrue \/ phi = FFalse lemma is_simpl_extended_renaming : forall phi:fo_formula 'ls 'b,f:'b -> 'c. is_simpl_extended phi -> is_simpl_extended (rename_fo_formula phi identity f) predicate no_existential (phi:fo_formula 'ls 'b) = match phi with | Not u -> no_existential u | PApp _ _ -> true | And a b -> no_existential a /\ no_existential b | Or a b -> no_existential a /\ no_existential b | Forall a -> no_existential a | Exists _ -> false | FTrue -> true | FFalse -> true end predicate no_existential_list (phis:fo_formula_list 'ls 'b) = match phis with | FOFNil -> true | FOFCons x q -> no_existential x /\ no_existential_list q end let rec lemma no_existential_subst (phi:fo_formula 'ls 'b) (f:'b -> (fo_term 'ls 'c)) : unit requires { no_existential phi } ensures { no_existential (subst_fo_formula phi subst_id_symbol f) } variant { size_fo_formula phi } = match phi with | Not u -> no_existential_subst u f ; assert { subst_fo_formula phi subst_id_symbol f = Not (subst_fo_formula u subst_id_symbol f) } | PApp _ _ -> () | And a b -> no_existential_subst a f ; no_existential_subst b f | Or a b -> no_existential_subst a f ; no_existential_subst b f | Forall a -> no_existential_subst a (olifts_fo_term f) ; assert { subst_fo_formula phi subst_id_symbol f = Forall (subst_fo_formula a subst_id_symbol (olifts_fo_term f)) } | Exists _ -> absurd | FTrue -> () | FFalse -> () end let lemma no_existential_renaming (phi:fo_formula 'ls 'b) (f:'b -> 'c) : unit requires { no_existential phi } ensures { no_existential (rename_fo_formula phi identity f) } = no_existential_subst phi (rcompose f subst_id_fo_term) (* Skolemization environment. *) use Choice.Choice use list.List (* Hack to force possibility of instantiation of extend_env definition axiom ! *) function extend_env_selection (g:(list 'st) -> ('b -> 'st)) (x:'b) (y:'b) (z:'st) (q:list 'st) : 'st = if x = y then z else g q x (* Abstraction-definition axiom : function extend_env (g:(list 'st) -> ('b -> 'st) (y:'b) : (list 'st) -> ('b -> 'st) = (\ l:list 'st. (\ x:option 'b. match l with | Cons z q -> extend_env_selection g x y z q | Nil -> default ) ) *) function extend_env (g:(list 'st) -> ('b -> 'st)) (y:'b) : (list 'st) -> ('b -> 'st) axiom extend_env_def : forall g:(list 'st) -> ('b -> 'st),y:'b, l:list 'st,x:'b. extend_env g y l x = match l with | Cons z q -> extend_env_selection g x y z q | Nil -> default end end module Impl use Types use Logic use Functions.Func use import set.Set as S use Firstorder_formula_spec.Spec use Firstorder_formula_impl.Types use Firstorder_formula_impl.Logic use Firstorder_formula_impl.Impl use Firstorder_formula_list_spec.Spec use Firstorder_formula_list_impl.Impl use Firstorder_formula_list_impl.Logic use Firstorder_formula_list_impl.Types use Firstorder_term_spec.Spec use Firstorder_term_impl.Impl use Firstorder_term_impl.Logic use Firstorder_term_impl.Types use Firstorder_symbol_spec.Spec use Firstorder_symbol_impl.Impl use Firstorder_symbol_impl.Logic use Firstorder_symbol_impl.Types use list.List use option.Option use OptionFuncs.Funcs use Firstorder_semantics.Sem use bool.Bool use list.Mem use int.Int exception Unsat let smart_and (phi1 phi2:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi1 } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi1.model_fo_formula_field -> S.mem x fvp } requires { nlimpl_fo_formula_ok phi2 } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi2.model_fo_formula_field -> S.mem x fvp } requires { is_simpl_extended phi1.model_fo_formula_field } requires { is_simpl_extended phi2.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic result.model_fo_formula_field m rho <-> formula_semantic phi1.model_fo_formula_field m rho /\ formula_semantic phi2.model_fo_formula_field m rho } ensures { is_nnf phi1.model_fo_formula_field /\ is_nnf phi2.model_fo_formula_field -> is_nnf result.model_fo_formula_field } ensures { nlimpl_fo_formula_ok result } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.model_fo_formula_field -> S.mem x fvp } = let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in match destruct_fo_formula phi1 with | NLC_FFalse -> phi1 | NLC_FTrue -> phi2 | _ -> assert { phi1m <> FTrue } ; assert { phi1m <> FFalse } ; match destruct_fo_formula phi2 with | NLC_FFalse -> phi2 | NLC_FTrue -> phi1 | _ -> assert { phi2m <> FTrue } ; assert { phi2m <> FFalse } ; assert { is_simpl phi1m /\ is_simpl phi2m } ; let phi0 = construct_fo_formula (NLC_And phi1 phi2) in assert { phi0.model_fo_formula_field = And phi1m phi2m } ; phi0 end end let smart_or (phi1 phi2:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi1 } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi1.model_fo_formula_field -> S.mem x fvp } requires { nlimpl_fo_formula_ok phi2 } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi2.model_fo_formula_field -> S.mem x fvp } requires { is_simpl_extended phi1.model_fo_formula_field } requires { is_simpl_extended phi2.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic result.model_fo_formula_field m rho <-> formula_semantic phi1.model_fo_formula_field m rho \/ formula_semantic phi2.model_fo_formula_field m rho } ensures { is_nnf phi1.model_fo_formula_field /\ is_nnf phi2.model_fo_formula_field -> is_nnf result.model_fo_formula_field } ensures { nlimpl_fo_formula_ok result } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.model_fo_formula_field -> S.mem x fvp } = let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in match destruct_fo_formula phi1 with | NLC_FTrue -> phi1 | NLC_FFalse -> phi2 | _ -> assert { phi1m <> FTrue } ; assert { phi1m <> FFalse } ; match destruct_fo_formula phi2 with | NLC_FTrue -> phi2 | NLC_FFalse -> phi1 | _ -> assert { phi2m <> FTrue } ; assert { phi2m <> FFalse } ; assert { is_simpl phi1m /\ is_simpl phi2m } ; let phi0 = construct_fo_formula (NLC_Or phi1 phi2) in assert { phi0.model_fo_formula_field = Or phi1m phi2m } ; phi0 end end let smart_forall (x:int) (phi:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi } requires { forall y:int. is_fo_term_free_var_in_fo_formula y phi.model_fo_formula_field -> S.mem y fvp \/ y = x } requires { is_simpl_extended phi.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic result.model_fo_formula_field m rho <-> (forall xm:'st. let r = rcompose (some[x <- None]) (ocase rho xm) in formula_semantic phi.model_fo_formula_field m r) } ensures { is_nnf phi.model_fo_formula_field -> is_nnf result.model_fo_formula_field } ensures { nlimpl_fo_formula_ok result } ensures { forall y:int. is_fo_term_free_var_in_fo_formula y result.model_fo_formula_field -> S.mem y fvp } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_FFalse -> assert { phim = FFalse && forall m:model int 'st,rho:int -> 'st. not(formula_semantic phim m rho) } ; phi | NLC_FTrue -> phi | _ -> assert { phim <> FTrue /\ phim <> FFalse && is_simpl phim } ; let phi0 = construct_fo_formula (NLC_Forall x phi) in let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phim identity (some[x <- None]) in assert { phi0m = Forall phi1m } ; assert { forall xf:int. (forall y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x<-None]) y = Some xf -> y <> x && Some xf = Some y && xf = y) && is_fo_term_free_var_in_fo_formula xf phi0m -> is_fo_term_free_var_in_fo_formula (Some xf) phi1m && (exists y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x <- None]) y = Some xf) && is_fo_term_free_var_in_fo_formula xf phim && xf <> x && S.mem xf fvp } ; phi0 end let smart_exists (x:int) (phi:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi } requires { forall y:int. is_fo_term_free_var_in_fo_formula y phi.model_fo_formula_field -> S.mem y fvp \/ y = x } requires { is_simpl_extended phi.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic result.model_fo_formula_field m rho <-> (exists xm:'st. let r = rcompose (some[x <- None]) (ocase rho xm) in formula_semantic phi.model_fo_formula_field m r) } ensures { is_nnf phi.model_fo_formula_field -> is_nnf result.model_fo_formula_field } ensures { nlimpl_fo_formula_ok result } ensures { forall y:int. is_fo_term_free_var_in_fo_formula y result.model_fo_formula_field -> S.mem y fvp } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_FFalse -> phi | NLC_FTrue -> assert { phim = FTrue /\ forall m:model int 'st,rho:int -> 'st. formula_semantic phim m rho } ; phi | _ -> assert { phim <> FTrue /\ phim <> FFalse && is_simpl phim } ; let phi0 = construct_fo_formula (NLC_Exists x phi) in let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phim identity (some[x <- None]) in assert { phi0m = Exists phi1m } ; assert { forall xf:int. (forall y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x<-None]) y = Some xf -> y <> x && Some xf = Some y && xf = y) && (is_fo_term_free_var_in_fo_formula xf phi0m -> is_fo_term_free_var_in_fo_formula (Some xf) phi1m && (exists y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x <- None]) y = Some xf) && is_fo_term_free_var_in_fo_formula xf phim && xf <> x && S.mem xf fvp) && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp) } ; phi0 end (* Put in negational normal form and simplify formula (e.g. true/false removal/propagation to toplevel) *) let rec nnf_simpl (phi:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field -> S.mem x fvp } ensures { nlimpl_fo_formula_ok result } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.model_fo_formula_field -> S.mem x fvp } ensures { forall m:model int 'st, rho:int -> 'st. formula_semantic phi.model_fo_formula_field m rho <-> formula_semantic result.model_fo_formula_field m rho } ensures { is_nnf result.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } variant { size_fo_formula phi.model_fo_formula_field } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_PApp p l -> phi | NLC_Not phi' -> assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi'.model_fo_formula_field -> is_fo_term_free_var_in_fo_formula x phim && S.mem x fvp } ; nnf_neg_simpl phi' fvp st | NLC_And phi1 phi2 -> let phi'1 = nnf_simpl phi1 fvp st in let phi'2 = nnf_simpl phi2 fvp st in smart_and phi'1 phi'2 fvp st | NLC_Or phi1 phi2 -> let phi'1 = nnf_simpl phi1 fvp st in let phi'2 = nnf_simpl phi2 fvp st in smart_or phi'1 phi'2 fvp st | NLC_FTrue -> phi | NLC_FFalse -> phi | NLC_Forall x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phi0m identity (some[x<-None]) in assert { phim = Forall phi1m } ; assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) }; let ghost fvp' = S.add x fvp in assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let phi' = nnf_simpl phi0 fvp' st in let phi'' = smart_forall x phi' fvp st in phi'' | NLC_Exists x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phi0m identity (some[x<-None]) in assert { phim = Exists phi1m } ; assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) }; let ghost fvp' = S.add x fvp in assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let phi' = nnf_simpl phi0 fvp' st in let phi'' = smart_exists x phi' fvp st in phi'' end with nnf_neg_simpl (phi:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field -> S.mem x fvp } ensures { nlimpl_fo_formula_ok result } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.model_fo_formula_field -> S.mem x fvp } ensures { forall m:model int 'st, rho:int -> 'st. formula_semantic phi.model_fo_formula_field m rho <-> not(formula_semantic result.model_fo_formula_field m rho) } ensures { is_nnf result.model_fo_formula_field } ensures { is_simpl_extended result.model_fo_formula_field } variant { size_fo_formula phi.model_fo_formula_field } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_PApp p l -> construct_fo_formula (NLC_Not phi) | NLC_Not phi' -> nnf_simpl phi' fvp st | NLC_And phi1 phi2 -> let phi'1 = nnf_neg_simpl phi1 fvp st in let phi'2 = nnf_neg_simpl phi2 fvp st in smart_or phi'1 phi'2 fvp st | NLC_Or phi1 phi2 -> let phi'1 = nnf_neg_simpl phi1 fvp st in let phi'2 = nnf_neg_simpl phi2 fvp st in smart_and phi'1 phi'2 fvp st | NLC_FTrue -> construct_fo_formula NLC_FFalse | NLC_FFalse -> construct_fo_formula NLC_FTrue | NLC_Forall x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phi0m identity (some[x<-None]) in assert { phim = Forall phi1m } ; assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) }; let ghost fvp' = S.add x fvp in assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let phi' = nnf_neg_simpl phi0 fvp' st in let phi'' = smart_exists x phi' fvp st in phi'' | NLC_Exists x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost phi1m = rename_fo_formula phi0m identity (some[x<-None]) in assert { phim = Exists phi1m } ; assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) }; let ghost fvp' = S.add x fvp in assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let phi' = nnf_neg_simpl phi0 fvp' st in let phi'' = smart_forall x phi' fvp st in phi'' end (* gnum : take care of eliminated starting points. *) let rec nnf_simpl_list (phis:nlimpl_fo_formula_list) (gnum:int) (ghost fvp:set int) (ghost st:'st) : (nlimpl_fo_formula_list,int) requires { nlimpl_fo_formula_list_ok phis } requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x phis.model_fo_formula_list_field -> S.mem x fvp } returns { (rs,_) -> nlimpl_fo_formula_list_ok rs } returns { (rs,_) -> forall x:int. is_fo_term_free_var_in_fo_formula_list x rs.model_fo_formula_list_field -> S.mem x fvp } returns { (rs,_) -> forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic phis.model_fo_formula_list_field m rho <-> formula_list_conj_semantic rs.model_fo_formula_list_field m rho } returns { (rs,_) -> is_nnf_list rs.model_fo_formula_list_field } returns { (rs,_) -> is_simpl_list rs.model_fo_formula_list_field } raises { Unsat -> forall m:model int 'st,rho:int -> 'st. not(formula_list_conj_semantic phis.model_fo_formula_list_field m rho) } variant { size_fo_formula_list phis.model_fo_formula_list_field } = let phism = phis.model_fo_formula_list_field in match destruct_fo_formula_list phis with | NLC_FOFNil -> (phis,gnum) | NLC_FOFCons phi q -> let phim = phi.model_fo_formula_field in let qm = q.model_fo_formula_list_field in assert { phism = FOFCons phim qm } ; let (q',gnum') = nnf_simpl_list q (gnum-1) fvp st in let phi' = nnf_simpl phi fvp st in let phi'_m = phi'.model_fo_formula_field in let q'_m = q'.model_fo_formula_list_field in match destruct_fo_formula phi' with | NLC_FTrue -> (q',if gnum > 0 then gnum' else gnum'+1) | NLC_FFalse -> raise Unsat | _ -> assert { is_simpl phi'.model_fo_formula_field } ; let res = construct_fo_formula_list (NLC_FOFCons phi' q') in let resm = res.model_fo_formula_list_field in assert { resm = FOFCons phi'_m q'_m } ; (res,gnum'+1) end end use ISet.Logic use ISet.Impl use Choice.Choice let rec term_free_vars (t:nlimpl_fo_term) (ghost fvp:set int) : list int requires { nlimpl_fo_term_ok t } requires { forall x:int. is_fo_term_free_var_in_fo_term x t.model_fo_term_field -> S.mem x fvp } ensures { forall x:int. is_fo_term_free_var_in_fo_term x t.model_fo_term_field -> mem x result } ensures { forall x:int. mem x result -> S.mem x fvp } ensures { iset_ok result } variant { size_fo_term t.model_fo_term_field } = match destruct_fo_term t with | NLCVar_fo_term x -> Cons x Nil | NLC_App _ l -> term_list_free_vars l fvp end with term_list_free_vars (l:nlimpl_fo_term_list) (ghost fvp:set int): list int requires { nlimpl_fo_term_list_ok l } requires { forall x:int. is_fo_term_free_var_in_fo_term_list x l.model_fo_term_list_field -> S.mem x fvp } ensures { forall x:int. is_fo_term_free_var_in_fo_term_list x l.model_fo_term_list_field -> mem x result } ensures { forall x:int. mem x result -> S.mem x fvp } ensures { iset_ok result } variant { size_fo_term_list l.model_fo_term_list_field } = match destruct_fo_term_list l with | NLC_FONil -> Nil | NLC_FOCons t q -> merge (term_free_vars t fvp) (term_list_free_vars q fvp) end let rec skolem_parameters (l:list int) (acc:skolemization_env_return 'st) (ghost fvp:set int) : skolemization_env_return 'st requires { iset_ok l } requires { forall x:int. mem x l -> S.mem x fvp } requires { nlimpl_fo_term_list_ok acc.skolemized_fv_list } requires { forall x:int. is_fo_term_free_var_in_fo_term_list x acc.skolemized_fv_list.model_fo_term_list_field -> S.mem x fvp } requires { forall x:int. not(mem x l /\ is_fo_term_free_var_in_fo_term_list x acc.skolemized_fv_list.model_fo_term_list_field) } requires { forall x:int,m:model int 'st,rho:int -> 'st. is_fo_term_free_var_in_fo_term_list x acc.skolemized_fv_list.model_fo_term_list_field -> eval acc.skolem_env (term_list_semantic acc.skolemized_fv_list.model_fo_term_list_field m rho) x = rho x } requires { forall f:int. not(is_symbol_free_var_in_fo_term_list f acc.skolemized_fv_list.model_fo_term_list_field) } ensures { nlimpl_fo_term_list_ok result.skolemized_fv_list } ensures { forall x:int. is_fo_term_free_var_in_fo_term_list x result.skolemized_fv_list.model_fo_term_list_field -> S.mem x fvp } ensures { forall x:int,m:model int 'st,rho:int -> 'st. mem x l \/ is_fo_term_free_var_in_fo_term_list x acc.skolemized_fv_list.model_fo_term_list_field -> eval result.skolem_env (term_list_semantic result.skolemized_fv_list.model_fo_term_list_field m rho) x = rho x } ensures { forall x:int. is_fo_term_free_var_in_fo_term_list x result.skolemized_fv_list.model_fo_term_list_field -> mem x l \/ is_fo_term_free_var_in_fo_term_list x acc.skolemized_fv_list.model_fo_term_list_field } ensures { forall f:int. not(is_symbol_free_var_in_fo_term_list f result.skolemized_fv_list.model_fo_term_list_field) } variant { l } = match l with | Nil -> acc | Cons x q -> let accl = acc.skolemized_fv_list in let skenv = acc.skolem_env in let varx = construct_fo_term (NLCVar_fo_term x) in let accl' = construct_fo_term_list (NLC_FOCons varx accl) in let (acclm,accl'_m) = (accl.model_fo_term_list_field ,accl'.model_fo_term_list_field) in assert { accl'_m = FOCons (Var_fo_term x) acclm } ; let ghost skenv' = extend_env skenv x in let acc' = { skolemized_fv_list = accl' ; skolem_env = skenv' } in skolem_parameters q acc' fvp end (* Not sufficient yet. *) let rec skolemize (phi:nlimpl_fo_formula) (skb:int) (b:bool) (ghost fvp:set int) : skolemization_return 'st requires { nlimpl_fo_formula_ok phi } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field -> S.mem x fvp } requires { is_simpl phi.model_fo_formula_field } requires { is_nnf phi.model_fo_formula_field } requires { forall ls:int. is_symbol_free_var_in_fo_formula ls phi.model_fo_formula_field -> ls < skb } ensures { nlimpl_fo_formula_ok result.skolemized } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.skolemized.model_fo_formula_field -> S.mem x fvp } ensures { result.skolem_bound >= skb } ensures { forall ls:int. is_symbol_free_var_in_fo_formula ls result.skolemized.model_fo_formula_field -> ls < result.skolem_bound } ensures { is_nnf result.skolemized.model_fo_formula_field } ensures { is_simpl result.skolemized.model_fo_formula_field } ensures { no_existential result.skolemized.model_fo_formula_field } ensures { forall m:model int 'st, rho:int -> 'st. formula_semantic phi.model_fo_formula_field m rho -> formula_semantic result.skolemized.model_fo_formula_field (eval result.model_transformer m) rho } (* Completeness concern. ensures { forall m:model int 'st, rho:int -> 'st. formula_semantic result.skolemized.model_fo_formula_field m rho -> formula_semantic phi.model_fo_formula_field m rho *) ensures { forall m:model int 'st, ls:int. ls < skb -> eval m.interp_fun ls = eval (eval result.model_transformer m).interp_fun ls } ensures { forall m:model int 'st. m.interp_pred = (eval result.model_transformer m).interp_pred } ensures { forall x:int. b = True -> is_fo_term_free_var_in_fo_formula x result.skolemized.model_fo_formula_field -> mem x result.free_var_list } ensures { iset_ok result.free_var_list } ensures { forall x:int. b = True -> mem x result.free_var_list -> S.mem x fvp } variant { size_fo_formula phi.model_fo_formula_field } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_PApp _ l -> { skolemized = phi ; skolem_bound = skb ; model_transformer = identity ; free_var_list = if b then term_list_free_vars l fvp else Nil } | NLC_Not phi' -> let phi'_m = phi'.model_fo_formula_field in assert { phim = Not phi'_m } ; assert { match phi'_m with | PApp _ _ -> true | _ -> false end } ; { skolemized = phi ; skolem_bound = skb ; model_transformer = identity ; free_var_list = if b then match destruct_fo_formula phi' with | NLC_PApp _ l -> term_list_free_vars l fvp | _ -> absurd end else Nil } | NLC_And phi1 phi2 -> let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in assert { phim = And phi1m phi2m } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phi1m -> is_symbol_free_var_in_fo_formula ls phim } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phi2m -> is_symbol_free_var_in_fo_formula ls phim } ; let res1 = skolemize phi1 skb b fvp in let res2 = skolemize phi2 res1.skolem_bound b fvp in let res1m = res1.skolemized.model_fo_formula_field in let res2m = res2.skolemized.model_fo_formula_field in let skr = construct_fo_formula (NLC_And res1.skolemized res2.skolemized) in let skrm = skr.model_fo_formula_field in let (res1f,res2f) = (res1.model_transformer,res2.model_transformer) in let ghost transf = rcompose res1f res2f in let fvlist = merge res1.free_var_list res2.free_var_list in assert { skrm = And res1m res2m } ; assert { forall m:model int 'st. m.interp_pred = (res1f m).interp_pred = (transf m).interp_pred } ; assert { forall m:model int 'st, ls:int. ls < skb -> eval m.interp_fun ls = eval (res1f m).interp_fun ls = eval (transf m).interp_fun ls } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic res1m m rho <-> formula_semantic res1m (res2f m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic phi2m m rho <-> formula_semantic phi2m (res1f m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. transf m = res2f (res1f m) && (formula_semantic phi1m m rho -> formula_semantic res1m (res1f m) rho && formula_semantic res1m (transf m) rho) /\ (formula_semantic phi2m m rho -> formula_semantic phi2m (res1f m) rho && formula_semantic res2m (transf m) rho) } ; assert { forall x:int. is_fo_term_free_var_in_fo_formula x skrm -> (is_fo_term_free_var_in_fo_formula x res1m \/ is_fo_term_free_var_in_fo_formula x res2m) && S.mem x fvp } ; { skolemized = skr ; skolem_bound = res2.skolem_bound ; model_transformer = transf ; free_var_list = fvlist } | NLC_Or phi1 phi2 -> let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in assert { phim = Or phi1m phi2m } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phi1m -> is_symbol_free_var_in_fo_formula ls phim } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phi2m -> is_symbol_free_var_in_fo_formula ls phim } ; let res1 = skolemize phi1 skb b fvp in let res2 = skolemize phi2 res1.skolem_bound b fvp in let res1m = res1.skolemized.model_fo_formula_field in let res2m = res2.skolemized.model_fo_formula_field in let skr = construct_fo_formula (NLC_Or res1.skolemized res2.skolemized) in let skrm = skr.model_fo_formula_field in let (res1f,res2f) = (res1.model_transformer,res2.model_transformer) in let ghost transf = rcompose res1f res2f in let fvlist = merge res1.free_var_list res2.free_var_list in assert { skrm = Or res1m res2m } ; assert { forall m:model int 'st. m.interp_pred = (res1f m).interp_pred = (transf m).interp_pred } ; assert { forall m:model int 'st, ls:int. ls < skb -> eval m.interp_fun ls = eval (res1f m).interp_fun ls = eval (transf m).interp_fun ls } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic res1m m rho <-> formula_semantic res1m (res2f m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic phi2m m rho <-> formula_semantic phi2m (res1f m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. transf m = res2f (res1f m) && (formula_semantic phi1m m rho -> formula_semantic res1m (res1f m) rho && formula_semantic res1m (transf m) rho) /\ (formula_semantic phi2m m rho -> formula_semantic phi2m (res1f m) rho && formula_semantic res2m (transf m) rho) } ; assert { forall x:int. is_fo_term_free_var_in_fo_formula x skrm -> (is_fo_term_free_var_in_fo_formula x res1m \/ is_fo_term_free_var_in_fo_formula x res2m) && S.mem x fvp } ; { skolemized = skr ; skolem_bound = res2.skolem_bound ; model_transformer = transf ; free_var_list = fvlist } | NLC_FTrue -> absurd | NLC_FFalse -> absurd | NLC_Forall x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost r0 = some[x <- None] in let ghost phi1m = rename_fo_formula phi0m identity r0 in assert { phim = Forall phi1m } ; assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) } ; assert { forall ls:int. (is_symbol_free_var_in_fo_formula ls phi1m <-> is_symbol_free_var_in_fo_formula ls phi0m) && (is_symbol_free_var_in_fo_formula ls phim <-> is_symbol_free_var_in_fo_formula ls phi0m) } ; let ghost fvp' = S.add x fvp in assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let res = skolemize phi0 skb b fvp' in let resm = res.skolemized.model_fo_formula_field in let ghost res1m = rename_fo_formula resm identity r0 in let skr = construct_fo_formula (NLC_Forall x res.skolemized) in let skrm = skr.model_fo_formula_field in let fvl = remove x res.free_var_list in let transf = res.model_transformer in assert { skrm = Forall res1m } ; assert { forall ls:int. (is_symbol_free_var_in_fo_formula ls res1m <-> (exists ls':int. is_symbol_free_var_in_fo_formula ls' resm /\ identity ls' = ls)) && (is_symbol_free_var_in_fo_formula ls res1m <-> is_symbol_free_var_in_fo_formula ls resm) } ; assert { forall m:model int 'st, rho:int -> 'st, xm:'st. formula_semantic phi1m m (ocase rho xm) -> formula_semantic phi0m m (rcompose r0 (ocase rho xm)) && formula_semantic resm (transf m) (rcompose r0 (ocase rho xm)) && formula_semantic res1m (transf m) (ocase rho xm) } ; assert { forall y:int. is_fo_term_free_var_in_fo_formula (Some y) res1m -> (forall z:int. is_fo_term_free_var_in_fo_formula z resm /\ r0 z = Some y -> z <> x && z = y ) && (is_fo_term_free_var_in_fo_formula y resm /\ y <> x) && ((b = True -> mem y fvl) /\ (S.mem y fvp' && S.mem y fvp)) } ; { skolemized = skr ; skolem_bound = res.skolem_bound ; model_transformer = transf ; free_var_list = fvl } | NLC_Exists x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost r0 = some[x <- None] in let ghost phi1m = rename_fo_formula phi0m identity r0 in assert { phim = Exists phi1m } ; assert { forall ls:int. (is_symbol_free_var_in_fo_formula ls phi1m <-> is_symbol_free_var_in_fo_formula ls phi0m) && (is_symbol_free_var_in_fo_formula ls phim <-> is_symbol_free_var_in_fo_formula ls phi0m) } ; let ghost fvp' = S.add x fvp in assert { phi0m = rename_fo_formula phi1m identity (ocase identity x) } ; assert { forall xf:int. (forall y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf -> match y with None -> x = xf && S.mem xf fvp' | Some y -> y = xf && is_fo_term_free_var_in_fo_formula y phim && S.mem xf fvp && S.mem xf fvp' end && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> (exists y:option int. is_fo_term_free_var_in_fo_formula y phi1m /\ ocase identity x y = xf) && S.mem xf fvp') && (is_fo_term_free_var_in_fo_formula xf phi0m -> S.mem xf fvp') }; let res = skolemize phi0 skb True fvp' in let resm = res.skolemized.model_fo_formula_field in let ghost res1m = rename_fo_formula resm identity r0 in let fvl = res.free_var_list in let fvl = remove x fvl in let skb' = res.skolem_bound in let fonil = construct_fo_term_list NLC_FONil in assert { fonil.model_fo_term_list_field = FONil } ; let skenv = skolem_parameters fvl { skolemized_fv_list = fonil ; skolem_env = default } fvp in let skparams = skenv.skolemized_fv_list in let skenv = skenv.skolem_env in let skparamsm = skparams.model_fo_term_list_field in assert { forall y:int. is_fo_term_free_var_in_fo_formula (Some y) res1m -> (forall z:int. is_fo_term_free_var_in_fo_formula z resm /\ r0 z = Some y -> z <> x && z = y ) && (is_fo_term_free_var_in_fo_formula y resm /\ y <> x) && mem y fvl } ; let transf = skolem_model_transformer res1m skb' skparamsm skenv in let symb = construct_symbol (NLCVar_symbol skb') in assert { symb.model_symbol_field = Var_symbol skb' } ; let skolemf = construct_fo_term (NLC_App symb skparams) in let skolemfm = skolemf.model_fo_term_field in assert { skolemfm = App (Var_symbol skb') skparamsm } ; let phir = nlsubst_fo_term_in_fo_formula res.skolemized x skolemf in let phirm = phir.model_fo_formula_field in let resf = res.model_transformer in let ghost transf2 = rcompose resf transf in (* sat (Exists phi1m) -> sat (Exists res1m). *) assert { forall m:model int 'st, rho:int -> 'st, xm:'st. formula_semantic phi1m m (ocase rho xm) -> formula_semantic phi0m m (rcompose r0 (ocase rho xm)) && formula_semantic resm (resf m) (rcompose r0 (ocase rho xm)) && formula_semantic res1m (resf m) (ocase rho xm) } ; assert { forall m:model int 'st, rho:int -> 'st. formula_semantic phim m rho -> formula_semantic (Exists res1m) (resf m) rho } ; (* sat (Exists res1m) -> sat phir. *) let ghost sub1 = subst_id_fo_term[x <- skolemfm] in let ghost r1 = ocase identity x in let ghost sub2 = ocase subst_id_fo_term skolemfm in assert { phirm = subst_fo_formula resm subst_id_symbol sub1 } ; assert { forall y:option int. is_fo_term_free_var_in_fo_formula y res1m -> (y <> Some x) && rcompose r1 sub1 y = sub2 y } ; assert { subst_fo_formula res1m subst_id_symbol sub2 = subst_fo_formula res1m subst_id_symbol (rcompose r1 sub1) } ; assert { extensionalEqual (rcompose r0 r1) identity } ; assert { phirm = subst_fo_formula res1m subst_id_symbol sub2 } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic (Exists res1m) m rho -> formula_semantic phirm (transf m) rho } ; assert { forall y:int. is_fo_term_free_var_in_fo_formula y phirm -> (forall z:int. is_fo_term_free_var_in_fo_formula z resm /\ is_fo_term_free_var_in_fo_term y (sub1 z) -> (if z <> x then z = y && mem y fvl else is_fo_term_free_var_in_fo_term y skolemfm && mem y fvl)) && mem y fvl } ; (* Vexingly painful ! *) assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phirm -> is_symbol_free_var_in_fo_formula ls (subst_fo_formula resm subst_id_symbol sub1) && ((forall z:int. is_symbol_free_var_in_fo_formula z resm /\ is_symbol_free_var_in_symbol ls (subst_id_symbol z) -> z = ls && z < skb' + 1 ) /\ (forall z:int. is_fo_term_free_var_in_fo_formula z resm /\ is_symbol_free_var_in_fo_term ls (sub1 z) -> (if z <> x then sub1 z = Var_fo_term z else is_symbol_free_var_in_fo_term ls skolemfm && ls = skb' && ls < skb' + 1) && ls < skb' + 1) /\ ((exists z:int. is_symbol_free_var_in_fo_formula z resm /\ is_symbol_free_var_in_symbol ls (subst_id_symbol z)) \/ (exists z:int. is_fo_term_free_var_in_fo_formula z resm /\ is_symbol_free_var_in_fo_term ls (sub1 z)))) && ls < skb' + 1 } ; (* Two point of views : either why3 do not deconstruct records enough, either too much. *) assert { forall m:model int 'st. let mf = (resf m).interp_fun in let mp = (resf m).interp_pred in m.interp_pred = mp = (transf ({ interp_fun = mf ; interp_pred = mp })).interp_pred = (transf2 m).interp_pred && m.interp_pred = (transf2 m).interp_pred } ; assert { forall m:model int 'st, ls:int. ls < skb -> let mf = (resf m).interp_fun in let mp = (resf m).interp_pred in eval m.interp_fun ls = eval mf ls = eval (transf { interp_fun = mf ; interp_pred = mp }).interp_fun ls = eval (transf2 m).interp_fun ls && eval m.interp_fun ls = eval (transf2 m).interp_fun ls } ; assert { forall m:model int 'st,rho:int -> 'st. let mf = (resf m).interp_fun in let mp = (resf m).interp_pred in formula_semantic phim m rho -> formula_semantic (Exists res1m) ({ interp_fun = mf ; interp_pred = mp }) rho && formula_semantic phirm (transf ({ interp_fun = mf ; interp_pred = mp})) rho && formula_semantic phirm (transf2 m) rho } ; { skolemized = phir ; skolem_bound = skb' + 1 ; model_transformer = transf2 ; free_var_list = fvl } end let rec skolemize_list (phil:nlimpl_fo_formula_list) (skb:int) (ghost fvp:set int) : skolemization_list_return 'st requires { nlimpl_fo_formula_list_ok phil } requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x phil.model_fo_formula_list_field -> S.mem x fvp } requires { is_simpl_list phil.model_fo_formula_list_field } requires { is_nnf_list phil.model_fo_formula_list_field } requires { forall ls:int. is_symbol_free_var_in_fo_formula_list ls phil.model_fo_formula_list_field -> ls < skb } ensures { nlimpl_fo_formula_list_ok result.skolemized_l } ensures { forall x:int. is_fo_term_free_var_in_fo_formula_list x result.skolemized_l.model_fo_formula_list_field -> S.mem x fvp } ensures { result.skolem_bound_l >= skb } ensures { forall ls:int. is_symbol_free_var_in_fo_formula_list ls result.skolemized_l.model_fo_formula_list_field -> ls < result.skolem_bound_l } ensures { is_nnf_list result.skolemized_l.model_fo_formula_list_field } ensures { is_simpl_list result.skolemized_l.model_fo_formula_list_field } ensures { no_existential_list result.skolemized_l.model_fo_formula_list_field } ensures { forall m:model int 'st, rho:int -> 'st. formula_list_conj_semantic phil.model_fo_formula_list_field m rho -> formula_list_conj_semantic result.skolemized_l.model_fo_formula_list_field (eval result.model_transformer_l m) rho } (* Completeness concern. ensures { forall m:model int 'st, rho:int -> 'st. formula_semantic result.skolemized.model_fo_formula_field m rho -> formula_semantic phi.model_fo_formula_field m rho *) ensures { forall m:model int 'st, ls:int. ls < skb -> eval m.interp_fun ls = eval (eval result.model_transformer_l m).interp_fun ls } ensures { forall m:model int 'st. m.interp_pred = (eval result.model_transformer_l m).interp_pred } variant { size_fo_formula_list phil.model_fo_formula_list_field } = let philm = phil.model_fo_formula_list_field in match destruct_fo_formula_list phil with | NLC_FOFNil -> { skolemized_l = phil ; skolem_bound_l = skb ; model_transformer_l = identity } | NLC_FOFCons phi phiq -> let phim = phi.model_fo_formula_field in let phiqm = phiq.model_fo_formula_list_field in assert { philm = FOFCons phim phiqm } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula ls phim -> is_symbol_free_var_in_fo_formula_list ls philm } ; assert { forall ls:int. is_symbol_free_var_in_fo_formula_list ls phiqm -> is_symbol_free_var_in_fo_formula_list ls philm } ; let res = skolemize phi skb False fvp in let resq = skolemize_list phiq res.skolem_bound fvp in let resm = res.skolemized.model_fo_formula_field in let resqm = resq.skolemized_l.model_fo_formula_list_field in let skr = construct_fo_formula_list (NLC_FOFCons res.skolemized resq.skolemized_l) in let skrm = skr.model_fo_formula_list_field in let (resf,resqf) = (res.model_transformer,resq.model_transformer_l) in let ghost transf = rcompose resf resqf in assert { skrm = FOFCons resm resqm } ; assert { forall m:model int 'st. m.interp_pred = (resf m).interp_pred = (transf m).interp_pred } ; assert { forall m:model int 'st, ls:int. ls < skb -> eval m.interp_fun ls = eval (resf m).interp_fun ls = eval (transf m).interp_fun ls } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic resm m rho <-> formula_semantic resm (resqf m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic phiqm m rho <-> formula_list_conj_semantic phiqm (resf m) rho } ; assert { forall m:model int 'st,rho:int -> 'st. transf m = resqf (resf m) && (formula_semantic phim m rho -> formula_semantic resm (resf m) rho && formula_semantic resm (transf m) rho) /\ (formula_list_conj_semantic phiqm m rho -> formula_list_conj_semantic phiqm (resf m) rho && formula_list_conj_semantic resqm (transf m) rho) } ; { skolemized_l = skr ; skolem_bound_l = resq.skolem_bound_l ; model_transformer_l = transf } end (* No need for it in the logic... *) type preprocessing_return 'st = { preprocessed : nlimpl_fo_formula_list ; final_goals_number : int ; ghost model_transf : (model int 'st) -> (model int 'st) ; } type fvr = { ghost sr : set int ; lr : list int ; } let rec term_free_vars_noghost (t:nlimpl_fo_term) : fvr requires { nlimpl_fo_term_ok t } ensures { forall x:int. is_fo_term_free_var_in_fo_term x t.model_fo_term_field -> mem x result.lr } ensures { iset_ok result.lr } ensures { forall x:int. S.mem x result.sr <-> mem x result.lr } variant { size_fo_term t.model_fo_term_field } = match destruct_fo_term t with | NLCVar_fo_term x -> { sr = S.singleton x ; lr = Cons x Nil } | NLC_App _ l -> term_list_free_vars_noghost l end with term_list_free_vars_noghost (l:nlimpl_fo_term_list) : fvr requires { nlimpl_fo_term_list_ok l } ensures { forall x:int. is_fo_term_free_var_in_fo_term_list x l.model_fo_term_list_field -> mem x result.lr } ensures { forall x:int. S.mem x result.sr <-> mem x result.lr } ensures { iset_ok result.lr } variant { size_fo_term_list l.model_fo_term_list_field } = match destruct_fo_term_list l with | NLC_FONil -> { lr = Nil ; sr = S.empty } | NLC_FOCons t q -> let r1 = term_free_vars_noghost t in let r2 = term_list_free_vars_noghost q in { lr = merge r1.lr r2.lr ; sr = S.union r1.sr r2.sr } end let rec collect_free_var_formula (phi:nlimpl_fo_formula) : fvr requires { nlimpl_fo_formula_ok phi } ensures { iset_ok result.lr } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field -> mem x result.lr } ensures { forall x:int. mem x result.lr <-> S.mem x result.sr } variant { size_fo_formula phi.model_fo_formula_field } = let phim = phi.model_fo_formula_field in match destruct_fo_formula phi with | NLC_PApp p l -> let pm = p.model_symbol_field in let lm = l.model_fo_term_list_field in assert { phim = PApp pm lm } ; term_list_free_vars_noghost l | NLC_Not phi0 -> let phi0m = phi0.model_fo_formula_field in assert { phim = Not phi0m } ; collect_free_var_formula phi0 | NLC_And phi1 phi2 -> let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in assert { phim = And phi1m phi2m } ; let r1 = collect_free_var_formula phi1 in let r2 = collect_free_var_formula phi2 in { lr = merge r1.lr r2.lr ; sr = S.union r1.sr r2.sr } | NLC_Or phi1 phi2 -> let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in assert { phim = Or phi1m phi2m } ; let r1 = collect_free_var_formula phi1 in let r2 = collect_free_var_formula phi2 in { lr = merge r1.lr r2.lr ; sr = S.union r1.sr r2.sr } | NLC_FTrue -> { lr = Nil ; sr = S.empty } | NLC_FFalse -> { lr = Nil ; sr = S.empty } | NLC_Forall x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost r0 = some[x <- None] in let ghost phi1m = rename_fo_formula phi0m identity r0 in assert { phim = Forall phi1m } ; let r = collect_free_var_formula phi0 in let res = { lr = remove x r.lr ; sr = S.remove x r.sr } in assert { forall xf:int. (forall y:int. is_fo_term_free_var_in_fo_formula y phi0m /\ eval (some[x<-None]) y = Some xf -> y <> x && Some xf = Some y && xf = y) && is_fo_term_free_var_in_fo_formula xf phim -> is_fo_term_free_var_in_fo_formula (Some xf) phi1m && (exists y:int. is_fo_term_free_var_in_fo_formula y phi0m /\ eval (some[x <- None]) y = Some xf) && is_fo_term_free_var_in_fo_formula xf phi0m && xf <> x && mem xf res.lr } ; res | NLC_Exists x phi0 -> let phi0m = phi0.model_fo_formula_field in let ghost r0 = some[x <- None] in let ghost phi1m = rename_fo_formula phi0m identity r0 in assert { phim = Exists phi1m } ; let r = collect_free_var_formula phi0 in let res = { lr = remove x r.lr ; sr = S.remove x r.sr } in assert { forall xf:int. (forall y:int. is_fo_term_free_var_in_fo_formula y phi0m /\ eval (some[x<-None]) y = Some xf -> y <> x && Some xf = Some y && xf = y) && is_fo_term_free_var_in_fo_formula xf phim -> is_fo_term_free_var_in_fo_formula (Some xf) phi1m && (exists y:int. is_fo_term_free_var_in_fo_formula y phi0m /\ eval (some[x <- None]) y = Some xf) && is_fo_term_free_var_in_fo_formula xf phi0m && xf <> x && mem xf res.lr } ; res end let rec collect_free_var_formula_list (phil:nlimpl_fo_formula_list) : fvr requires { nlimpl_fo_formula_list_ok phil } ensures { iset_ok result.lr } ensures { forall x:int. is_fo_term_free_var_in_fo_formula_list x phil.model_fo_formula_list_field -> mem x result.lr } ensures { forall x:int. mem x result.lr <-> S.mem x result.sr } variant { size_fo_formula_list phil.model_fo_formula_list_field } = match destruct_fo_formula_list phil with | NLC_FOFNil -> { lr = Nil ; sr = S.empty } | NLC_FOFCons phi0 q -> let fvr1 = collect_free_var_formula phi0 in let fvr2 = collect_free_var_formula_list q in { lr = merge fvr1.lr fvr2.lr ; sr = S.union fvr1.sr fvr2.sr } end let rec exists_quantify (l:list int) (phi:nlimpl_fo_formula) (ghost st:'st) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok phi } requires { is_simpl phi.model_fo_formula_field } requires { is_nnf phi.model_fo_formula_field } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field -> mem x l } ensures { nlimpl_fo_formula_ok result } ensures { forall x:int. not(is_fo_term_free_var_in_fo_formula x result.model_fo_formula_field) } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic phi.model_fo_formula_field m rho -> formula_semantic result.model_fo_formula_field m rho } ensures { is_simpl result.model_fo_formula_field } ensures { is_nnf result.model_fo_formula_field } variant { l } = let phim = phi.model_fo_formula_field in match l with | Nil -> phi | Cons x q -> let phi' = construct_fo_formula (NLC_Exists x phi) in let phi'_m = phi'.model_fo_formula_field in let ghost phi1m = rename_fo_formula phim identity (some[x <- None]) in assert { phi'_m = Exists phi1m } ; assert { forall xf:int. (forall y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x<-None]) y = Some xf -> y <> x && Some xf = Some y && xf = y) && is_fo_term_free_var_in_fo_formula xf phi'_m -> is_fo_term_free_var_in_fo_formula (Some xf) phi1m && (exists y:int. is_fo_term_free_var_in_fo_formula y phim /\ eval (some[x <- None]) y = Some xf) && is_fo_term_free_var_in_fo_formula xf phim && xf <> x && mem xf q } ; assert { forall m:model int 'st,rho:int -> 'st. formula_semantic phim m rho -> let rhos = ocase rho (rho x) in let sub = rcompose (some[x <- None]) subst_id_fo_term in let rhos' = semantic_subst sub m rhos in extensionalEqual rhos' rho && phi1m = subst_fo_formula phim subst_id_symbol (rcompose (some[x <- None]) subst_id_fo_term) && formula_semantic phi1m m rhos && (exists xm:'st. formula_semantic phi1m m (ocase rho xm)) && formula_semantic phi'_m m rho } ; exists_quantify q phi' st end type comb_ret = { form : nlimpl_fo_formula ; llen : int ; } let rec combine_with (l:nlimpl_fo_formula_list) (phi0:nlimpl_fo_formula) (ghost fvp:set int) (ghost st:'st) : comb_ret requires { nlimpl_fo_formula_list_ok l } requires { forall x:int. is_fo_term_free_var_in_fo_formula x phi0.model_fo_formula_field -> S.mem x fvp } requires { nlimpl_fo_formula_ok phi0 } requires { forall x:int. is_fo_term_free_var_in_fo_formula_list x l.model_fo_formula_list_field -> S.mem x fvp } requires { is_simpl_list l.model_fo_formula_list_field } requires { is_nnf_list l.model_fo_formula_list_field } requires { is_simpl phi0.model_fo_formula_field } requires { is_nnf phi0.model_fo_formula_field } variant { size_fo_formula_list l.model_fo_formula_list_field } ensures { nlimpl_fo_formula_ok result.form } ensures { is_simpl result.form.model_fo_formula_field } ensures { is_nnf result.form.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_semantic result.form.model_fo_formula_field m rho <-> (formula_list_conj_semantic l.model_fo_formula_list_field m rho /\ formula_semantic phi0.model_fo_formula_field m rho) } ensures { forall x:int. is_fo_term_free_var_in_fo_formula x result.form.model_fo_formula_field -> S.mem x fvp } = let lm = l.model_fo_formula_list_field in let phi0m = phi0.model_fo_formula_field in match destruct_fo_formula_list l with | NLC_FOFNil -> { form = phi0 ; llen = 1 } | NLC_FOFCons x q -> let xm = x.model_fo_formula_field in let qm = q.model_fo_formula_list_field in assert { lm = FOFCons xm qm } ; let cr = combine_with q x fvp st in let phi' = cr.form in let phi'_m = phi'.model_fo_formula_field in let phir = construct_fo_formula (NLC_And phi0 phi') in let phirm = phir.model_fo_formula_field in assert { phirm = And phi0m phi'_m } ; { form = phir ; llen = cr.llen + 1 } end type split_ret = { forms : nlimpl_fo_formula_list ; total_goals : int ; } let rec split (phi:nlimpl_fo_formula) (l:nlimpl_fo_formula_list) (lnum:int) (gnum:int) (ghost st:'st) : split_ret requires { nlimpl_fo_formula_ok phi } requires { forall x:int. not(is_fo_term_free_var_in_fo_formula x phi.model_fo_formula_field) } requires { is_simpl phi.model_fo_formula_field } requires { is_nnf phi.model_fo_formula_field } requires { no_existential phi.model_fo_formula_field } requires { nlimpl_fo_formula_list_ok l } requires { forall x:int. not(is_fo_term_free_var_in_fo_formula_list x l.model_fo_formula_list_field) } requires { is_simpl_list l.model_fo_formula_list_field } requires { is_nnf_list l.model_fo_formula_list_field } requires { no_existential_list l.model_fo_formula_list_field } variant { size_fo_formula phi.model_fo_formula_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic result.forms.model_fo_formula_list_field m rho <-> (formula_semantic phi.model_fo_formula_field m rho /\ formula_list_conj_semantic l.model_fo_formula_list_field m rho) } ensures { nlimpl_fo_formula_list_ok result.forms } ensures { forall x:int. not(is_fo_term_free_var_in_fo_formula_list x result.forms.model_fo_formula_list_field) } ensures { is_simpl_list result.forms.model_fo_formula_list_field } ensures { is_nnf_list result.forms.model_fo_formula_list_field } ensures { no_existential_list result.forms.model_fo_formula_list_field } = match destruct_fo_formula phi with | NLC_And phi1 phi2 -> (* gnum <> 0 : either need full count (<0), either phi is a "goal". if lnum = 1, then gnumcall must be updated accordingly. if lnum <> 1 (not last of initial list), then either gnum = 1 (last goal,do not want next count), either it is expected. *) let phim = phi.model_fo_formula_field in let phi1m = phi1.model_fo_formula_field in let phi2m = phi2.model_fo_formula_field in assert { phim = And phi1m phi2m } ; assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi1m -> is_fo_term_free_var_in_fo_formula x phim } ; assert { forall x:int. is_fo_term_free_var_in_fo_formula x phi2m -> is_fo_term_free_var_in_fo_formula x phim } ; let gnumcall = if lnum = 1 then if gnum <> 0 then (-1) else gnum - 1 else gnum - 1 in let r0 = split phi2 l (lnum-1) gnumcall st in let l0 = r0.forms in (* need full count for r1. *) let r1 = split phi1 l0 0 (-1) st in let l1 = r1.forms in { forms = l1 ; total_goals = if gnum <> 0 then r0.total_goals + r1.total_goals else 0 } | _ -> let lr = construct_fo_formula_list (NLC_FOFCons phi l) in { forms = lr ; total_goals = if gnum <> 0 then 1 else 0 } end (* Prover preprocessing function: From a set of formulas, return an equi-satisfiable (as completeness is not considered here, it is only proved that satisfiability is preserved) set of formulas without occurrence of true/false, in negational normal form, without existential quantifiers. Potentially raises an exception when the input set of formulas was (trivially) unsatisfiable. *) exception Sat let preprocessing (phil:nlimpl_fo_formula_list) (gnum:int) (ghost st:'st) : preprocessing_return 'st requires { nlimpl_fo_formula_list_ok phil } ensures { nlimpl_fo_formula_list_ok result.preprocessed } ensures { forall x:int. not(is_fo_term_free_var_in_fo_formula_list x result.preprocessed.model_fo_formula_list_field) } ensures { is_nnf_list result.preprocessed.model_fo_formula_list_field } ensures { is_simpl_list result.preprocessed.model_fo_formula_list_field } ensures { no_existential_list result.preprocessed.model_fo_formula_list_field } ensures { forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic phil.model_fo_formula_list_field m rho -> formula_list_conj_semantic result.preprocessed.model_fo_formula_list_field (eval result.model_transf m) rho } raises { Unsat -> forall m:model int 'st,rho:int -> 'st. not(formula_list_conj_semantic phil.model_fo_formula_list_field m rho) } raises { Sat -> forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic phil.model_fo_formula_list_field m rho } = let s = collect_free_var_formula_list phil in let fvp = s.sr in let (phisimpl,gnum) = nnf_simpl_list phil gnum fvp st in match destruct_fo_formula_list phisimpl with | NLC_FOFNil -> raise Sat | NLC_FOFCons phi0 q -> let cb = combine_with q phi0 fvp st in let len = cb.llen in let phicb = cb.form in let phiex = exists_quantify s.lr phicb st in let skr = (skolemize phiex phiex.nlfree_var_symbol_set_abstraction_fo_formula_field False S.empty:skolemization_return 'st) in let phisk = skr.skolemized in let tr = skr.model_transformer in let fonil = construct_fo_formula_list NLC_FOFNil in let spl = split phisk fonil len gnum st in assert { forall m:model int 'st,rho:int -> 'st. formula_list_conj_semantic phil.model_fo_formula_list_field m rho -> formula_list_conj_semantic phisimpl.model_fo_formula_list_field m rho && (formula_semantic phi0.model_fo_formula_field m rho /\ formula_list_conj_semantic q.model_fo_formula_list_field m rho) && formula_semantic phicb.model_fo_formula_field m rho && formula_semantic phisk.model_fo_formula_field (tr m) rho && formula_list_conj_semantic fonil.model_fo_formula_list_field (tr m) rho && formula_list_conj_semantic spl.forms.model_fo_formula_list_field (tr m) rho } ; { preprocessed = spl.forms ; final_goals_number = spl.total_goals ; model_transf = tr } end (* let preprocessing (phil:nlimpl_fo_formula_list) : preprocessing_return 'st requires { nlimpl_fo_formula_list_ok phil } ensures { nlimpl_fo_formula_list_ok result.preprocessed } ensures { forall x:int. not(is_fo_term_free_var_in_fo_formula_list x result.preprocessed.model_fo_formula_list_field) } ensures { is_nnf_list result.preprocessed.model_fo_formula_list_field } ensures { is_simpl_list result.preprocessed.model_fo_formula_list_field } ensures { no_existential_list result.preprocessed.model_fo_formula_list_field } ensures { forall m:model int 'st, rho:int -> 'st. formula_list_conj_semantic phil.model_fo_formula_list_field m rho -> formula_list_conj_semantic result.preprocessed.model_fo_formula_list_field (eval result.model_transf m) rho } raises { Unsat -> forall m:model int 'st,rho:int -> 'st. not(formula_list_conj_semantic phil.model_fo_formula_list_field m rho) } = let s = collect_free_var_formula_list in let fvp = s.sr in let phil' = nnf_simpl_list phil fvp in TODO let skr = (skolemize_list phil' phil'.nlfree_var_symbol_set_abstraction_fo_formula_list_field fvp: skolemization_list_return 'st) in { preprocessed = skr.skolemized_l ; model_transf = skr.model_transformer_l }*) end
Generated by why3doc 1.7.0