Commit 8c06d842 authored by Mário Pereira's avatar Mário Pereira
Browse files
parents 3a01684a 3082132d
......@@ -32,8 +32,8 @@ timeout "interrupted by timeout"
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
*)
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -42,14 +42,4 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
......@@ -29,6 +29,8 @@ transformation "simplify_formula"
transformation "encoding_smt"
transformation "encoding_sort"
(*
disabled: veriT seems more efficient with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -37,7 +39,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
(*
Local Variables:
......
......@@ -58,3 +58,17 @@ goal G1: forall x:real. x >. 2.0 -> (pow x 3.0) *. 2.0 >. 20.0
goal G2: forall x:real. x >. 2.0 -> x >. 5.0
end
theory PolyPaverExamples
use import real.Real
use import real.ExpLog
goal g1: forall a b : real.
-10.0 <= a <= 10.0 ->
-10.0 <= b <= 10.0 ->
b > a + 0.1 ->
exp a - exp b > (b-a) * exp ((a + b) / 2.0)
end
......@@ -88,4 +88,25 @@ module AllZeros
in
check_from 0
(** divide-and-conqueer *)
predicate zero_interval (a: array int) (lo hi: int) =
forall i: int. lo <= i < hi -> a[i] = 0
use import int.ComputerDivision
let all_zeros5 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let rec check_between (lo hi: int) : bool
requires { 0 <= lo <= hi <= a.length }
variant { hi - lo }
ensures { result <-> zero_interval a lo hi }
=
hi <= lo ||
let mid = lo + div (hi - lo) 2 in
a[mid] = 0 && check_between lo mid && check_between (mid+1) hi
in
check_between 0 (Array.length a)
end
......@@ -45,7 +45,7 @@
</transf>
</goal>
</theory>
<theory name="AllZeros" sum="1d320632b50748c7da056f42e9fe27a9" expanded="true">
<theory name="AllZeros" sum="4d522333682d37ebf90b16bbe3ff5d1b" expanded="true">
<goal name="WP_parameter all_zeros1" expl="VC for all_zeros1" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="104"/></proof>
</goal>
......@@ -58,6 +58,9 @@
<goal name="WP_parameter all_zeros4" expl="VC for all_zeros4" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="WP_parameter all_zeros5" expl="VC for all_zeros5" expanded="true">
<proof prover="3" timelimit="61"><result status="valid" time="0.88" steps="292"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -223,7 +223,7 @@ let rec print_dity pri fmt = function
(print_dity 1) t1 (print_dity 0) t2
| Dpur (s,tl) when is_ts_tuple s.its_ts ->
Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity 0)) tl
| Dpur (s,tl) when s.its_mutable || s.its_regions <> [] ->
| Dpur (s,tl) when its_impure s ->
Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "{%a}%a")
Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
| Dpur (s,tl) ->
......
......@@ -162,10 +162,7 @@ let rs_dup ({rs_name = {id_loc = loc}} as s) c =
check_effects ?loc c;
mk_rs id c RLlemma None
let create_field id s v =
if not (List.exists (fun u -> pv_equal u v) s.its_mfields ||
List.exists (fun u -> pv_equal u v) s.its_ifields) then
invalid_arg "Expr.create_field";
let create_projection id s v =
let eff = eff_ghostify v.pv_ghost eff_empty in
let tyl = List.map ity_var s.its_ts.ts_args in
let ity = ity_app s tyl s.its_regions in
......@@ -173,18 +170,17 @@ let create_field id s v =
let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in
let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
let c = create_cty [arg] [] [q] Mexn.empty eff v.pv_ity in
mk_rs ls.ls_name c (RLls ls) (Some v)
let fld = if List.exists (pv_equal v) s.its_mfields then Some v else None in
mk_rs ls.ls_name c (RLls ls) fld
let create_constructor ~constr id s fl =
let exn = Invalid_argument "Expr.create_constructor" in
let fs = List.fold_right (Spv.add_new exn) fl Spv.empty in
if s.its_private || s.its_def <> None then raise exn;
if s.its_mutable then begin
if s.its_privmut || s.its_def <> None then raise exn;
if s.its_mfields <> [] then begin
if constr <> 1 then raise exn;
let mfs = Spv.of_list s.its_mfields in
let ifs = Spv.of_list s.its_ifields in
let sfs = Spv.union mfs ifs in
if not (Spv.equal fs sfs) then raise exn
if not (Spv.subset mfs fs) then raise exn
end else if constr < 1 then raise exn;
let argl = List.map (fun a -> a.pv_vs.vs_ty) fl in
let tyl = List.map ity_var s.its_ts.ts_args in
......@@ -366,7 +362,7 @@ let e_locate_effect pr e = fst (find_effect pr None e)
let localize_ghost_write v r el =
let taints eff = Mreg.mem r eff.eff_taints in
let writes eff = match Mreg.find_opt r eff.eff_writes with
| Some fds -> r.reg_its.its_private ||
| Some fds -> r.reg_its.its_privmut ||
Spv.exists (fun fd -> not fd.pv_ghost) fds
| None -> false in
(* check if some component taints region r *)
......
......@@ -58,7 +58,7 @@ val create_rsymbol : preid -> ?ghost:bool -> ?kind:rs_kind -> cty -> rsymbol
val create_constructor :
constr:int -> preid -> itysymbol -> pvsymbol list -> rsymbol
val create_field : preid -> itysymbol -> pvsymbol -> rsymbol
val create_projection : preid -> itysymbol -> pvsymbol -> rsymbol
val restore_rs : lsymbol -> rsymbol
(** raises [Not_found] if the argument is not a [rs_logic] *)
......
This diff is collapsed.
......@@ -17,16 +17,16 @@ open Term
type itysymbol = private {
its_ts : tysymbol; (** pure "snapshot" type symbol *)
its_private : bool; (** is a private/abstract type *)
its_mutable : bool; (** is a record with mutable fields *)
its_mfields : pvsymbol list; (** mutable fields of a mutable type *)
its_ifields : pvsymbol list; (** immutable fields of a mutable type *)
its_privmut : bool; (** private mutable record type *)
its_mfields : pvsymbol list; (** mutable record fields *)
its_regions : region list; (** mutable shareable components *)
its_reg_vis : bool list; (** non-ghost shareable components *)
its_arg_vis : bool list; (** non-ghost type parameters *)
its_arg_upd : bool list; (** updatable type parameters *)
its_arg_imm : bool list; (** non-updatable type parameters *)
its_arg_exp : bool list; (** exposed type parameters *)
its_def : ity option; (** is a type alias *)
its_arg_vis : bool list; (** non-ghost type parameters *)
its_arg_frz : bool list; (** irreplaceable type parameters *)
its_reg_vis : bool list; (** non-ghost shareable components *)
its_reg_frz : bool list; (** irreplaceable shareable components *)
its_def : ity option; (** type alias *)
}
and ity = private {
......@@ -93,18 +93,40 @@ val ity_hash : ity -> int
val reg_hash : region -> int
val pv_hash : pvsymbol -> int
exception ImpurePrivateField of ity
exception DuplicateRegion of region
exception UnboundRegion of region
(** creation of a symbol for type in programs *)
val create_itysymbol :
preid -> (tvsymbol * bool * bool * bool) list ->
bool -> bool -> (region * bool) list ->
bool Mpv.t -> ity option -> itysymbol
val create_itysymbol_pure : preid -> tvsymbol list -> itysymbol
(** [create_itysymbol_pure id args] creates a new type symbol with
immutable type arguments and with no mutable fields or subregions.
This function should be used for all immutable non-updatable types:
abstract types, private immutable records, immutable records with
invariant, and recursive algebraic types. *)
val create_itysymbol_alias : preid -> tvsymbol list -> ity -> itysymbol
(** [create_itysymbol_alias id args def] creates a new type alias. *)
val create_itysymbol_rich :
preid -> tvsymbol list -> bool -> Spv.t -> Spv.t -> itysymbol
(** [create_itysymbol_rich id args privmut mfields ifields] creates
a new type symbol. Every mutable and immutable field is represented
by a [pvsymbol] of the corresponding ghost status in the [mfields]
or [ifields] set, respectively. The variables from [mfields] are
stored in the created type symbol and used in effects. If [privmut]
is [true], then all types in [mfields] and [ifields] must be pure. *)
val restore_its : tysymbol -> itysymbol
(** raises [Not_found] if the argument is not a [its_ts] *)
val its_mutable : itysymbol -> bool
(** [its_mutable s] checks if [s] is a mutable record or an alias for one *)
val its_impure : itysymbol -> bool
(** [its_impure s] checks if [s] is mutable or has mutable components *)
(** {2 Type constructors} *)
exception BadItyArity of itysymbol * int
......@@ -173,7 +195,6 @@ val ity_r_stale : region -> Sreg.t -> ity -> bool
val reg_r_stale : region -> Sreg.t -> region -> bool
val ity_closed : ity -> bool
val ity_immutable : ity -> bool
(* detect non-ghost type variables and regions *)
......@@ -261,7 +282,6 @@ exception AssignPrivate of region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception WriteImmutable of region * pvsymbol
exception GhostDivergence
type effect = private {
......
......@@ -63,11 +63,17 @@ let pp_url fmt lp =
| _ ->
Format.fprintf fmt "%s.html" fn
let pp_anchor fmt id = match id.id_loc with
let pp_anchor fmt id =
match id.id_loc with
| None -> raise Not_found
| Some loc -> let _, l, _, _ = Loc.get loc in pp_tag fmt id.id_string l
| Some loc ->
let _, l, _, _ = Loc.get loc in pp_tag fmt id.id_string l
let pp_locate fmt id =
let lp, _, _ =
try Mlw_module.restore_path id with Not_found -> Theory.restore_path id in
Format.fprintf fmt "%a#%a" pp_url lp pp_anchor id
match id.id_loc with
| None -> raise Not_found
| Some _loc ->
let lp, _, _ =
try Mlw_module.restore_path id with Not_found -> Theory.restore_path id
in
Format.fprintf fmt "%a#%a" pp_url lp pp_anchor id
......@@ -22,6 +22,7 @@ val set_stdlib_url: string -> unit
val output_file: string -> string
val pp_anchor: Format.formatter -> ident -> unit
(* raises [Not_found] if ident has no location *)
val pp_locate: Format.formatter -> ident -> unit
(* or raises [Not_found] *)
(* raises [Not_found] if ident has no location *)
......@@ -63,13 +63,17 @@
(* Format.eprintf " IDENT %s/%d/%d@." f l c; *)
(* is this a def point? *)
try
match Glob.find loc with
| id, Glob.Def ->
fprintf fmt "<a name=\"%a\">%a</a>"
Doc_def.pp_anchor id Pp.html_string s
| id, Glob.Use ->
fprintf fmt "<a href=\"%a\">%a</a>"
Doc_def.pp_locate id Pp.html_string s
let id, def = Glob.find loc in
match id.Ident.id_loc with
| None -> raise Not_found
| Some _ ->
match def with
| Glob.Def ->
fprintf fmt "<a name=\"%a\">%a</a>"
Doc_def.pp_anchor id Pp.html_string s
| Glob.Use ->
fprintf fmt "<a href=\"%a\">%a</a>"
Doc_def.pp_locate id Pp.html_string s
with Not_found ->
(* otherwise, just print it *)
pp_print_string fmt s
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment