Skip to content

Commit

Permalink
I create a new kind of values in Alt-Ergo, named model values, for co…
Browse files Browse the repository at this point in the history 
…nstant

semantic values. Each Shostak theory exposes a new module Value that
produces on demand a model value (if it can) for an interpreted semantic
value of theory. Uninterpreted semantic values are managed by the module
Shostak itself.
  • Loading branch information
@Halbaroth
Halbaroth committed Aug 30, 2023
1 parent d2e51d4 commit 8233963
Show file tree
Hide file tree
Showing 37 changed files with 606 additions and 458 deletions.
3 changes: 2 additions & 1 deletion src/lib/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,9 @@
dune-build-info
alt_ergo_prelude
fmt
ppx_deriving.ord
)
(preprocess (pps ppx_blob))
(preprocess (pps ppx_blob ppx_deriving.ord))
(preprocessor_deps (glob_files ../preludes/*.ae))

; .mli only modules *also* need to be in this field
Expand Down
8 changes: 3 additions & 5 deletions src/lib/frontend/frontend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,12 +162,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
far. You may need to change your model generation strategy \
or to increase your timeouts. Returned timeout reason = %s@]" s

| Some mdl ->
| Some _ ->
assert (get_m);
if get_m then
Printer.print_dbg "@[<v 0>Returned timeout reason = %s@]" s;
let mdl = Lazy.force mdl in
Models.pp (Options.Output.get_fmt_std ()) mdl
if get_m && Options.get_debug () then
Printer.print_dbg "@[<v 0>; Returned timeout reason = %s@]" s

let filter_by_all_sat propositional filter =
if filter == E.Set.empty then propositional
Expand Down
156 changes: 76 additions & 80 deletions src/lib/frontend/models.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,14 +48,14 @@ let constraints = ref MS.empty
type objective_value =
| Obj_pinfty
| Obj_minfty
| Obj_val of string
| Obj_val of X.Value.t
| Obj_unk

let pp_objective_value ppf obj_val =
match obj_val with
| Obj_pinfty -> Fmt.pf ppf "+oo"
| Obj_minfty -> Fmt.pf ppf "-oo"
| Obj_val s -> Fmt.pf ppf "%s" s
| Obj_val v -> X.Value.pp ppf v
| Obj_unk -> Fmt.pf ppf "(interval -oo +oo)"

let pp_objective ppf (obj_t, obj_val) =
Expand All @@ -73,10 +73,7 @@ type t = {
functions : ModelMap.t;
arrays : ModelMap.t;
objectives : (Expr.t * objective_value) Util.MI.t;
terms_values : (X.r * string) ME.t (* a map from terms to their values
in the model (as a
representative of type X.r and
as a string *)
terms_values : Shostak.Combine.Value.t ME.t
}

module Pp_smtlib_term = struct
Expand Down Expand Up @@ -142,15 +139,15 @@ module Pp_smtlib_term = struct

| Sy.L_built (Sy.IsConstr hs), [e] ->
if get_output_smtlib () then
fprintf fmt "((_ is %a) %a)" Hstring.print hs print e
fprintf fmt "((_ is %a) %a)" Hstring.pp hs print e
else
fprintf fmt "(%a ? %a)" print e Hstring.print hs
fprintf fmt "(%a ? %a)" print e Hstring.pp hs

| Sy.L_neg_built (Sy.IsConstr hs), [e] ->
if get_output_smtlib () then
fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e
fprintf fmt "(not ((_ is %a) %a))" Hstring.pp hs print e
else
fprintf fmt "not (%a ? %a)" print e Hstring.print hs
fprintf fmt "not (%a ? %a)" print e Hstring.pp hs

| (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
| Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
Expand Down Expand Up @@ -209,7 +206,7 @@ module Pp_smtlib_term = struct

(* TODO: introduce PrefixOp in the future to simplify this ? *)
| Sy.Op (Sy.Constr hs), ((_::_) as l) ->
fprintf fmt "%a(%a)" Hstring.print hs print_list l
fprintf fmt "%a(%a)" Hstring.pp hs print_list l

| Sy.Op _, [e1; e2] ->
if get_output_smtlib () then
Expand All @@ -219,7 +216,7 @@ module Pp_smtlib_term = struct

| Sy.Op Sy.Destruct (hs, grded), [e] ->
fprintf fmt "%a#%s%a"
print e (if grded then "" else "!") Hstring.print hs
print e (if grded then "" else "!") Hstring.pp hs


| Sy.In(lb, rb), [t] ->
Expand Down Expand Up @@ -263,6 +260,12 @@ module Pp_smtlib_term = struct

end

module MV = Map.Make (struct
type t = X.Value.t

let compare = X.Value.compare
end)

module SmtlibCounterExample = struct
let rec pp_dummy_value_of_type ppf ty =
match ty with
Expand All @@ -277,16 +280,17 @@ module SmtlibCounterExample = struct
if not (Options.get_interpretation_use_underscore ()) then
pp_dummy_value_of_type fmt ty
else
fprintf fmt "_ "
Fmt.pf fmt "_ "

let add_records_destr records record_name destr_name rep =
let destrs =
(* let add_records_destr records record_name destr_name rep =
let destrs =
try MS.find record_name records
with Not_found -> MS.empty
in
let destrs =
MS.add destr_name rep destrs in
MS.add record_name destrs records
in
let destrs =
MS.add destr_name rep destrs
in
MS.add record_name destrs records *)

let mk_records_constr records record_name
{ Ty.name = _n; record_constr = cstr; lbs = lbs; _} =
Expand All @@ -313,47 +317,49 @@ module SmtlibCounterExample = struct
(Hstring.view cstr)
print_destr (destrs,lbs)

let add_record_constr records record_name
(* let add_record_constr records record_name
{ Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values =
List.fold_left2(fun records (destr,_) (rep,_) ->
List.fold_left2(fun records (destr,_) (rep,_) ->
add_records_destr
records
record_name
(Hstring.view destr)
(asprintf "%a" Pp_smtlib_term.print rep)
) records lbs xs_values

let check_records records xs_ty_named xs_values f ty rep =
match xs_ty_named with
| [Ty.Trecord _r, _arg] -> begin
) records lbs xs_values *)

(* TODO: restore this check. *)
(* let check_records records xs_ty_named xs_values f ty v =
let records = MS.map (MS.map (Fmt.str "%a" X.Value.pp)) records in
let name = Fmt.str "%a" X.Value.pp v in
match xs_ty_named with
| [Ty.Trecord _r, _arg] -> begin
match xs_values with
| [record_name,_] ->
add_records_destr
records
(asprintf "%a" Expr.print record_name)
(Sy.to_string f)
rep
name
| [] | _ -> records
end
| _ ->
| _ ->
match ty with
| Ty.Trecord r ->
add_record_constr records rep r xs_values
| _ -> records
add_record_constr records name r xs_values
| _ -> records *)

let print_fun_def ~is_array fmt name args ty t =
let print_args fmt (ty,name) =
Format.fprintf fmt "(%s %a)" name Ty.pp_smtlib ty in
let print_fun_def ppf name args ty t =
let print_args ppf (ty,name) =
Fmt.pf ppf "(%s %a)" name Ty.pp_smtlib ty in
let defined_value =
try
let res,_,_ = (MS.find (Sy.to_string name) !constraints) in
dprintf "%s" res
with _ -> t
in

Format.fprintf fmt
"@ (@[define-%s %a (%a) %a@ %t)@]"
(if is_array then "array" else "fun")
Fmt.pf ppf
"@ (@[define-fun %a (%a) %a@ %t)@]"
Sy.print name
(Printer.pp_list_space (print_args)) args
Ty.pp_smtlib ty
Expand All @@ -364,7 +370,7 @@ module SmtlibCounterExample = struct
(fun (f, xs_ty, ty) st ->
assert (xs_ty == []);
match ModelMap.V.elements st with
| [[], rep] ->
| [([], rep)] ->
let rep =
match ty with
| Ty.Trecord r ->
Expand All @@ -373,31 +379,34 @@ module SmtlibCounterExample = struct
| _ -> dprintf "%a" pp rep
in

print_fun_def ~is_array:false fmt f [] ty rep
print_fun_def fmt f [] ty rep
| _ -> assert false
)

let output_functions_counterexample ?(is_array=false) pp fmt records fprofs =
let output_functions_counterexample pp fmt records fprofs =
let records = ref records in
ModelMap.iter
(fun (f, xs_ty, ty) st ->
let xs_ty_named = List.mapi (fun i ty ->
ty,(sprintf "arg_%d" i)
) xs_ty in

let xs_ty_named =
List.mapi (fun i ty ->
ty,(sprintf "arg_%d" i)
) xs_ty
in
let rep =
let representants =
ModelMap.V.fold (fun (xs_values,(rep,srep)) acc ->
ModelMap.V.fold (fun (xs_values, v) acc ->
assert ((List.length xs_ty_named) = (List.length xs_values));
records :=
check_records !records xs_ty_named xs_values f ty srep;
let reps = try MX.find rep acc |> snd with Not_found -> [] in
MX.add rep (srep, xs_values :: reps) acc
) st MX.empty in

let representants = MX.fold (fun rep (srep, xs_values_list) acc ->
((rep, srep),xs_values_list) :: acc) representants [] in

(* records :=
check_records !records xs_ty_named xs_values f ty v; *)
let vs = try MV.find v acc with Not_found -> [] in
MV.add v (xs_values :: vs) acc
) st MV.empty
in
let representants =
MV.fold (fun v xs_values_list acc ->
(v, xs_values_list) :: acc
) representants []
in
let rec mk_ite_and xs tys =
match xs, tys with
| [],[] -> assert false
Expand Down Expand Up @@ -446,15 +455,10 @@ module SmtlibCounterExample = struct
else
reps_aux representants
in
print_fun_def ~is_array fmt f xs_ty_named ty rep;
print_fun_def fmt f xs_ty_named ty rep;
) fprofs;
!records

let output_arrays_counterexample pp fmt arrays =
let _records = output_functions_counterexample
~is_array:true pp fmt MS.empty arrays in
()

end
(* of module SmtlibCounterExample *)

Expand All @@ -466,28 +470,23 @@ type value_defn =
| Constant of Symbols.t * Ty.t
(* A constant of a given type. If the constant is defined in a model, it
must be resolved before being printed. *)
| Value of X.r * string
(* A leaf semantic value. This must be an actual value, i.e. it must not
| Value of X.Value.t
(* A model value. This must be an actual value, i.e. it must not
contain any uninterpreted terms. *)

let value (r, s) =
match X.term_extract r with
| Some t, _ ->
begin match E.term_view t with
| { f = Name _ as sy; _ } -> Constant (sy, X.type_info r)
| _ -> Value (r, s)
end
| _ ->
Value (r, s)
let value v =
match X.Value.extract v with
| Some (Name _ as sy, ty) -> Constant (sy, ty)
| _ -> Value v

let rec pp_value ppk ppf = function
| Store (a, k, v) ->
Format.fprintf ppf "(@[<hv>store@ %a@ %a %a)@]"
Fmt.pf ppf "(@[<hv>store@ %a@ %a %a)@]"
(pp_value ppk) a
(pp_value ppk) k
(pp_value ppk) v
| Constant (sy, t) -> ppk ppf (sy, t)
| Value (_, s) -> Format.pp_print_string ppf s
| Value v -> X.Value.pp ppf v

let pp_constant ppf (_, t) =
Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
Expand All @@ -506,9 +505,9 @@ let pp fmt mdl =
(* Add the constants *)
ModelMap.iter (fun (f, xs_ty, _) st ->
assert (Lists.is_empty xs_ty);
ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
ModelMap.V.iter (fun (keys, v) ->
assert (Lists.is_empty keys);
Hashtbl.add values f (value (value_r, value_s))
Hashtbl.add values f (value v)
) st
) mdl.constants;

Expand All @@ -519,8 +518,8 @@ let pp fmt mdl =
with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty))
in
Hashtbl.replace values f @@
ModelMap.V.fold (fun (keys, rs) acc ->
Store (acc, value (snd (List.hd keys)), value rs)) st root
ModelMap.V.fold (fun (keys, v) acc ->
Store (acc, value (snd (List.hd keys)), value v)) st root
) mdl.arrays;

let pp_value =
Expand All @@ -533,16 +532,13 @@ let pp fmt mdl =
(* Functions *)
let records =
SmtlibCounterExample.output_functions_counterexample
~is_array:false pp_x fmt MS.empty mdl.functions
pp_x fmt MS.empty mdl.functions
in

(* Constants *)
SmtlibCounterExample.output_constants_counterexample
pp_x fmt records mdl.constants;

(* Arrays *)
SmtlibCounterExample.output_arrays_counterexample pp_x fmt mdl.arrays;

Printer.print_fmt fmt "@]@,)";

(* TODO: Remove this option
Expand Down
7 changes: 3 additions & 4 deletions src/lib/frontend/models.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
type objective_value =
| Obj_pinfty
| Obj_minfty
| Obj_val of string
| Obj_val of Shostak.Combine.Value.t
| Obj_unk

type t = {
Expand All @@ -43,9 +43,8 @@ type t = {
arrays : ModelMap.t;
objectives : (Expr.t * objective_value) Util.MI.t;

terms_values : (Shostak.Combine.r * string) Expr.Map.t
(* a map from terms to their values in the model (as a
representative of type X.r and as a string *)
terms_values : Shostak.Combine.Value.t Expr.Map.t
(** A map from terms to their values in the model. *)
}

(** Print the given counterexample on the given formatter with the
Expand Down
Loading

0 comments on commit 8233963

Please sign in to comment.