mirror of
https://github.com/Z3Prover/z3
synced 2025-06-24 06:43:40 +00:00
19 lines
625 B
Text
19 lines
625 B
Text
quote(mlmli,"
|
|
(**
|
|
A model assigns uninterpreted sorts to finite universes of distinct values, constants to values,
|
|
and arrays and functions to finite maps from argument values to result values plus a default
|
|
value for all other arguments.
|
|
*)
|
|
type model_refined = {
|
|
sorts : (sort, ast_vector) Hashtbl.t;
|
|
consts : (func_decl, ast) Hashtbl.t;
|
|
arrays : (func_decl, (ast, ast) Hashtbl.t * ast) Hashtbl.t;
|
|
funcs : (func_decl, (ast array, ast) Hashtbl.t * ast) Hashtbl.t;
|
|
}
|
|
");
|
|
quote(mli,"
|
|
(**
|
|
Summary: [model_refine c m] is the refined model of [m].
|
|
*)
|
|
val model_refine : context -> model -> model_refined
|
|
");
|