Refactoring models representation

[Halbaroth]

This PR changes the way Alt-Ergo stores models.

Before the PR, Alt-Ergo didn't produce a printable model in memory but performed some basic computations in the model printers.

Now, Alt-Ergo will produce in memory a printable model. The PR mostly consists in moving some codes from Models.ml to ModelMap.ml or Uf.ml.

• All the require computation is now done in the output_concrete_model of the union-find module (included the computation for records).
• All the printings stuff are in ModelMap.ml.
• We use Expr.t to store model values.
• The only reason I kept Models.ml is because we are the printer of constraint model here. This will be remove later.

Besides, as I notice, the symbols we define in models are all Sy.Name. Thus I create an new module to manage identifiers Id.ml and I store identifiers instead of symbols in models.

[bclement-ocp]

This PR feels like it stops halfway through: from reading the PR description I thought that we would be building a structured representation of the model in memory prior to printing, but we actually build a fairly shallow map where most things are strings. I think we should go all the way and keep the structured representation throughout, rather than build (and intern!) intermediate strings that are only used for printing; although there are maybe blockers to that I don't immediately see — thoughts?

Besides, as I notice, the symbols we define in models are all Sy.Name. Thus I create an new module to manage identifiers Id.ml and I store identifiers instead of symbols in models.

I am not entirely convinced this is a good idea — I am not opposed to it but we may want to include things that are not Sy.Name in the models at some point (namely, values for partially interpreted functions such as division by zero) where we may regret this change.

(Unrelated thought: at some point we should probably use the Id module from Dolmen to represent identifiers as well)

[bclement-ocp]

Why did this model change?

[bclement-ocp]

Note that after #886 model generation should only be incomplete when the FPA prelude is disabled — which I don't think is a configuration we want to support.

[Halbaroth]

For this one, it seems the test is running without enabling the fpa theory:

  (rule
   (target test_float2.models_tableaux.output)
   (deps (:input test_float2.models.smt2))
   (package alt-ergo)
   (action
    (chdir %{workspace_root}
     (with-stdout-to %{target}
      (ignore-stderr
       (with-accepted-exit-codes 0
        (run %{bin:alt-ergo}
             --timelimit=2
             --enable-assertions
             --output=smtlib2
             --frontend dolmen
             --sat-solver Tableaux
             %{input})))))))

[bclement-ocp]

My point is that we don't inspect the preludes for the "known to be incomplete" message and that I think we should never print it for the float function (rather than always print it), because we expect users to use them with the preludes (or to know what they are doing).

(BTW the fact that we reply "unknown" and not "sat" is also an indication that the model might be incomplete)

[Halbaroth]

I don't understand your point. I don't know if I'm supposed to print something if the user tries to produce models in presence of FPA symbols without loading the FPA theory. I guess we should print something because users can forget flags.

[bclement-ocp]

My point is that it is fine to not print anything since replying "unknown" is already saying that the model may be incomplete. At least we should remove this when #917 is taken care of.

[bclement-ocp]

After #886 model generation for bv2nat and int2bv should be complete.

[bclement-ocp]

I am not sure how to link the types in the tuple to the description "typed symbol of function". I believe this is: (symbol, args_ty, ret_ty) tuples where symbol is the function name, args_ty the type of arguments, ret_ty the return type?

[Halbaroth]

I add a documentation to explain the meaning of its fields.

[bclement-ocp]

The corresponding code that expects the record constructors to be there in models.ml seems to have been removed, was it intentional?

[Halbaroth]

Uhm I'm not sure. The function is_forbidden_symbol is used to filter the symbols on which we will iterate during the model generation. I think the comment means we have to keep Access symbol, even if this symbol is interpreted by the theory of records, otherwise we cannot construct the model value for this theory.

[bclement-ocp]

I wrote this comment. It refers to the fact that in we (used to) need to preserve the record constructors for check_records et al in models.ml, but those functions have been removed. This means that either some stuff will no longer be working, or the new code in uf.ml is meant to replace those functions and we don't need to keep the record constructors here anymore (probably the latter).

[Halbaroth]

This comment isn't relevant anymore as we don't need to fold on all the terms in the union-find to produce model values for record symbols.

[bclement-ocp]

Is there a reason why the caches are stored in global variables? It would be cleaner (and thread-safe) to have a type that bundles the hash tables and is passed to compute_concrete_model_of_val.

[Halbaroth]

No reason, I will create the cache in compute_concrete_model directly.

[Halbaroth]

I put caches in the closure of the function extract_concrete_model.

[bclement-ocp]

This is not true. The result of the set operator can be equal to a user-defined array, as in #929 (in fact this may or may not be the source of #929)

[Halbaroth]

My comment was misleading. In fact Set symbols occur here by accident because X.is_my_symbol isn't the appropriate function to filter terms here. I just removed the comment and I'll do another PR in which a create a better predicate for this use case.

[bclement-ocp]

After #886, BV2Nat, Int2BV and Pow should no longer be treated as suspicious. Further, Float, Abs_int, Abs_real, Sqrt_real_default, Sqrt_real_excess, Real_of_int, Int_floor, Int_ceil, Max_int, Max_real, Min_int, Min_real, Integer_log2 and Integer_round are now only suspicious if the FPA prelude is not loaded.

This is because we now propagate their arguments during model generation, which should prevent us from generating models with invalid values for these functions.

[Halbaroth]

This PR feels like it stops halfway through: from reading the PR description I thought that we would be building a structured representation of the model in memory prior to printing, but we actually build a fairly shallow map where most things are strings. I think we should go all the way and keep the structured representation throughout, rather than build (and intern!) intermediate strings that are only used for printing; although there are maybe blockers to that I don't immediately see — thoughts?

As I explained in the description of this PR, the purpose of it is to solve the issue #833. Actually, this PR comes from a first commit I did in a old PR I've never pushed because we had to merge OptimAE first. I keep it as simple as possible because I want to merge it before #921.

In a next PR, I plan to produce models with the following ADT:

  type simple =
    | Int of Z.t
    | Real of Q.t
    | Bool of bool
    | Constructor of string

  type array =
    | AbstractArray of Id.t * Ty.t * Ty.t
    | Store of array * t * t

  and t =
    | Abstract of sy
    | Constant of simple
    | Array of array
    | Record of string * t list

This should be sufficient to perform evaluation of expression on the model, and so to perform checking models.

Actually, I'm not really happy of the next commits of my old PR. The situation is complicated because we have a conflict between two designs:

• First, the semantic value type is abstract, which means we cannot using directly the semantic values to get the model values because we have no access to their recursive structures in the uf module.
  The case of records is particularly eloquent here. Generating the model value in shostak would be so easy. You just need to write a recursive function. This is what I did in my old PR. It works very fine with all the current theories but arrays...

• Second, arrays has no semantic value. In other words, we cannot retrieve directly the model value from the semantic values by a simple recursive call in shostak. Currently, we explore all the union-find in uf and retrieve the mode value by catching all the get expressions and accumulating values in caches.

There is another annoying issue. The current function choose_adequate_model needs the class of the value for which we want a model value. For recursive values, as records or ADT, we will need more as we will perform recursive call. So the new choose_adequate_model requires the state of the union-find.... which means the best place to perform this computation is uf as it is actually? I don't know, may be we should create semantic values for arrays?

I fixed the issue you noticed with records and add some tests.

[Halbaroth]

I am not entirely convinced this is a good idea — I am not opposed to it but we may want to include things that are not Sy.Name in the models at some point (namely, values for partially interpreted functions such as division by zero) where we may regret this change.

If we need some other symbols in the futur, we can create a new type for it in ModelMap. A lot of the symbols of Symbols are fully interpreted and shouldn't appear in the signature of model values.

[bclement-ocp]

I don't understand why these changes are needed to fix #833. #833 is about when we decide to print the model or not. This PR doesn't change that, it changes the way we store the model prior to printing it. Besides, the offending call to Options.get_interpretation that was the source of #833 is no longer present in output_concrete_model, so to me it looks like #833 is already fixed.

Anyways, arrays cannot have (meaningful) semantic values because the theory of arrays cannot have a Shostak solver, so I think we are stuck with a few contorsions for arrays specifically.

That doesn't mean we have to do the same contorsions for records. In fact, for Shostak theories we can (and probably should) use semantic values, as you suggest here and we also discussed a couple months ago. I don't think that the type of semantic values being abstract is a big issue; we just need to figure out the proper API to expose from the Shostak module.

I think that the best way might be to expose:

• children : r -> r list that returns the list of direct alien children of a semantic value
• pp_model : r Fmt.t -> r Fmt.t that prints a semantic value, using the first argument for its children

This should be enough for the union-find part to do its job. In fact, since model generation is done through the case split mechanism (case_split ~for_model:true is first called before extracting the model), we may only need pp_model?

This way, we can check with X.is_a_leaf -- if it returns true, this is an uninterpreted term (or AC symbol) and we can either print the associated abstract constant or (if it's an array) the structure reconstructed from UF. And we could get rid of most of the strings laying around…

(As an aside, I am not sure I understand the issue with choose_adequate_model and recursion. At the point we reach choose_adequate_model all values should be (conceptually) ground and have been assigned by the previous calls to assign_value. In fact, I think that arrays (and records, in the current implementation) are the only ones that truly need the equivalence class in choose_adequate_model — in my understanding any other theory needing this equivalence class is a symptom of a bug or a design issue.)

[bclement-ocp]

You changed the name from Abstract to AbstractArray but my question remains: what is the difference between Abstract (n, tys, ty) and Array (AbstractArray (n, tys, ty))? I feel like just having Store of t * t * t should be enough here and would avoid this possible confusion.

[Halbaroth]

Not relevant anymore.

[bclement-ocp]

My point is that we don't inspect the preludes for the "known to be incomplete" message and that I think we should never print it for the float function (rather than always print it), because we expect users to use them with the preludes (or to know what they are doing).

(BTW the fact that we reply "unknown" and not "sat" is also an indication that the model might be incomplete)

[Halbaroth]

So I close this PR?

[bclement-ocp]

I think this PR does some things right (even fixes some bugs!), even though it doesn't seem needed to fix #833. In particular, having a structured representation of models is useful (notably because for some theories such as arrays the solver doesn't really store the information in the appropriate way in the first place we we noted), even if we may want to change the way that representation is built in the future.

That said, if it is the first in a sequence of PRs that you are no longer happy with, maybe we should first take some time to brainstorm the API we want to have (my gut feeling is that it should be centered around canonical semantic values, not symbols, associated with an auxiliary mapping for uninterpreted terms that don't have ground semantic values, i.e. arrays, functions) to make sure we are going towards the direction we want and one that fixes the design bugs we can encounter with the current implementation.

[Halbaroth]

I update this PR to use Expr.t instead of strings in order to store model values. I also add a new function to_const_term in sig.mli. This function returns a constant interpreted term from a constant semantic value. Please refer to the commit message of caae55f for more details.

[bclement-ocp]

It looks like there are still some issues with the ways arrays and abstract types are printed.

See for instance:

(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)

This prints:

unknown
(
  (define-fun s () S (as @a0 S))
  (define-fun x () Pair (pair .k4 .k4))
  (define-fun .k4 () (Array Int S) (store (as @a1 (Array Int S)) 0 s))
)

but the .k4 symbol should not appear in the model as it is an internal name (and only symbols defined by the user should appear in models). The expected output should be along the lines of:

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)))
)

We probably need one last substitution step of fresh array and abstract constants.

[bclement-ocp]

Nit: this should be term_values.

[bclement-ocp]

Not sure what this means?

[Halbaroth]

I guess it's a rebase artefact. It was used to delimit a module that doesn't exist anymore.

[bclement-ocp]

There should be a comment here explaining why this is not Expr.is_const_term (because other constants are semantic values).

[Halbaroth]

In fact, we could use Expr.is_const_term. I didn't use it because when I wrote this code, the predicate Expr.is_const_term should accept variables as we use it in the smart constructor of let bindings. I decided to use two predicates and we don't need to accept variables with Expr.is_const_term anymore. Still, it makes sense to write a specific code here. I add a comment to explain the situation.

[Halbaroth]

After simplifying the code model_repr_of_term in the union-find, we don't need to change X.is_constant anymore. But I think it would be better to have this invariant:

let mk, _ = X.make e in
if Expr.is_const_term e then assert (X.is_constant mk)

In other words, X.make sends model values to constant semantic values.

  let is_constant r =
    match r.v with
    | Arith t -> ARITH.is_constant t
    | Records t -> RECORDS.is_constant t
    | Bitv t -> BITV.is_constant t
    | Arrays t -> ARRAYS.is_constant t
    | Enum t -> ENUM.is_constant t
    | Adt t -> ADT.is_constant t
    | Ite t -> ITE.is_constant t
    | Term t ->
      begin
        let Expr.{ f; xs; _ } = Expr.term_view t in
        match f, xs with
        | Symbols.(True | False | Void | Name _), [] -> true
        | _ -> false
      end
    | Ac _ -> false

[bclement-ocp]

Should be documented here.

[Halbaroth]

I put the documentation in the second signature. I do a copy.

[bclement-ocp]

Not sure what this comment means; terms of most semantic values created by Alt-Ergo are not added to env.make. I'd have expected X.to_const_term rep to always be the correct answer (except for arrays). When is that not the case?

(My understanding is that cls is guaranteed to be either [] or [rep] and any other value would break Shostak invariants; is that correct?)

[Halbaroth]

I agree. I reproduced the old code here but we don't need to filter the class at all. This code seems to work:

    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
    match X.to_const_term rep with 
    | Some v -> v, ME.add t v mrepr
    | None -> assert false

If X.to_const_term rep fails to produce a model term here, it's a bug.

[bclement-ocp]

Suggested change

	| _ -> invalid_arg "[Expr.ArraysEx.select]"
	| _ -> invalid_arg "Expr.ArraysEx.select"

[bclement-ocp]

This has been merged, I believe (#955 )

[bclement-ocp]

Which ones? This problem only uses the builtin < and <= on reals, as far as I can tell.

[Halbaroth]

I didn't fix this issue because I don't understand your point as I explained here: #925 (comment)

[bclement-ocp]

I replied there (sorry, it got lost int the notifications somewhere) but I don't think this is related; arith7 doesn't look like it is using any suspicious symbols.

[bclement-ocp]

I thought this was replacing the pre-existing const_term function. Given that it's not, it is very confusing to have both const_term and is_const_term performing checks but returning different values. Can we maybe call this is_model_term or is_value_term instead?

[Halbaroth]

Sure

[bclement-ocp]

I'll let you choose whether to use internal identifers or abstract identifiers during model generation; I think on the other points we are ready to merge.

The review is outdated.