From f451ee0d179ca70c63eabfd761ec2bd7fc165cd0 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 21 Dec 2023 18:38:58 +0100 Subject: [PATCH] Refactoring models representation (#925) * Refactoring model * Creating a module for identifiers As we need to use identifiers in both `Symbols` and `Value` of models, I create a new module `Id.ml` which contains namespaces for internal identifiers and abstract values. * Clean-up printers * Reset the cache at the start of generation model The call to `Cache.reset` wasn't in the appropriate function and reset the cache after computing each model value. * Produce an abstract value for abstract type. We cannot produce a concrete value for a symbol whose the type is an abstract value. For instance, consider the input file: ``` (set-logic ALL) (set-option :produce-models true) (declare-sort s 0) (declare-const a s) (declare-const b s) (assert (= a b)) (check-sat) (get-model) ``` Alt-Ergo outputs `unknown`, which makes sense as we don't know anything about the abstract type `s`. As `a` and `b` are user-defined, we have to print something in the model about them but we cannot! Thus, we have to print abstract values for them. * Restoring record model generation * Print the same abstract value of equal semantic values. If we have the equation `a = b` for two terms `a` and `b` and we produce an abstract value for `a`, we have to use the same abstract value for `b` in the model. * Prefix unused arguments of model values Prefix unused arguments of model values by an underscore. In the current codebase, the only situation in which such arguments can appear is while printing constants. * Restoring objectives in interpretation * Restoring assertion mode for models and clean-up * Use `Seq.is_empty` from `stdcompat` * Cleanup and a bit of documentation * Promote tests * Linter * Update src/lib/structures/modelMap.ml Co-authored-by: Stevendeo * Update src/lib/util/util.mli Co-authored-by: Stevendeo * Update src/lib/reasoners/uf.ml Co-authored-by: Stevendeo * Update src/lib/reasoners/uf.ml Co-authored-by: Stevendeo * Review changes * Unused argument in the test * Promote tests * Models for functions returning records The previous implementation of `compute_concrete_model` doesn't support properly model generation for functions returning records. This is a quick fix. * Improve the type of `ModelMap.Value` The previous type was not sufficient to represent all the possible model values. In particular, we couldn't represent embedded records in other record and we cannot use complex types for indices and values of functional arrays. * Change review * rebase artefact * Use `Expr.t` to store model values Use `Expr.t` values instead of strings to store the value of the first-order model. Add a new function `to_term_const` in the signature of `Shostak`. Basically this function is the inverse function of `X.make` on the constant terms only. The function always returns a term `t` such that `Expr.is_const_term t` is `true`. Notice that we need this function during model generation. Indeed, even if the class of a semantic value in UF contains terms whose the `make` is constant according to `X.is_constant`, these terms aren't necessary constant according to `Expr.is_const_term`. For instance, the term `0 + 1` will become the semantic value `1` and we expect that `X.to_term_const` returns `Some 1`. Modify the definition of `Expr.is_const_term` (formerly named `const_term`). The previous definition considered that the application of constructor of an ADT to constant terms isn't a constant term. The same went for record definitions. Now, there are constant too. We have to check that this modification is correct for the Notice that we keep the old definion `const_term` in the module `Expr` but we don't expose it anymore. Indeed, this function is used to detect constants in the smart constructor of the let bindings because the definition of the depth of formulae have been tweaked to prevent regressions. Modifying this function could be dangereous. * Poetry * Hide the caches in the closure of `compute_concrete_model` * Fix `to_const_term` in BV theory * Documentation in UF and fix BV symbols Currently, we produce casesplits for bitvectors in order to generate models but we cannot reasoning with `BVand`, `BVxor` and `BVor`. It means we cannot add these symbols as interpreted symbols of the theory BV (see the function `Bitv.is_mine_symbol`) but these symbols can appear in the union-find environment. We have to ignore them while computing the model in UF. * Documentation of the type sy * documentation * restoring the constraint printer * Incorrect `is_internal` predicate We have to consider every symbol names starting with a dot or a `at` as an internal symbols. For instance the CDCL SAT solver produces internal names prefixed by `.PROXY__`. * Simpler `to_const_term` in BV theory We don't need to consider the case where a constant semantic value would be a concatenation of constant simple terms. Now the canonizer eliminate this case completely. * rename `terms_values` to `term_values` * rebase artefact in models.ml * Use Dolmen to quote identifiers * Rename `is_const_term` to `is_model_term` Variables aren't adequate model values. Now the predicate `is_model_term` returns `false` on them. * Remove brackets in `ArrayEx.select` * Clarify `X.is_constant` implementation * Simplify `model_repr_of_term` We don't need to inspect the class of a term to retrieve a constant expression in it. When we call `model_repr_of_term` during the model generation, we are sure that the representant of the class is a constant semantic value and `X.to_const_term` cannot fail. Otherwise, it's a bug! * Rename `to_const_term` to `to_model_term` As we rename `Expr.is_const_term` to `Expr.is_model_term`, I rename this function for consistency purposes. * Only use `Expr.t` to store model values As arrays can occur into model values, we need to use `Expr.t` to represent them. We cannot produce the appropriate model term with `Arrays.to_model_term` because we haven't semantic values for arrays. Instead we perform two passes on a pre-model generating with `X.to_model_term`. - The first pass collects all the values of arrays and generates a model term for each array. If the array was declared by the user, we add it to the model. - The second pass substitutes all the array identifiers in the pre-model by model terms we have generated in the first pass. * Remove warning message for models in presence of FPA symbols * bvor, bvand and bvxor aren't suspicious anymore * prefix model error * Poetry --------- Co-authored-by: Stevendeo --- alt-ergo-lib.opam | 1 + dune-project | 1 + src/bin/common/solving_loop.ml | 9 +- src/lib/dune | 2 +- src/lib/frontend/d_cnf.ml | 40 +- src/lib/frontend/frontend.ml | 2 +- src/lib/frontend/models.ml | 375 ++---------------- src/lib/frontend/models.mli | 13 +- src/lib/frontend/typechecker.ml | 2 +- src/lib/reasoners/ac.ml | 2 +- src/lib/reasoners/adt.ml | 5 +- src/lib/reasoners/arith.ml | 50 +-- src/lib/reasoners/arrays.ml | 20 +- src/lib/reasoners/bitv.ml | 40 +- src/lib/reasoners/enum.ml | 22 +- src/lib/reasoners/fun_sat.ml | 2 +- src/lib/reasoners/ite.ml | 2 +- src/lib/reasoners/records.ml | 33 +- src/lib/reasoners/satml_frontend.ml | 2 +- src/lib/reasoners/shostak.ml | 96 ++--- src/lib/reasoners/sig.mli | 25 +- src/lib/reasoners/uf.ml | 291 +++++++++----- src/lib/structures/errors.ml | 19 + src/lib/structures/errors.mli | 9 + src/lib/structures/expr.ml | 74 +++- src/lib/structures/expr.mli | 27 +- src/lib/structures/id.ml | 81 ++++ src/lib/structures/id.mli | 52 +++ src/lib/structures/modelMap.ml | 222 +++++++---- src/lib/structures/modelMap.mli | 44 +- src/lib/structures/symbols.ml | 47 +-- src/lib/structures/symbols.mli | 8 +- src/lib/util/lists.ml | 8 + src/lib/util/lists.mli | 4 + src/lib/util/util.ml | 1 - tests/cram.t/run.t | 2 +- tests/dune.inc | 63 +++ tests/issues/555.models.expected | 4 +- tests/issues/854/function.models.expected | 4 +- tests/issues/854/function.models.smt2 | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 4 +- tests/models/arith/arith11.optimize.expected | 2 +- tests/models/arith/arith5.optimize.expected | 2 +- tests/models/array/array1.models.expected | 4 +- .../array/embedded-array.models.expected | 8 + tests/models/array/embedded-array.models.smt2 | 10 + tests/models/bitv/extract.models.expected | 2 +- tests/models/records/record1.models.expected | 2 +- tests/models/records/record2.models.expected | 5 + tests/models/records/record2.models.smt2 | 8 + tests/models/records/record3.models.expected | 7 + tests/models/records/record3.models.smt2 | 12 + tests/models/uf/uf1.models.expected | 2 +- tests/models/uf/uf2.models.expected | 2 +- 55 files changed, 908 insertions(+), 870 deletions(-) create mode 100644 src/lib/structures/id.ml create mode 100644 src/lib/structures/id.mli create mode 100644 tests/models/array/embedded-array.models.expected create mode 100644 tests/models/array/embedded-array.models.smt2 create mode 100644 tests/models/records/record2.models.expected create mode 100644 tests/models/records/record2.models.smt2 create mode 100644 tests/models/records/record3.models.expected create mode 100644 tests/models/records/record3.models.smt2 diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index b4e86e7ca..89b163266 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -26,6 +26,7 @@ depends: [ "fmt" {>= "0.9.0"} "stdlib-shims" "ppx_blob" {>= "0.7.2"} + "ppx_deriving" "camlzip" {>= "1.07"} "odoc" {with-doc} "ppx_deriving" diff --git a/dune-project b/dune-project index cab2fcd37..2b6de3b71 100644 --- a/dune-project +++ b/dune-project @@ -86,6 +86,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (fmt (>= 0.9.0)) stdlib-shims (ppx_blob (>= 0.7.2)) + ppx_deriving (camlzip (>= 1.07)) (odoc :with-doc) ppx_deriving diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 746e17dcc..33e996d1c 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -181,7 +181,8 @@ let main () = begin let mdl = Model ((module SAT), partial_model) in if Options.(get_interpretation () && get_dump_models ()) then begin - FE.print_model (Options.Output.get_fmt_models ()) partial_model + Fmt.pf (Options.Output.get_fmt_models ()) "%a@." + FE.print_model partial_model end; Sat mdl end @@ -193,7 +194,8 @@ let main () = Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[Returned unknown reason = %a@]" Sat_solver_sig.pp_ae_unknown_reason_opt ur; - FE.print_model (Options.Output.get_fmt_models ()) partial_model + Fmt.pf (Options.Output.get_fmt_models ()) "%a@." + FE.print_model partial_model end; Unknown (Some mdl) end @@ -927,7 +929,8 @@ let main () = let () = match State.get partial_model_key st with | Some (Model ((module SAT), env)) -> let module FE = Frontend.Make (SAT) in - FE.print_model (Options.Output.get_fmt_regular ()) env + Fmt.pf (Options.Output.get_fmt_regular ()) "%a@." + FE.print_model env | None -> (* TODO: add the location of the statement. *) recoverable_error "No model produced." diff --git a/src/lib/dune b/src/lib/dune index 7bada9b61..1d59f6223 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -55,7 +55,7 @@ ; structures Commands Errors Explanation Fpa_rounding Parsed Profiling Satml_types Symbols - Expr Var Ty Typed Xliteral ModelMap Objective + Expr Var Ty Typed Xliteral ModelMap Id Objective ; util Emap Gc_debug Hconsing Hstring Heap Lists Loc MyUnix Numbers diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 1ba519ec4..c7545a8ee 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -39,7 +39,6 @@ module SM = Sy.Map module DE = DStd.Expr module DT = DE.Ty -module Id = DStd.Id module B = DStd.Builtin let unsupported msg = @@ -194,7 +193,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t let builtin_ty t = Dl.Typer.T.builtin_ty t let ty name ty = - Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@ fun env s -> builtin_ty @@ Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty @@ -214,10 +213,11 @@ let builtin_enum = function let add_cstrs map = List.fold_left (fun map ((c : DE.term_cst), _) -> let name = get_basename c.path in - Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> - builtin_term @@ - Dolmen_type.Base.term_app_cst - (module Dl.Typer.T) env c) map) + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } + (fun env _ -> + builtin_term @@ + Dolmen_type.Base.term_app_cst + (module Dl.Typer.T) env c) map) map cstrs in Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_; @@ -238,19 +238,19 @@ module Const = struct let bv2nat = with_cache (fun n -> let name = "bv2nat" in - Id.mk ~name ~builtin:(BV2Nat n) + DE.Id.mk ~name ~builtin:(BV2Nat n) (DStd.Path.global name) Ty.(arrow [bitv n] int)) let int2bv = with_cache (fun n -> let name = "int2bv" in - Id.mk ~name ~builtin:(Int2BV n) + DE.Id.mk ~name ~builtin:(Int2BV n) (DStd.Path.global name) Ty.(arrow [int] (bitv n))) let smt_round = with_cache (fun (n, m) -> let name = "ae.round" in - Id.mk + DE.Id.mk ~name ~builtin:(AERound (n, m)) (DStd.Path.global name) @@ -299,7 +299,7 @@ let bv_builtins env s = equivalent *) let inject_ae_to_smt2 id = match id with - | Id.{name = Simple n; _} -> + | DStd.Id.{name = Simple n; _} -> begin if String.equal n Fpa_rounding.fpa_rounding_mode_ae_type_name then (* Injecting the type name as the SMT2 Type name. *) @@ -322,7 +322,7 @@ let inject_ae_to_smt2 id = let ae_fpa_builtins = let (->.) args ret = (args, ret) in let dterm name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f @@ -330,7 +330,7 @@ let ae_fpa_builtins = let op ?(tyvars = []) name builtin (args, ret) = let ty = DT.pi tyvars @@ DT.arrow args ret in let cst = DE.Id.mk ~name ~builtin (DStd.Path.global name) ty in - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env _ -> builtin_term @@ Dolmen_type.Base.term_app_cst @@ -358,13 +358,13 @@ let ae_fpa_builtins = let float64 = float (DE.Term.int "53") (DE.Term.int "1074") in let float64d x = float64 (mode "NearestTiesToEven") x in let partial1 name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f in let partial2 name f = - Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@ fun env s -> builtin_term @@ Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f @@ -380,7 +380,7 @@ let ae_fpa_builtins = in let fpa_builtins = let open DT in - Id.Map.empty + DStd.Id.Map.empty |> add_rounding_modes @@ -454,7 +454,7 @@ let ae_fpa_builtins = fun env s -> let search_id id = try - Id.Map.find_exn id fpa_builtins env s + DStd.Id.Map.find_exn id fpa_builtins env s with Not_found -> `Not_found in match s with @@ -469,7 +469,7 @@ let smt_fpa_builtins = Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f in let other_builtins = - Id.Map.empty + DStd.Id.Map.empty |> add_rounding_modes in fun env s -> @@ -487,7 +487,7 @@ let smt_fpa_builtins = | exception Failure _ -> `Not_found end | Dl.Typer.T.Id id -> begin - match Id.Map.find_exn id other_builtins env s with + match DStd.Id.Map.find_exn id other_builtins env s with | e -> e | exception Not_found -> `Not_found end @@ -1876,7 +1876,7 @@ let make dloc_file acc stmt = let ns = DStd.Namespace.Decl in let name = Ty.fresh_hypothesis_name goal_sort in let decl: _ Typer_Pipe.stmt = { - id = Id.mk ns name; + id = DStd.Id.mk ns name; contents = `Hyp t; loc; attrs; implicit } in @@ -1893,7 +1893,7 @@ let make dloc_file acc stmt = assert false (* Axiom definitions *) - | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; + | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; implicit=_ } -> let dloc = DStd.Loc.(loc dloc_file stmt.loc) in let aloc = DStd.Loc.lexing_positions dloc in diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index c18df4c21..10808c3cf 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -520,5 +520,5 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct Sat_solver_sig.pp_ae_unknown_reason_opt ur; | Some model -> - Models.output_concrete_model ppf model + Models.pp ppf model end diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 7a962267a..457475278 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -28,53 +28,39 @@ (* *) (**************************************************************************) -open Format -open Options - -module X = Shostak.Combine - -module Ac = Shostak.Ac -module Ex = Explanation - module Sy = Symbols +module X = Shostak.Combine module E = Expr -module ME = Expr.Map -module SE = Expr.Set module MS = Map.Make(String) -module MX = Shostak.MXH let constraints = ref MS.empty type t = { propositional : Expr.Set.t; - constants : ModelMap.t; - functions : ModelMap.t; - arrays : ModelMap.t; - terms_values : (Shostak.Combine.r * string) Expr.Map.t + model : ModelMap.t; + term_values : Expr.t Expr.Map.t } let empty = { propositional = Expr.Set.empty; - constants = ModelMap.empty; - functions = ModelMap.empty; - arrays = ModelMap.empty; - terms_values = Expr.Map.empty; + model = ModelMap.empty ~suspicious:false; + term_values = Expr.Map.empty; } module Pp_smtlib_term = struct - + open Format let to_string_type t = asprintf "%a" Ty.pp_smtlib t let rec print fmt t = - let {E.f;xs;ty; _} = E.term_view t in + let {Expr.f;xs;ty; _} = Expr.term_view t in match f, xs with | Sy.Lit lit, xs -> begin match lit, xs with | Sy.L_eq, a::l -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(= %a%a)" print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l else @@ -82,13 +68,13 @@ module Pp_smtlib_term = struct print a (fun fmt -> List.iter (fprintf fmt " = %a" print)) l | Sy.L_neg_eq, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(not (= %a %a))" print a print b else fprintf fmt "(%a <> %a)" print a print b | Sy.L_neg_eq, a::l -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(distinct %a%a)" print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l else @@ -96,25 +82,25 @@ module Pp_smtlib_term = struct print a (fun fmt -> List.iter (fprintf fmt ", %a" print)) l | Sy.L_built Sy.LE, [a;b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(<= %a %a)" print a print b else fprintf fmt "(%a <= %a)" print a print b | Sy.L_built Sy.LT, [a;b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(< %a %a)" print a print b else fprintf fmt "(%a < %a)" print a print b | Sy.L_neg_built Sy.LE, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(> %a %a)" print a print b else fprintf fmt "(%a > %a)" print a print b | Sy.L_neg_built Sy.LT, [a; b] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(>= %a %a)" print a print b else fprintf fmt "(%a >= %a)" print a print b @@ -123,13 +109,13 @@ module Pp_smtlib_term = struct fprintf fmt "(not %a)" print a | Sy.L_built (Sy.IsConstr hs), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "((_ is %a) %a)" Hstring.print hs print e else fprintf fmt "(%a ? %a)" print e Hstring.print hs | Sy.L_neg_built (Sy.IsConstr hs), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e else fprintf fmt "not (%a ? %a)" print e Hstring.print hs @@ -143,13 +129,13 @@ module Pp_smtlib_term = struct end | Sy.Op Sy.Get, [e1; e2] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(select %a %a)" print e1 print e2 else fprintf fmt "%a[%a]" print e1 print e2 | Sy.Op Sy.Set, [e1; e2; e3] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(store %a %a %a)" print e1 print e2 @@ -164,7 +150,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a^{%d,%d}" print e i j | Sy.Op (Sy.Access field), [e] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%s %a)" (Hstring.view field) print e else fprintf fmt "%a.%s" print e (Hstring.view field) @@ -194,7 +180,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a(%a)" Hstring.print hs print_list l | Sy.Op _, [e1; e2] -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2 else fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2 @@ -231,7 +217,7 @@ module Pp_smtlib_term = struct fprintf fmt "%a" Sy.print f | _, _ -> - if get_output_smtlib () then + if Options.get_output_smtlib () then fprintf fmt "(%a %a)" Sy.print f print_list xs else fprintf fmt "%a(%a)" Sy.print f print_list xs @@ -245,221 +231,17 @@ module Pp_smtlib_term = struct end -module SmtlibCounterExample = struct - let fresh_counter = ref 0 - - let reset_counter () = fresh_counter := 0 - +module Why3CounterExample = struct let pp_term fmt t = if Options.get_output_format () == Why3 then Pp_smtlib_term.print fmt t else E.print fmt t - let pp_abstract_value_of_type ppf ty = - if not @@ Options.get_interpretation_use_underscore () then begin - Fmt.pf ppf "(as @@a%i %a)" !fresh_counter Ty.pp_smtlib ty; - incr fresh_counter - end - else - Fmt.pf ppf "_ " - - 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 - - let mk_records_constr records record_name - { Ty.name = _n; record_constr = cstr; lbs = lbs; _} = - let find_destrs destr destrs = - try let rep = MS.find destr destrs in - Some rep - with Not_found -> None - in - - let print_destr fmt (destrs,lbs) = - List.iter (fun (destr, ty_destr) -> - let destr = Hstring.view destr in - match find_destrs destr destrs with - | None -> - pp_abstract_value_of_type fmt ty_destr - | Some rep -> fprintf fmt "%s " rep - ) lbs - in - let destrs = - try MS.find (Sy.to_string record_name) records - with Not_found -> MS.empty - in - asprintf "%s %a" - (Hstring.view cstr) - print_destr (destrs,lbs) - - let add_record_constr records record_name - { Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values = - List.fold_left2(fun records (destr,_) (rep,_) -> - add_records_destr - records - record_name - (Hstring.view destr) - (asprintf "%a" pp_term 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 - match xs_values with - | [record_name,_] -> - (* HOTFIX: this fix is temporary. The current implementation of - model generation for records relies on string representants, - which means the printer for access symbols has to agree with - the name of the field in the type trecord. As the printer - [Symbols.print] will always output AE native format, this - doesn't agree when the output format is SMT-LIB. But the - printer of expression will output the right string if we don't - give the arguments of the field. - - Issue: https://github.com/OCamlPro/alt-ergo/issues/958 *) - let access = Fmt.str "%a" Expr.print (Expr.mk_term f [] ty) in - add_records_destr - records - (asprintf "%a" Expr.print record_name) - access - rep - | [] | _ -> records - end - | _ -> - match ty with - | Ty.Trecord r -> - add_record_constr records rep r xs_values - | _ -> records - - let print_fun_def fmt name args ty t = - let print_args fmt (ty,name) = - Format.fprintf fmt "(%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-fun %a (%a) %a@ %t)@]" - Sy.print name - (Printer.pp_list_space (print_args)) args - Ty.pp_smtlib ty - defined_value - - let output_constants_counterexample pp fmt records = - ModelMap.iter - (fun (f, xs_ty, ty) st -> - assert (xs_ty == []); - match ModelMap.V.elements st with - | [[], rep] -> - let rep = - match ty with - | Ty.Trecord r -> - let constr = mk_records_constr records f r in - dprintf "(%s)" constr - | _ -> dprintf "%a" pp rep - in - - print_fun_def fmt f [] ty rep - | _ -> assert false) - - 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 rep = - let representants = - ModelMap.V.fold (fun (xs_values,(rep,srep)) 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 - - let rec mk_ite_and xs tys = - match xs, tys with - | [],[] -> assert false - | [_,rs],[_ty,name] -> - dprintf "(= %s %a)" name pp rs - | (_,rs) :: l1, (_ty,name) :: l2 -> - dprintf "(and (= %s %a) %t)" - name - pp rs - (mk_ite_and l1 l2) - | _, _ -> assert false - in - - let mk_ite_or l = - let pp_or_list fmt xs_values = - fprintf fmt "%t" (mk_ite_and xs_values xs_ty_named) - in - match l with - | [] -> assert false - | [xs_values] -> mk_ite_and xs_values xs_ty_named - | xs_values :: l -> - dprintf "(or %t %a)" - (mk_ite_and xs_values xs_ty_named) - (Printer.pp_list_space pp_or_list) l - in - - let rec reps_aux reps = - match reps with - | [] -> dprintf "%a" pp_abstract_value_of_type ty - | [srep,xs_values_list] -> - if Options.get_interpretation_use_underscore () then - dprintf "(@[ite %t@ %a@ %t)@]" - (mk_ite_or xs_values_list) - pp srep - (reps_aux []) - else - dprintf "%a" pp srep - | (srep,xs_values_list) :: l -> - dprintf "(@[ite %t@ %a@ %t)@]" - (mk_ite_or xs_values_list) - pp srep - (reps_aux l) - in - if List.length representants = 1 then - dprintf "%a" pp (fst (List.hd representants)) - else - reps_aux representants - in - (* Only print declared (but not defined!) function symbols -- note - that we still need to *handle* other symbols without printing them - because they could be record accessors that must be added to the - `records` reference *) - match f with - | Sy.Name { defined = false; _ } -> - print_fun_def fmt f xs_ty_named ty rep - | _ -> () - ) fprofs; - !records - -end -(* of module SmtlibCounterExample *) - -module Why3CounterExample = struct - let output_constraints fmt prop_model = - let assertions = SE.fold (fun e acc -> - (dprintf "%t(assert %a)@ " acc SmtlibCounterExample.pp_term e) - ) prop_model (dprintf "") in + let assertions = Expr.Set.fold (fun e acc -> + (Format.dprintf "%t(assert %a)@ " acc pp_term e) + ) prop_model (Format.dprintf "") in Format.fprintf fmt "@ ; constraints@ "; MS.iter (fun _ (name,ty,args_ty) -> match args_ty with @@ -478,109 +260,8 @@ module Why3CounterExample = struct end (* of module Why3CounterExample *) -(* The [value_defn] type is a mini-language of the expressions that can occur in - constant values. *) -type value_defn = - | Store of value_defn * value_defn * value_defn - (* An array store: [(store array key value)] *) - | 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 - contain any uninterpreted terms. *) - | Abstract of string - (* An unique abstract value *) - -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 rec pp_value ppk ppf = function - | Store (a, k, v) -> - Format.fprintf ppf "(@[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 - | Abstract s -> Format.pp_print_string ppf s - -let pp_constant ppf (_sy, t) = - Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t - -let output_concrete_model fmt m = - SmtlibCounterExample.reset_counter (); - if ModelMap.(is_suspicious m.functions || is_suspicious m.constants - || is_suspicious m.arrays) then - Format.fprintf fmt "; This model is a best-effort. It includes symbols - for which model generation is known to be incomplete. @."; - - Format.fprintf fmt "@[("; +let pp ppf { model; propositional; _ } = if Options.get_model_type_constraints () then begin - Why3CounterExample.output_constraints fmt m.propositional + Why3CounterExample.output_constraints ppf propositional end; - - let values = Hashtbl.create 17 in - let find_or_add sy f = - try Hashtbl.find values sy - with Not_found -> - let value = f () in - Hashtbl.replace values sy value; - value - in - (* 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)) -> - assert (Lists.is_empty keys); - Hashtbl.add values f (value (value_r, value_s)) - ) st - ) m.constants; - - (* Add the arrays values, when applicable *) - ModelMap.iter (fun (f, xs_ty, ty) st -> - let root = - try Hashtbl.find values f - 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 - ) m.arrays; - - let pp_value = - pp_value (fun ppf (sy, ty) -> - let v = - find_or_add sy @@ fun () -> - (* NB: It is important that we call `pp_abstract_value_of_type` - immediately (not in a delayed fashion) so that we make sure that - the same abstract value will get printed each time. *) - Abstract ( - Fmt.to_to_string SmtlibCounterExample.pp_abstract_value_of_type ty) - in - pp_value pp_constant ppf v) - in - - let pp_x ppf xs = pp_value ppf (value xs) in - - (* Functions *) - let records = - SmtlibCounterExample.output_functions_counterexample - pp_x fmt MS.empty m.functions - in - - (* Constants *) - SmtlibCounterExample.output_constants_counterexample - pp_x fmt records m.constants; - - (* Arrays *) - (* SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *) - - Printer.print_fmt fmt "@]@,)" + ModelMap.pp ppf model diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index b83f19034..20c466cad 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -32,16 +32,11 @@ type t = { propositional : Expr.Set.t; - constants : ModelMap.t; - functions : ModelMap.t; - arrays : ModelMap.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. *) + model : ModelMap.t; + term_values : Expr.t Expr.Map.t + (** A map from terms to their values in the model. *) } val empty : t -val output_concrete_model : t Fmt.t -(** [output_concrete_model ppf mdl] prints the model [mdl] on - the formatter [ppf]. *) +val pp : t Fmt.t diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 673373f3a..8a5003fe8 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2165,7 +2165,7 @@ let axioms_of_rules loc name lf acc env = (fun acc f -> let name = Fmt.str "%s_%s" - (Symbols.fresh_internal_string ()) + (Id.Namespace.Internal.fresh ()) name in let td = {c = TAxiom(loc,name,Util.Default, f); annot = new_id () } in diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index dcdb35286..b5abbfdc8 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -325,7 +325,7 @@ module Make (X : Sig.X) = struct let module SX = Set.Make(struct type t=r let compare = X.hash_cmp end) in let exception Found of Expr.t in fun r distincts eq -> - if List.exists (fun (t,(_:r)) -> Expr.const_term t) eq then + if List.exists (fun (t,(_:r)) -> Expr.is_model_term t) eq then None else (*match X.ac_extract r with diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 54cd9a464..ba39cbb43 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -412,9 +412,8 @@ module Shostak (X : ALIEN) = struct "[ADTs.models] assign_value currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - let choose_adequate_model _ _ _ = + let to_model_term _r = Printer.print_err - "[ADTs.models] choose_adequate_model currently not implemented"; + "[ADTs.models] to_model_term currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - end diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 9fa3a8a2f..7aaf7f9bc 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -809,49 +809,11 @@ module Shostak cpt := Q.add Q.one (max_constant distincts !cpt); Some (term_of_cst (Q.to_string !cpt), true) - let pp_constant ppf r = + let to_model_term r = match P.is_const (embed r), X.type_info r with - | Some q, Ty.Tint -> - assert (Z.equal (Q.den q) Z.one); - let i = Q.num q in - if Z.sign i = -1 then - Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i) - else - Fmt.pf ppf "%a" Z.pp_print i - | Some q, Ty.Treal -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) - | _ -> assert false - - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.filter (fun (_, r) -> P.is_const (embed r) != None) l in - let r = - match l with - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - if (P.is_const (embed r) == None) then begin - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "no adequate model found for %a" X.print r; - assert false - end; - r - - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - in - r, Fmt.str "%a" pp_constant r - + | Some i, Ty.Tint -> + assert (Z.equal (Q.den i) Z.one); + Some (Expr.Ints.of_Z (Q.num i)) + | Some q, Ty.Treal -> Some (Expr.Reals.of_Q q) + | _ -> None end diff --git a/src/lib/reasoners/arrays.ml b/src/lib/reasoners/arrays.ml index 624dbd91e..3aa281702 100644 --- a/src/lib/reasoners/arrays.ml +++ b/src/lib/reasoners/arrays.ml @@ -60,28 +60,12 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value r _ eq = - if List.exists (fun (t,_) -> Expr.const_term t) eq then None + if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else match X.term_extract r with | Some _, true -> Some (Expr.fresh_name (X.type_info r), false) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_, r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - - | _ -> assert false - + let to_model_term _r = assert false end diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 73079f2b8..06f756905 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1543,34 +1543,14 @@ module Shostak(X : ALIEN) = struct let bv = String.make sz '0' in Some (E.bitv bv (Ty.Tbitv sz), true) - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Bitv" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.map (fun (t, r) -> (t, r, embed r)) l in - let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in - let r, a = - match l with - | [] -> - let a = embed r in - assert (is_cte_abstract a); - r, a - | (_, r, a) :: l -> - List.iter (fun (_, x, _) -> assert (X.equal x r)) l; - r, a - in - let s = - List.map (function - | { bv = Cte b; sz } -> - Z.format ("%0" ^ string_of_int sz ^ "b") b - | _ -> - (* Cannot happen because [a] must satisfy [is_cte_abstract] at this - point. *) - assert false - ) a - |> String.concat "" - in - r, "#b" ^ s - + let to_model_term r = + match embed r with + | [{ bv = Cte b; sz }] -> + let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in + Some (Expr.bitv s Ty.(Tbitv sz)) + | _ -> + (* A constant semantic value cannot be a concatenation of constant + simple term as the canonizer merges consecutive constant simple + terms. *) + None end diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml index e84153a85..1ca19e9f2 100644 --- a/src/lib/reasoners/enum.ml +++ b/src/lib/reasoners/enum.ml @@ -195,21 +195,9 @@ module Shostak (X : ALIEN) = struct Thus we don't need to guess new values here. *) None - let choose_adequate_model _ r l = - let l = - List.filter - (fun (_, r) -> match embed r with Cons _ -> true | _ -> false) l - in - let r = match l with - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - match embed r with Cons _ -> r | _ -> assert false - in - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - + let to_model_term r = + match embed r with + | Cons (hs, ty) -> + Some (E.mk_term Sy.(Op (Constr hs)) [] ty) + | Alien a -> X.to_model_term a end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 1ea043114..879645be9 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1877,7 +1877,7 @@ module Make (Th : Theory.S) = struct clear_instances_cache (); Th.reinit_cpt (); Symbols.clear_labels (); - Symbols.reset_id_builders (); + Id.Namespace.reinit (); Var.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); Ty.reinit_decls (); diff --git a/src/lib/reasoners/ite.ml b/src/lib/reasoners/ite.ml index a60151288..fdd6b5794 100644 --- a/src/lib/reasoners/ite.ml +++ b/src/lib/reasoners/ite.ml @@ -60,5 +60,5 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value _ _ _ = assert false - let choose_adequate_model _ _ _ = assert false + let to_model_term _r = assert false end diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index cd75c0ea8..8bbc3b333 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -30,6 +30,7 @@ module Hs = Hstring module E = Expr +module Sy = Symbols type 'a abstract = | Record of (Hs.t * 'a abstract) list * Ty.t @@ -414,7 +415,7 @@ module Shostak (X : ALIEN) = struct | Access _ -> None | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.const_term t) eq + if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else Some (Expr.fresh_name ty, false) @@ -426,20 +427,20 @@ module Shostak (X : ALIEN) = struct Some (s, false) (* false <-> not a case-split *) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_,r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - | _ -> assert false + let to_model_term = + let rec to_model_term r = + match r with + | Record (fields, ty) -> + (* We can ignore the names of fields as they are inlined in the + type [ty] of the record. *) + let l = + Lists.try_map (fun (_name, rf) -> to_model_term rf) fields + in + Option.bind l @@ fun l -> + Some (E.mk_term Sy.(Op Record) l ty) + | Other (a, _) -> + X.to_model_term a + | Access _ -> None + in fun r -> to_model_term (embed r) end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index e41546464..678d855e1 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1346,7 +1346,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); - Symbols.reset_id_builders (); + Id.Namespace.reinit (); Symbols.clear_labels (); Var.reinit_cnt (); Satml_types.Flat_Formula.reinit_cpt (); diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index fcac11341..e0724c2b8 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -270,6 +270,23 @@ struct | Ac _ -> None, false (* SYLVAIN : TODO *) | Term t -> Some t, true + let to_model_term r = + let res = + match r.v with + | Arith _ -> ARITH.to_model_term r + | Records _ -> RECORDS.to_model_term r + | Bitv _ -> BITV.to_model_term r + | Arrays _ -> ARRAYS.to_model_term r + | Enum _ -> ENUM.to_model_term r + | Adt _ -> ADT.to_model_term r + | Ite _ -> ITE.to_model_term r + | Term t when Expr.is_model_term t -> Some t + | Ac _ | Term _ -> None + in + Option.bind res @@ fun t -> + assert (Expr.is_model_term t); + Some t + let top () = term_embed Expr.vrai let bot () = term_embed Expr.faux @@ -369,7 +386,20 @@ struct | Enum t -> ENUM.is_constant t | Adt t -> ADT.is_constant t | Ite t -> ITE.is_constant t - | Ac _ | Term _ -> false + | Term t -> + begin + let Expr.{ f; xs; _ } = Expr.term_view t in + (* We don't use [Expr.is_model_term] here to ensure that [t] is a + constant term because most of model terms are represented by + semantic values of builtin theories. Constant terms not managed by + builtin theories have to be considered as constant semantic + values. In particular, this code enforces the invariant: + [e] is a model term ==> [X.make e] is a constant semantic value. *) + match f, xs with + | Symbols.(True | False | Void | Name _), [] -> true + | _ -> false + end + | Ac _ -> false let subst p v r = if equal p v then r @@ -646,8 +676,8 @@ struct end | Term t, ty -> (* case disable_adts() handled here *) - if Expr.const_term t || - List.exists (fun (t,_) -> Expr.const_term t) eq then None + if Expr.is_model_term t || + List.exists (fun (t,_) -> Expr.is_model_term t) eq then None else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *) | _ -> (* There is no model-generation support for the AC symbols yet. @@ -663,66 +693,6 @@ struct | None -> Format.asprintf "None" | Some(res, _is_cs) -> Format.asprintf "%a" Expr.print res); opt - - let choose_adequate_model t rep l = - let r, pprint = - match Expr.type_info t with - | Ty.Tint - | Ty.Treal -> ARITH.choose_adequate_model t rep l - | Ty.Tbitv _ -> BITV.choose_adequate_model t rep l - | Ty.Tsum _ -> ENUM.choose_adequate_model t rep l - | Ty.Tadt _ when not (Options.get_disable_adts()) -> - ADT.choose_adequate_model t rep l - | Ty.Trecord _ -> RECORDS.choose_adequate_model t rep l - | Ty.Tfarray _ -> ARRAYS.choose_adequate_model t rep l - | Ty.Tbool -> - (* case split is now supposed to be done for internal bools if - needed as well *) - assert (is_bool_const rep); - rep, Format.asprintf "%a" print rep - | _ -> - let acc = - List.fold_left - (fun acc (s, r) -> - if Expr.const_term s then - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - else - acc - ) None l - in - let r = - match acc with - | Some (_,r) -> r - | None -> - match term_extract rep with - | Some t, true when Expr.const_term t -> rep - | _ -> - let print_aux fmt (t,r) = - Format.fprintf fmt "> impossible case: %a -- %a@ " - Expr.print t - print r - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "@[What to choose for term %a with rep %a?\ - %a@]" - Expr.print t - print rep - (Printer.pp_list_no_space print_aux) l; - assert false - in - r, Format.asprintf "%a" print r (* it's a EUF constant *) - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "%a selected as a model for %a" - print r Expr.print t; - r, pprint - end and TARITH : Polynome.T diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index cc6075f4b..08d626d7c 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -128,11 +128,14 @@ module type SHOSTAK = sig [Some (t, false)], then there must be no context in which [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *) - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string - + val to_model_term : r -> Expr.t option + (** [to_model_term r] creates a model term if [r] is constant. + The function cannot fail if [r] is a constant (that is statisfied the + predicate [X.is_constant]). + + The returned value always satisfies the predicate + [Expr.is_model_term]. See its documentation for more details about + model terms. *) end module type X = sig @@ -191,8 +194,12 @@ module type X = sig val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string + val to_model_term : r -> Expr.t option + (** [to_model_term r] creates a model term if [r] is constant. + The function cannot fail if [r] is a constant (that is statisfied the + predicate [X.is_constant]). + + The returned value always satisfies the predicate + [Expr.is_model_term]. See its documentation for more details about + model terms. *) end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4fcfb6534..c22bcff25 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -32,7 +32,6 @@ module X = Shostak.Combine module Ac = Shostak.Ac module Ex = Explanation - module Sy = Symbols module E = Expr module ME = Expr.Map @@ -999,95 +998,32 @@ let assign_next env = Debug.check_invariants "assign_next" env; res, env -(**** Counter examples functions ****) -let is_a_good_model_value (x, _) = - match X.leaves x with - [] -> true - | [y] -> X.equal x y - | _ -> false - -let is_const_term (x, _) = - match X.term_extract x with - | Some t, _ -> - E.const_term t - | _ -> - (*cannot test for theories which don't implement term_extract*) - true - -let model_repr_of_term t env mrepr = - try ME.find t mrepr, mrepr - with Not_found -> - let mk = try ME.find t env.make with Not_found -> assert false in - let rep,_ = try MapX.find mk env.repr with Not_found -> assert false in - let cls = - try SE.elements (MapX.find rep env.classes) - with Not_found -> assert false - in - let cls = - try List.rev_map (fun s -> s, ME.find s env.make) cls - with Not_found -> assert false - in - let e = X.choose_adequate_model t rep cls in - e, ME.add t e mrepr - let save_cache () = LX.save_cache () let reinit_cache () = LX.reinit_cache () -let compute_concrete_model_of_val - env t ((fprofs, cprofs, carrays, mrepr) as acc) = - let { E.f; xs; ty; _ } = E.term_view t in - (* Keep record constructors because models.ml expects them to be there *) - if (X.is_solvable_theory_symbol f ty - && not (Shostak.Records.is_mine_symb f ty)) - || E.is_internal_name t || E.is_internal_skolem t - || E.equal t E.vrai || E.equal t E.faux - || Sy.is_internal f - then - acc - else - let xs, tys, mrepr = - List.fold_left - (fun (xs, tys, mrepr) x -> - let rep_x, mrepr = model_repr_of_term x env mrepr in - assert (is_const_term rep_x); - (x, rep_x)::xs, - (E.type_info x)::tys, - mrepr - ) ([],[], mrepr) (List.rev xs) - in - let rep, mrepr = model_repr_of_term t env mrepr in - assert (is_a_good_model_value rep); - assert (is_const_term rep); - match f, xs, ty with - | Sy.Op Sy.Set, _, _ -> acc - - | Sy.Op Sy.Get, [(_,(a,_));((_,(i,_)) as e)], _ -> - begin - match X.term_extract a with - | Some ta, true -> - let { E.f = f_ta; xs=xs_ta; _ } = E.term_view ta in - assert (xs_ta == []); - fprofs, - cprofs, - ModelMap.add (f_ta,[X.type_info i], ty) ([e], rep) carrays, - mrepr - - | _ -> assert false - end +(****************************************************************************) +(* Model generation functions *) +(****************************************************************************) - | _ -> - if tys == [] then - fprofs, ModelMap.add (f, tys, ty) (xs, rep) cprofs, carrays, - mrepr - else - ModelMap.add (f, tys, ty) (xs, rep) fprofs, cprofs, carrays, - mrepr +let model_repr_of_term t env mrepr = + try ME.find t mrepr, mrepr + with Not_found -> + let mk = try ME.find t env.make with Not_found -> assert false in + let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in + (* We call this function during the model generation only. At this time, + we are sure that class representatives are constant semantic values. *) + assert (X.is_constant rep); + match X.to_model_term rep with + | Some v -> v, ME.add t v mrepr + | None -> + (* [X.to_model_term] cannot fail on constant semantic values. *) + assert false -(* A map of expressions / terms, ordered by depth first, and then by - Expr.compare for expressions with same depth. This structure will +(* A map of expressions to terms, ordered by depth first, and then by + [Expr.compare] for expressions with same depth. This structure will be used to build a model, by starting with the inner/smaller terms first. The values associated to the key will be their make *) module MED = Map.Make @@ -1099,15 +1035,186 @@ module MED = Map.Make else Expr.compare a b end) -let terms env = ME.fold MED.add env.make MED.empty +let is_suspicious_name hs = + match Hstring.view hs with + | "@/" | "@%" | "@*" -> true + | _ -> false -let compute_concrete_model env = - MED.fold - (fun t _mk acc -> compute_concrete_model_of_val env t acc - ) (terms env) - (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty) +(* The model generation is known to be imcomplete for FPA theory. *) +let is_suspicious_symbol = function + | Symbols.Name { hs; _ } when is_suspicious_name hs -> true + | _ -> false -let extract_concrete_model ~prop_model env = - let functions, constants, arrays, mrepr = compute_concrete_model env in - { Models.propositional = prop_model; functions; constants; arrays; - terms_values = mrepr } +let terms env = + ME.fold + (fun t r ((terms, suspicious) as acc) -> + let Expr.{ f; _ } = Expr.term_view t in + match f with + | Name { defined = true; _ } -> + (* We don't store names defined by the user. *) + acc + | _ -> + let suspicious = is_suspicious_symbol f || suspicious in + MED.add t r terms, suspicious + ) env.make (MED.empty, false) + +(* Helper functions used by the caches during the computation of the model. *) +module Cache = struct + let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) = + match Hashtbl.find_opt arrays_cache t with + | Some values -> + Hashtbl.replace values i v + | None -> + let values = Hashtbl.create 17 in + Hashtbl.add values i v; + Hashtbl.add arrays_cache t values + + let get_abstract_for abstracts_cache env (t : Expr.t) = + let r, _ = find env t in + match Hashtbl.find_opt abstracts_cache r with + | Some abstract -> abstract + | None -> + let abstract = Expr.mk_abstract (Expr.type_info t) in + Hashtbl.add abstracts_cache r abstract; + abstract +end + +type cache = { + array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t) + Hashtbl.t; + (** Stores all the get accesses to arrays. *) + + abstracts: (r, Expr.t) Hashtbl.t; + (** Stores all the abstract values generated. This cache is necessary + to ensure we don't generate twice an abstract value for a given symbol. *) +} + +(* The environment of the union-find contains almost a first-order model. + There are two situations that require some computations to retrieve an + appropriate model value: + - As our array theory has no semantic values, there are no value + which represents an array in the union-find environment. Instead, the + union-find stores the collection of all the access to the array. This + function retrieves all these accesses in order to build an expression + which defines the approriate array. + - If the problem involves declared terms whose the type is abstract, + Alt-Ergo cannot produces a constant value for them. This function creates + a new abstract value in this case. *) +let compute_concrete_model_of_val cache = + let store_array_select = Cache.store_array_get cache.array_selects + and get_abstract_for = Cache.get_abstract_for cache.abstracts + in fun env t ((mdl, mrepr) as acc) -> + let { E.f; xs; ty; _ } = E.term_view t in + if X.is_solvable_theory_symbol f ty + || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t + || E.equal t E.vrai || E.equal t E.faux + then + (* These terms are built-in interpreted ones and we don't have + to produce a definition for them. *) + acc + else + begin + let arg_vals, arg_tys, mrepr = + List.fold_left + (fun (arg_vals, arg_tys, mrepr) arg -> + let rep_arg, mrepr = model_repr_of_term arg env mrepr in + rep_arg :: arg_vals, + (Expr.type_info arg) :: arg_tys, + mrepr + ) + ([], [], mrepr) (List.rev xs) + in + let ret_rep, mrepr = model_repr_of_term t env mrepr in + match f, arg_vals, ty with + | Sy.Name _, [], Ty.Tfarray _ -> + begin + match Hashtbl.find_opt cache.array_selects t with + | Some _ -> acc + | None -> + (* We have to add an abstract array in case there is no + constraint on its values. *) + Hashtbl.add cache.array_selects t (Hashtbl.create 17); + acc + end + + | Sy.Op Sy.Set, _, _ -> acc + + | Sy.Op Sy.Get, [a; i], _ -> + begin + store_array_select a i ret_rep; + acc + end + + | Sy.Name { hs = id; _ }, _, _ -> + let value = + match ty with + | Ty.Text _ -> + (* We cannot produce a concrete value as the type is abstract. + In this case, we produce an abstract value with the appropriate + type. *) + get_abstract_for env t + | _ -> ret_rep + in + ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr + + | _ -> + Printer.print_err + "Expect a uninterpreted term declared by the user, got %a" + E.print t; + assert false + end + +let extract_concrete_model cache = + let compute_concrete_model_of_val = compute_concrete_model_of_val cache in + let get_abstract_for = Cache.get_abstract_for cache.abstracts + in fun ~prop_model env -> + let terms, suspicious = terms env in + let model, mrepr = + MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc) + terms (ModelMap.empty ~suspicious, ME.empty) + in + let model = + Hashtbl.fold (fun t vals mdl -> + (* We produce a fresh identifiant for abstract value in order to + prevent any capture. *) + let abstract = get_abstract_for env t in + let ty = Expr.type_info t in + let arr_val = + Hashtbl.fold (fun i v arr_val -> + Expr.ArraysEx.store arr_val i v + ) vals abstract + in + let id = + let Expr.{ f; _ } = Expr.term_view t in + match f with + | Sy.Name { hs; _ } -> hs + | _ -> + (* We only store array declarations as keys in the cache + [array_selects]. *) + assert false + in + let mdl = + if not @@ Id.Namespace.Internal.is_id (Hstring.view id) then + ModelMap.add (id, [], ty) [] arr_val mdl + else + (* Internal identifiers can occur here if we need to generate + a model term for an embedded array but this array isn't itself + declared by the user. *) + mdl + in + (* We need to update the model [mdl] in order to substitute all the + occurrences of the array identifier [id] by an appropriate model + term. This cannot be performed while computing the model with + `compute_concrete_model_of_val` because we need to first iterate + on all the union-find environment to collect array values. *) + ModelMap.subst id arr_val mdl + ) cache.array_selects model + in + { Models.propositional = prop_model; model; term_values = mrepr } + +let extract_concrete_model ~prop_model = + let cache : cache = { + array_selects = Hashtbl.create 17; + abstracts = Hashtbl.create 17; + } + in fun env -> extract_concrete_model cache ~prop_model env diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index d0ec32d90..e2bab17d8 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -89,6 +89,10 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + type error = | Parser_error of string | Lexical_error of Loc.t * string @@ -98,6 +102,7 @@ type error = | Warning_as_error | Dolmen_error of (int * string) | Mode_error of Util.mode * mode_error + | Model_error of model_error exception Error of error @@ -252,6 +257,18 @@ let report_mode_error fmt = function | Forbidden_command s -> fprintf fmt "Command %s" s +let report_model_error ppf = function + | Subst_type_clash (id, ty1, ty2) -> + Fmt.pf ppf + "Cannot substitute the identifier %a of type %a by an expression of \ + type %a" + Id.pp id + Ty.pp_smtlib ty1 + Ty.pp_smtlib ty2 + + | Subst_not_model_term e -> + Fmt.pf ppf "The expression %a is not a model term" Expr.print e + let report fmt = function | Parser_error s -> Format.fprintf fmt "Parser Error: %s" s; @@ -277,3 +294,5 @@ let report fmt = function "Invalid action during %a mode: %a" Util.pp_mode mode report_mode_error merr; + | Model_error err -> + Fmt.pf fmt "Model Error: %a" report_model_error err diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index b0ca4ddc0..f9d8284e9 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -97,6 +97,11 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +(** Errors raised while using models. *) +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + (** All types of error that can be raised *) type error = | Parser_error of string (** Error used at parser loading *) @@ -107,9 +112,13 @@ type error = | Warning_as_error | Dolmen_error of (int * string) (** Error code + description raised by dolmen. *) + | Mode_error of Util.mode * mode_error (** Error used when performing actions forbidden in some modes. *) + | Model_error of model_error + (** Error raised while using models. *) + (** {2 Exceptions } *) exception Error of error diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 42fa54793..360106e03 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -313,6 +313,16 @@ module SmtPrinter = struct | Sy.Real q when Q.(equal q zero) -> true | _ -> false + let pp_rational ppf q = + if Z.equal (Q.den q) Z.one then + Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) + else if Q.sign q = -1 then + Fmt.pf ppf "(/ (- %a) %a)" + Z.pp_print (Z.abs (Q.num q)) + Z.pp_print (Q.den q) + else + Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + let pp_binder ppf (var, ty) = Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty @@ -415,6 +425,9 @@ module SmtPrinter = struct | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op + | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> + pp_rational ppf (Q.neg q) + | Sy.Op Minus, [e1; e2] when is_zero e1.f -> Fmt.pf ppf "@[<2>(- %a@])" pp e2 @@ -427,6 +440,10 @@ module SmtPrinter = struct | Sy.False, [] -> Fmt.pf ppf "false" + | Sy.Name { hs = n; _ }, [] + when Id.Namespace.Abstract.is_id (Hstring.view n) -> + Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty + | Sy.Name { hs = n; _ }, [] -> Symbols.pp_name ppf (Hstring.view n) | Sy.Name { hs = n; _ }, _ :: _ -> @@ -443,14 +460,7 @@ module SmtPrinter = struct Fmt.pf ppf "%a" Z.pp_print i | Sy.Real q, [] -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + pp_rational ppf q | Sy.Bitv (n, s), [] -> Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) @@ -671,6 +681,8 @@ let print_list_sep sep = let print_list ppf = print_list_sep "," ppf +let pp_smtlib = SmtPrinter.pp + let pp_binders ppf = if Options.get_output_smtlib () then SmtPrinter.pp_binders ppf @@ -895,6 +907,10 @@ let void = mk_term (Sy.Void) [] Ty.Tunit let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty +let mk_abstract ty = + let id = Id.Namespace.Abstract.fresh () |> Hstring.make in + mk_term (Sy.Name { hs = id; defined = false; kind = Other }) [] ty + let is_internal_name t = match t with | { f; xs = []; _ } -> Sy.is_fresh_internal_name f @@ -1015,14 +1031,23 @@ let mk_ite cond th el = if ty == Ty.Tbool then mk_if cond th el else mk_term (Sy.Op Sy.Tite) [cond; th; el] ty -let [@inline always] const_term e = - (* we use this function because depth is currently not correct to +let rec is_model_term e = + match e.f, e.xs with + | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs + | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true + | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero + | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero + | (True | False | Void | Name _ | Int _ | Real _ | Bitv _), [] -> true + | _ -> false + +let[@inline always] is_value_term e = + (* We use this function because depth is currently not correct to detect constants (not incremented in some situations due to - some regression) *) + some regression). *) match e.f with - | Sy.Form _ | Sy.Lit _ | Sy.Let -> false - | True | False | Void | Name _ | Int _ | Real _ | Bitv _ - | Op _ | Var _ | In _ | MapsTo _ -> + | Sy.Form _ | Sy.Lit _ | Sy.Let -> false + | True | False | Void | Name _ | Int _ | Real _ | Bitv _ | Op _ + | Var _ | In _ | MapsTo _ -> let res = (e.xs == []) in assert (res == (depth e <= 1)); res @@ -1368,7 +1393,7 @@ and mk_let_aux ({ let_v; let_e; in_e; _ } as x) = try let _, nb_occ = Var.Map.find let_v in_e.vars in if nb_occ = 1 && (let_e.pure (*1*) || Sy.equal (Sy.var let_v) in_e.f) || - const_term let_e then (* inline in these situations *) + is_value_term let_e then (* inline in these situations *) apply_subst_aux (Var.Map.singleton let_v let_e, Ty.esubst) in_e else let ty = type_info in_e in @@ -1697,7 +1722,7 @@ let skolemize { main = f; binders; sko_v; sko_vty; _ } = let mk_sym cpt s = Fmt.kstr - (fun str -> Sy.make_as_fresh_skolem str) + (fun str -> Sy.name (Id.Namespace.make_as_fresh_skolem str)) "%s%s!%d" s tyvars @@ -3112,3 +3137,20 @@ module BV = struct let bvsgt s t = bvslt t s let bvsge s t = bvsle t s end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx = struct + let select a i = + let rty = + match type_info a with + | Tfarray (_, rty) -> rty + | _ -> invalid_arg "Expr.ArraysEx.select" + in + mk_term Sy.(Op Get) [a; i] rty + + let store a i v = + mk_term Sy.(Op Set) [a; i; v] (type_info a) +end diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 3bc83c5c5..8ca71acbc 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -151,6 +151,10 @@ val print_list : Format.formatter -> t list -> unit val print_list_sep : string -> Format.formatter -> t list -> unit val print_triggers : Format.formatter -> trigger list -> unit +val pp_smtlib : t Fmt.t +(** [pp_smtlib ppf e] prints the expression [e] on the formatter + [ppf] using the SMT-LIB standard. *) + (** Comparison and hashing functions *) val compare : t -> t -> int @@ -198,6 +202,11 @@ val int : string -> t val real : string -> t val bitv : string -> Ty.t -> t val fresh_name : Ty.t -> t + +val mk_abstract : Ty.t -> t +(** [mk_abstract ty] creates an abstract model term of type [ty]. + This function is intended to be used only in models. *) + val pred : t -> t (** smart constructors for literals *) @@ -331,8 +340,13 @@ val print_th_elt : Format.formatter -> th_elt -> unit val is_pure : t -> bool -val const_term : t -> bool -(** return true iff the given argument is a term without arguments *) +val is_model_term : t -> bool +(** [is_model_term e] checks if the expression [e] is a model terms. + A model term can be: + - A record definition involving only model terms. + - A constructor application involving only model terms, + - A literal of a basic type (integer, real, boolean, unit or bitvector), + - A name. *) val save_cache: unit -> unit (** Saves the modules cache *) @@ -478,3 +492,12 @@ module BV : sig val bvlshr : t -> t -> t val bvashr : t -> t -> t end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx : sig + val select : t -> t -> t + val store : t -> t -> t -> t +end diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml new file mode 100644 index 000000000..e34de223f --- /dev/null +++ b/src/lib/structures/id.ml @@ -0,0 +1,81 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type t = Hstring.t [@@deriving ord] + +let equal = Hstring.equal + +let pp ppf id = + Dolmen.Smtlib2.Script.Poly.Print.id ppf + (Dolmen.Std.Name.simple (Hstring.view id)) + +let show id = Fmt.str "%a" pp id + +module Namespace = struct + module type S = sig + val fresh : ?base:string -> unit -> string + val is_id : string -> bool + end + + module Make (S : sig val prefix : string end) = struct + let make_as_fresh = (^) S.prefix + + let fresh, reset_fresh_cpt = + let cpt = ref 0 in + let fresh_string ?(base = "") () = + let res = make_as_fresh (base ^ (string_of_int !cpt)) in + incr cpt; + res + in + let reset_fresh_string_cpt () = + cpt := 0 + in + fresh_string, reset_fresh_string_cpt + + let is_id = Stdcompat.String.starts_with ~prefix:S.prefix + end + + module Internal = Make (struct let prefix = ".k" end) + + module Skolem = Make + (struct + (* garder le suffixe "__" car cela influence l'ordre *) + let prefix = ".?__" + end) + + let make_as_fresh_skolem = Skolem.make_as_fresh + + module Abstract = Make (struct let prefix = "@a" end) + + let reinit () = + Internal.reset_fresh_cpt (); + Skolem.reset_fresh_cpt (); + Abstract.reset_fresh_cpt () +end diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli new file mode 100644 index 000000000..0b2434918 --- /dev/null +++ b/src/lib/structures/id.mli @@ -0,0 +1,52 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type t = Hstring.t [@@deriving ord] + +val equal : t -> t -> bool +val show : t -> string +val pp : t Fmt.t + +module Namespace : sig + module type S = sig + val fresh : ?base:string -> unit -> string + val is_id : string -> bool + end + + module Internal : S + module Skolem : S + module Abstract : S + + val make_as_fresh_skolem : string -> string + + val reinit : unit -> unit + (** Resets the [fresh_internal_name], [fresh_skolem] and [fresh_abstract] + counters. *) +end diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index d41ea00d6..2b7fb096f 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -29,100 +29,152 @@ (**************************************************************************) module X = Shostak.Combine - module Sy = Symbols -module E = Expr +type sy = Id.t * Ty.t list * Ty.t [@@deriving ord] + +module Graph = struct + module M = Map.Make + (struct + type t = Expr.t list [@@deriving ord] + end) + + type t = Expr.t M.t + + let empty = M.empty + let add = M.add + let map = M.map + + (* A fiber of the function [f] over a value [v] is the set of all the values + in the domain of [f] whose the image by [f] is [v]. + + The function [inverse] of this module constructs a map of all the + non-empty fibers of the function represented by its graph. *) + module Fiber = struct + include Set.Make (struct + type t = Expr.t list [@@deriving ord] + end) + + let pp_arg ppf (ctr, arg) = + Fmt.pf ppf "(= arg_%i %a)" ctr Expr.pp_smtlib arg + + (* For an argument (x_1, ..., x_n) of the function represented by the graph, + prints the SMT-LIB formula: + (and (= arg_0 x_1)(= arg_1 x2) ... (= arg_n x_n)). + *) + let pp_args ppf = function + | [] -> () + | [arg] -> + pp_arg ppf (0, arg) + | args -> + Fmt.pf ppf "(and %a)" Fmt.(iter_bindings ~sep:sp List.iteri pp_arg) args + + (* For a fiber [x; y; z; ...] of the function represented by the graph, + prints the SMT-LIB formula: + (or + (and (= arg_0 x_0) (= arg_1 x_1) ...) + (and (= arg_0 y_0) (= arg_1 y_1) ...) + ...) + *) + let pp ppf fiber = + match cardinal fiber with + | 0 -> () + | 1 -> + let args = choose fiber in + Fmt.pf ppf "%a" pp_args args + | _ -> + Fmt.pf ppf "(or %a)" (Fmt.iter ~sep:Fmt.sp iter pp_args) fiber + end + + (* Compute all the fibers of the function represented by the graph. *) + let inverse graph = + M.fold (fun arg_vals ret_val acc -> + match Expr.Map.find_opt ret_val acc with + | Some fib -> + Expr.Map.add ret_val (Fiber.add arg_vals fib) acc + | None -> + Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc + ) graph Expr.Map.empty + + let pp_inverse ppf rel = + let rec aux ppf seq = + match seq () with + | Seq.Nil -> () + | Cons ((ret_val, _), seq) when Stdcompat.Seq.is_empty seq -> + Fmt.pf ppf "%a" Expr.pp_smtlib ret_val + | Cons ((ret_val, fiber), seq) -> + Fmt.pf ppf "(@[ite %a@ %a@ %a)@]" + Fiber.pp fiber + Expr.pp_smtlib ret_val + aux seq + in + aux ppf (Expr.Map.to_seq rel) +end module P = Map.Make (struct - type t = Sy.t * Ty.t list * Ty.t - - let (|||) c1 c2 = if c1 <> 0 then c1 else c2 - - let compare (a1, b1, c1) (a2, b2, c2) = - let l1_l2 = List.length b1 - List.length b2 in - let c = l1_l2 ||| (Ty.compare c1 c2) ||| (Sy.compare a1 a2) in - if c <> 0 then c - else - let c = ref 0 in - try - List.iter2 - (fun ty1 ty2 -> - let d = Ty.compare ty1 ty2 in - if d <> 0 then begin c := d; raise Exit end - ) b1 b2; - 0 - with - | Exit -> assert (!c <> 0); !c - | Invalid_argument _ -> assert false - end) + type t = sy -module V = Set.Make - (struct - type t = (E.t * (X.r * string)) list * (X.r * string) - let compare (l1, (v1,_)) (l2, (v2,_)) = - let c = X.hash_cmp v1 v2 in - if c <> 0 then c - else - let c = ref 0 in - try - List.iter2 - (fun (_,(x,_)) (_,(y,_)) -> - let d = X.hash_cmp x y in - if d <> 0 then begin c := d; raise Exit end - ) l1 l2; - !c - with - | Exit -> !c - | Invalid_argument _ -> List.length l1 - List.length l2 + let compare = compare_sy end) -type key = P.key -type elt = V.t - type t = { - values : V.t P.t; + values : Graph.t P.t; suspicious : bool; } -let is_suspicious_name hs = - match Hstring.view hs with - | "@/" | "@%" | "@*" -> true - | _ -> false - -(* The model generation is known to be imcomplete for FPA and Bitvector - theories. *) -let is_suspicious_symbol = function - | Sy.Op (Float | Abs_int | Abs_real | Sqrt_real - | Sqrt_real_default | Sqrt_real_excess - | Real_of_int | Int_floor | Int_ceil - | Max_int | Max_real | Min_int | Min_real - | Pow | Integer_log2 | Integer_round) -> true - | Sy.Name { hs; _ } when is_suspicious_name hs -> true - | _ -> false - -let add ((sy, _, _) as p) v { values; suspicious } = - let prof_p = try P.find p values with Not_found -> V.empty in - let values = - if V.mem v prof_p then values - else P.add p (V.add v prof_p) values - in - { values; suspicious = suspicious || is_suspicious_symbol sy } - -let iter f { values; _ } = - P.iter (fun ((sy, _, _) as key) value -> - match sy with - | Sy.Name { defined = true; _ } -> - (* We don't print constants defined by the user. *) - () - | _ -> f key value - ) values - -let[@inline always] is_suspicious { suspicious; _ } = suspicious - -let fold f { values; _ } acc = P.fold f values acc - -let empty = { values = P.empty; suspicious = false } - -let is_empty { values; _ } = P.is_empty values +let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = + if List.compare_lengths arg_tys arg_vals <> 0 then + Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \ + arguments" Id.pp id; + + let graph = try P.find sy values with Not_found -> Graph.empty in + let values = P.add sy (Graph.add arg_vals ret_val graph) values in + { values; suspicious } + +let empty ~suspicious = { values = P.empty; suspicious } + +let rec subst_in_term id e c = + let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in + match f, xs with + | Sy.Name { hs = id'; _ }, [] when Id.equal id id' -> + let ty = Expr.type_info e in + if not @@ Ty.equal ty ty' then + raise (Errors.Error (Model_error (Subst_type_clash (id, ty', ty)))); + e + | _ -> + begin + let xs = List.map (subst_in_term id e) xs in + Expr.mk_term f xs ty' + end + +let subst id e { values; suspicious } = + if not @@ Expr.is_model_term e then + raise (Errors.Error (Model_error (Subst_not_model_term e))); + let values = P.map (Graph.map (subst_in_term id e)) values in + { values; suspicious } + +let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) = + let pp_unused ppf unused = if unused then Fmt.pf ppf "_" else () in + Fmt.pf ppf "(%aarg_%i %a)" pp_unused unused arg_name Ty.pp_smtlib arg_ty + +let pp_define_fun ppf ((id, arg_tys, ret_ty), graph) = + let inverse_rel = Graph.inverse graph in + let is_constant = Expr.Map.cardinal inverse_rel = 1 in + let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in + Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]" + Id.pp id + Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys + Ty.pp_smtlib ret_ty + Graph.pp_inverse inverse_rel + +let pp ppf {values; suspicious} = + if suspicious then begin + Fmt.pf ppf "; This model is a best-effort. It includes symbols\n\ + ; for which model generation is known to be incomplete.@." + end; + if P.is_empty values then + Fmt.pf ppf "@[(@]@,)" + else + Fmt.pf ppf "@[(@,%a@]@,)" + (Fmt.iter_bindings ~sep:Fmt.cut P.iter pp_define_fun) values diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index c9584a88e..9d8e9f0ec 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -28,33 +28,31 @@ (* *) (**************************************************************************) -(** Maps of values for alt-ergo's models. - Elements are sorted by symbols/types (P) and accumulated as sets - of expressions matching the P.key type (V). -*) - -module P : Map.S with type key = - Symbols.t * Ty.t list * Ty.t - -module V : Set.S with type elt = - (Expr.t * (Shostak.Combine.r * string)) list * - (Shostak.Combine.r * string) - -type key = P.key -type elt = V.t +type sy = Id.t * Ty.t list * Ty.t +(** Typed symbol of function defined in the model. In order: + - The identifier of the symbol. + - The types of its arguments. + - The returned type. *) type t +(** Type of model. *) -val add : key -> V.elt -> t -> t - -val iter : (key -> elt -> unit) -> t -> unit +val add : sy -> Expr.t list -> Expr.t -> t -> t +(** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph + associated with the symbol [sy]. *) -val fold : (key -> elt -> 'acc -> 'acc) -> t -> 'acc -> 'acc +val empty : suspicious:bool -> t +(** An empty model. The [suspicious] flag is used to remember that this + model may be wrong as it involves symbols from theories for which the + model generation is known to be incomplete. *) -val empty : t +val subst : Id.t -> Expr.t -> t -> t +(** [subst id e mdl] substitutes all the occurrences of the identifier [id] + in the model [mdl] by the model term [e]. -val is_empty : t -> bool + @Raise Error if the expression [e] is not a model term or the type of + [e] doesn't agree with some occurrence of [id] in the model. *) -val is_suspicious : t -> bool -(* Determine if the model is suspicious as it contains symbols - of theories for which the model generation is not properly supported. *) +val pp : t Fmt.t +(** [pp ppf mdl] prints the model [mdl] on the formatter [ppf] using the + SMT-LIB format. *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index bcde80996..7946d4a3f 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,12 +79,11 @@ type bound_kind = Unbounded | VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) { kind : bound_kind; sort : Ty.t; is_open : bool; is_lower : bool } - type t = | True | False | Void - | Name of { hs : Hstring.t ; kind : name_kind ; defined : bool } + | Name of { hs : Id.t ; kind : name_kind ; defined : bool } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -454,49 +453,17 @@ let to_string sy = Fmt.str "%a" (AEPrinter.pp ~show_vars:true) sy -module type Id = sig - val fresh : ?base:string -> unit -> string - val reset_fresh_cpt : unit -> unit - val is_id : string -> bool - val make_as_fresh : string -> string -end - -module MakeId(S : sig val prefix : string end) : Id = struct - - let make_as_fresh = (^) S.prefix - - let fresh, reset_fresh_cpt = - let cpt = ref 0 in - let fresh_string ?(base = "") () = - incr cpt; - make_as_fresh (base ^ (string_of_int !cpt)) - in - let reset_fresh_string_cpt () = - cpt := 0 - in - fresh_string, reset_fresh_string_cpt +let fresh_internal_name () = name (Id.Namespace.Internal.fresh ()) - let is_id = Stdcompat.String.starts_with ~prefix:S.prefix -end - -module InternalId = MakeId(struct let prefix = ".k" end) -module SkolemId = MakeId(struct let prefix = ".?__" end) -(* garder le suffixe "__" car cela influence l'ordre *) - -let fresh_internal_string () = InternalId.fresh () -let fresh_internal_name () = name (fresh_internal_string ()) - -let fresh_skolem_string base = SkolemId.fresh ~base () +let fresh_skolem_string base = Id.Namespace.Skolem.fresh ~base () let fresh_skolem_name base = name (fresh_skolem_string base) -let make_as_fresh_skolem str = name (SkolemId.make_as_fresh str) - let is_fresh_internal_name = function - | Name { hs = hd; _ } -> InternalId.is_id (Hstring.view hd) + | Name { hs = hd; _ } -> Id.Namespace.Internal.is_id (Hstring.view hd) | _ -> false let is_fresh_skolem = function - | Name { hs = hd; _ } -> SkolemId.is_id (Hstring.view hd) + | Name { hs = hd; _ } -> Id.Namespace.Skolem.is_id (Hstring.view hd) | _ -> false let is_get f = equal f (Op Get) @@ -516,10 +483,6 @@ let label t = try Labels.find labels t with Not_found -> Hstring.empty let clear_labels () = Labels.clear labels -let reset_id_builders () = - InternalId.reset_fresh_cpt (); - SkolemId.reset_fresh_cpt () - module Set : Set.S with type elt = t = Set.Make (struct type t=s let compare=compare end) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 04df74d6e..e5d234ed6 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -83,7 +83,7 @@ type t = | True | False | Void - | Name of { hs : Hstring.t ; kind : name_kind ; defined : bool } + | Name of { hs : Id.t ; kind : name_kind ; defined : bool } | Int of Z.t | Real of Q.t | Bitv of int * Z.t @@ -137,14 +137,13 @@ val pp_smtlib_operator : operator Fmt.t (*val dummy : t*) -val fresh_internal_string : unit -> string val fresh_internal_name : unit -> t val is_fresh_internal_name : t -> bool val fresh_skolem_string : string -> string val fresh_skolem_name : string -> t -val make_as_fresh_skolem : string -> t val is_fresh_skolem : t -> bool + (** Resets to 0 the fresh symbol counter *) val is_get : t -> bool @@ -159,9 +158,6 @@ val string_of_bound : bound -> string val clear_labels : unit -> unit (** Empties the labels Hashtable *) -val reset_id_builders : unit -> unit -(** Resets the `fresh_internal_name` and `fresh_skolem` counters. *) - module Set : Set.S with type elt = t module Map : Map.S with type key = t diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml index f959ac1a1..10b9389ae 100644 --- a/src/lib/util/lists.ml +++ b/src/lib/util/lists.ml @@ -51,3 +51,11 @@ let apply_right f l = )([], true) l in (if same then l else List.rev res), same + +let rec try_map f l = + match l with + | [] -> Some [] + | x :: xs -> + Option.bind (f x) @@ fun y -> + Option.bind (try_map f xs) @@ fun ys -> + Some (y :: ys) diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli index 01cb2555b..8cf8eb0fe 100644 --- a/src/lib/util/lists.mli +++ b/src/lib/util/lists.mli @@ -47,3 +47,7 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool (** similar to function apply, but the elements of the list are couples **) + +val try_map : ('a -> 'b option) -> 'a list -> 'b list option +(** [try_map f l] is similar to [List.map f l] but the function [f] + may fail and the iterator shortcuts the computation. *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index a2d7048f6..07d1dc490 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -203,7 +203,6 @@ let print_list ~sep ~pp fmt l = Format.fprintf fmt "%a" pp e; List.iter (fun e -> Format.fprintf fmt "%s %a" sep pp e) l - let rec print_list_pp ~sep ~pp fmt = function | [] -> () | [x] -> pp fmt x diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index bf837bf48..1aa6dc1e5 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -10,9 +10,9 @@ appropriate here. unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) Now we will test some semantic triggers. diff --git a/tests/dune.inc b/tests/dune.inc index 196e9039c..26d82ad68 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -210019,6 +210019,27 @@ ; Auto-generated part begin (subdir models/array + (rule + (target embedded-array.models_dolmen.output) + (deps (:input embedded-array.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps embedded-array.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff embedded-array.models.expected embedded-array.models_dolmen.output))) (rule (target array1.models_dolmen.output) (deps (:input array1.models.smt2)) @@ -210443,6 +210464,48 @@ ; Auto-generated part begin (subdir models/records + (rule + (target record3.models_dolmen.output) + (deps (:input record3.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps record3.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff record3.models.expected record3.models_dolmen.output))) + (rule + (target record2.models_dolmen.output) + (deps (:input record2.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps record2.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff record2.models.expected record2.models_dolmen.output))) (rule (target record1.models_dolmen.output) (deps (:input record1.models.smt2)) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index ef323fb3e..086ba7ffb 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index ebc7421cb..bb0b49fe0 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) - (define-fun f ((arg_0 Int)) Int 0) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) + (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/function.models.smt2 b/tests/issues/854/function.models.smt2 index 65e42142b..57ef18bcd 100644 --- a/tests/issues/854/function.models.smt2 +++ b/tests/issues/854/function.models.smt2 @@ -5,7 +5,7 @@ (declare-fun intrefqtmk (Int) intref) (declare-fun a () Int) (declare-fun f (Int) Int) -(define-fun aqtunused ((x Int)) intref (intrefqtmk (f a))) +(define-fun aqtunused ((_x Int)) intref (intrefqtmk (f a))) (assert (= (aqtunused 0) (aqtunused 1))) (declare-fun a1 () Int) (assert (not (and (<= 5 a1) (<= a1 15)))) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index 8e20717fb..9198abbbf 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index 0168a993e..f18c7f58e 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((arg_0 Int)) intref (as @a0 intref)) - (define-fun another_mk ((arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected index b83837cc9..99f7450f0 100644 --- a/tests/models/arith/arith11.optimize.expected +++ b/tests/models/arith/arith11.optimize.expected @@ -1,9 +1,9 @@ unknown ( - (define-fun x () Real 2.0) (define-fun p1 () Bool false) (define-fun p2 () Bool true) + (define-fun x () Real 2.0) ) (objectives (x 2.0) diff --git a/tests/models/arith/arith5.optimize.expected b/tests/models/arith/arith5.optimize.expected index 68d4b0380..e886d1332 100644 --- a/tests/models/arith/arith5.optimize.expected +++ b/tests/models/arith/arith5.optimize.expected @@ -6,5 +6,5 @@ unknown (define-fun z () Real (/ (- 7) 9)) ) (objectives - (x (- (/ 1 18))) + (x (/ (- 1) 18)) ) \ No newline at end of file diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected index ef323fb3e..086ba7ffb 100644 --- a/tests/models/array/array1.models.expected +++ b/tests/models/array/array1.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected new file mode 100644 index 000000000..dd6a80ae9 --- /dev/null +++ b/tests/models/array/embedded-array.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun s () S (as @a0 S)) + (define-fun x () Pair + (pair (store (as @a1 (Array Int S)) 0 s) + (store (as @a1 (Array Int S)) 0 s))) +) diff --git a/tests/models/array/embedded-array.models.smt2 b/tests/models/array/embedded-array.models.smt2 new file mode 100644 index 000000000..fa76cb828 --- /dev/null +++ b/tests/models/array/embedded-array.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-sort S 0) +(declare-const s S) +(declare-datatype Pair ((pair (first (Array Int S)) (second (Array Int S))))) +(declare-const x Pair) +(assert (= (select (first x) 0) s)) +(assert (= (first x) (second x))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/extract.models.expected b/tests/models/bitv/extract.models.expected index 99bcb1175..16b1f5e3a 100644 --- a/tests/models/bitv/extract.models.expected +++ b/tests/models/bitv/extract.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun z () (_ BitVec 1) #b0) (define-fun a () (_ BitVec 2) #b11) (define-fun b () (_ BitVec 3) #b111) (define-fun c () (_ BitVec 6) #b111011) + (define-fun z () (_ BitVec 1) #b0) ) diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected index c8d49e171..da5e88f8f 100644 --- a/tests/models/records/record1.models.expected +++ b/tests/models/records/record1.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun a () Pair (pair 5 (as @a0 Int))) + (define-fun a () Pair (pair 5 0)) ) diff --git a/tests/models/records/record2.models.expected b/tests/models/records/record2.models.expected new file mode 100644 index 000000000..d95838e69 --- /dev/null +++ b/tests/models/records/record2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) +) diff --git a/tests/models/records/record2.models.smt2 b/tests/models/records/record2.models.smt2 new file mode 100644 index 000000000..1e4238645 --- /dev/null +++ b/tests/models/records/record2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(assert (= (first (f 0)) 5)) +(check-sat) +(get-model) diff --git a/tests/models/records/record3.models.expected b/tests/models/records/record3.models.expected new file mode 100644 index 000000000..b478bf755 --- /dev/null +++ b/tests/models/records/record3.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) + (define-fun x () Int 0) + (define-fun y () Int 5) +) diff --git a/tests/models/records/record3.models.smt2 b/tests/models/records/record3.models.smt2 new file mode 100644 index 000000000..cc32e9e5b --- /dev/null +++ b/tests/models/records/record3.models.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(declare-const x Int) +(declare-const y Int) +(assert (= (first (f x)) 5)) +(assert (= (first (f 0)) y)) +(assert (= x 0)) +(check-sat) +(get-model) diff --git a/tests/models/uf/uf1.models.expected b/tests/models/uf/uf1.models.expected index b3bca4e8f..2891baf56 100644 --- a/tests/models/uf/uf1.models.expected +++ b/tests/models/uf/uf1.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((arg_0 Int)) Int 0) + (define-fun f ((_arg_0 Int)) Int 0) (define-fun a () Int 0) (define-fun b () Int 0) ) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected index 3c1182254..ce06fd333 100644 --- a/tests/models/uf/uf2.models.expected +++ b/tests/models/uf/uf2.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 2 0)) + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 2)) 0 2)) (define-fun a () Int 0) (define-fun b () Int (- 2)) )