mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
97 lines
3.4 KiB
Plaintext
97 lines
3.4 KiB
Plaintext
|
|
module Types
|
|
|
|
end
|
|
|
|
module Impl
|
|
|
|
use Firstorder_semantics.Sem
|
|
use Firstorder_term_spec.Spec
|
|
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.Types
|
|
use Firstorder_formula_list_impl.Logic
|
|
use Firstorder_formula_list_impl.Impl
|
|
use Firstorder_tableau_spec.Spec
|
|
use Firstorder_tableau_impl.Types
|
|
use Firstorder_tableau_impl.Logic
|
|
use Firstorder_tableau_impl.Impl
|
|
use FormulaTransformations.Types
|
|
use FormulaTransformations.Logic
|
|
use FormulaTransformations.Impl
|
|
use Unification.Types
|
|
use Unification.Logic
|
|
use Functions.Func
|
|
use option.Option
|
|
use OptionFuncs.Funcs
|
|
use bool.Bool
|
|
use int.Int
|
|
use Prover.Types
|
|
use Prover.Logic
|
|
use Prover.Impl
|
|
use list.List
|
|
use import set.Set as S
|
|
use import BacktrackArray.Impl as BA
|
|
|
|
val ghost sdata_inv_hack (u:unit) : sdata -> bool
|
|
ensures { result = sdata_inv }
|
|
|
|
let main (base:nlimpl_fo_formula_list) (gnum:int) (ghost st:'st): int
|
|
requires { nlimpl_fo_formula_list_ok base }
|
|
diverges
|
|
ensures { forall m:model int 'st,rho:int -> 'st.
|
|
not(formula_list_conj_semantic base.model_fo_formula_list_field m rho) }
|
|
raises { Sat -> forall m:model int 'st,rho:int -> 'st.
|
|
formula_list_conj_semantic base.model_fo_formula_list_field m rho }
|
|
=
|
|
let root = construct_tableau NLC_Root in
|
|
try let phip = preprocessing base gnum st in
|
|
let phip0 = (phip:preprocessing_return 'st).preprocessed in
|
|
let phip0m = phip0.model_fo_formula_list_field in
|
|
assert { root.model_tableau_field = Root } ;
|
|
let gnum = phip.final_goals_number in
|
|
let gnum = if gnum <= 0 then (-1) else gnum in
|
|
let rec aux (n:int) (ghost st:'st) : (int, prover_return)
|
|
diverges
|
|
returns { (_,{ contradictory_assignment = s }) ->
|
|
forall m:model int 'st,rho:int -> 'st.
|
|
let rhos = semantic_subst s m rho in
|
|
not(formula_list_conj_semantic phip0.model_fo_formula_list_field m rhos) }
|
|
=
|
|
(* Do work to define them outside the loop, but harder
|
|
to prove while not more performant. *)
|
|
let unifb = BA.create (sdata_inv_hack ()) in
|
|
let unif = {
|
|
unifier_base_model = subst_id_fo_term ;
|
|
unifier = subst_id_fo_term } in
|
|
assert { extensionalEqual (smodel (BA.current_timestamp unifb))
|
|
(subst_id_fo_term) &&
|
|
(smodel (BA.current_timestamp unifb)) = subst_id_fo_term } ;
|
|
assert { forall x:int. unassigned (BA.current_timestamp unifb) x } ;
|
|
try (n,extend_branch phip0 root unifb unif 0 n gnum st)
|
|
with Failure -> aux (n+1) st
|
|
end
|
|
in
|
|
let n,r = aux 0 st in
|
|
let s = r.contradictory_assignment in
|
|
let basem = base.model_fo_formula_list_field in
|
|
let tr = phip.model_transf in
|
|
assert { forall m:model int 'st,rho:int -> 'st.
|
|
let m' = { interp_fun = (tr m).interp_fun ;
|
|
interp_pred = (tr m).interp_pred } in
|
|
let rhos = semantic_subst s m' rho in
|
|
m' = (tr m) &&
|
|
not(formula_list_conj_semantic phip0m m' rhos) &&
|
|
(forall x:int. is_fo_term_free_var_in_fo_formula_list x phip0m ->
|
|
rho x = rhos x) &&
|
|
not(formula_list_conj_semantic phip0m m' rho) &&
|
|
not(formula_list_conj_semantic basem m rho) };
|
|
n
|
|
with Unsat -> 0
|
|
end
|
|
|
|
end
|