Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 <de.oliveira.steven@gmail.com> * Update src/lib/util/util.mli Co-authored-by: Stevendeo <de.oliveira.steven@gmail.com> * Update src/lib/reasoners/uf.ml Co-authored-by: Stevendeo <de.oliveira.steven@gmail.com> * Update src/lib/reasoners/uf.ml Co-authored-by: Stevendeo <de.oliveira.steven@gmail.com> * 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 <de.oliveira.steven@gmail.com>
- Loading branch information
