mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1468 lines
67 KiB
Plaintext
1468 lines
67 KiB
Plaintext
|
|
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
|