mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
master
4 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Basile Clément
|
e7fc6642e8 |
cleanup: Use proper namespacing for names (#1028)
This introduces proper namespacing for variable names instead of relying on string prefixes. In order to disturb the ordering as little as possible, names are pre-mangled using their namespace (e.g. "x" in the `Internal` namespace is stored as ".!x") and further operations (hashing, comparison, etc.) are performed on the mangled names. |
||
Pierrot
|
373f90351a |
Complete model (#1019)
* Move typed symbols from ModelMap to Id * Generate complete model This PR fixes the issue #778. The suggested solution by this PR is as follows: - Collect user-declared symbols in `D_cnf`; - As the function `make` of the module `D_cnf` returns a list of commands, we add a new command `Decl` in `Frontend` to declare symbols; - The declared symbols are given to the SAT solver through a new function `declaration` in `sat_solver_sig`. - These symbols are collected in vectors and we keep indexes in another PR in order to manage properly the push/pop mechanism. - Finally the declared symbols are given to `Uf` and we create the empty model with them. Another annoying point comes from the current datastructure used in `ModelMap`. The type of `ModelMap` saves model values in the form of graphs. A graph is a finite set of constraints but there is no appropriate representation for the graph without constraints. Let's imagine we have the input: ```smt2 (set-option :produce-models true) (set-logic ALL) (declare-fun (Int) Int) (check-sat) (get-model) ``` We expect an output as follows: ```smt2 ( (define-fun f (_x Int) (@a as Int)) ) ``` But `Graph.empty` cannot hold the abstract value `@a`. A naive solution consists in using an ADT: ```ocaml type graph = | Empty of Id.typed | G of Graph.t ``` But we'll add an extra indirection. Probably the best solution would be to use a custom datastructure instead of a map to store the constraints. In this PR, we detect in `ModelMap.add` if the only constraint in the graph is of the form `something -> abstract value`. In this case we remove this constraint. This solution isn't perfect as explained in issue #1018. The biggest drawback of this solution is the fact we have to declare symbols in the SAT API, otherwise models returned by `get_model` could be incomplete. * Move comment * Remove useless option * Remove useless DeclSet module * We aren't in C++ :) * Split the test * Use a stack of the stdlib for `declare_ids` * Use a stack of the stdlib for declared symbols in SatML * Use an ADT to discriminate free graph and constant graph * Avoid list concatenation * Add a new error in case of stack underflow * Don't perform substitution into free graphes |
||
|
Pierrot
|
f451ee0d17 |
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> |
||
|
Pierrot
|
61b5b3e41b |
Use a separated counter for abstract value (#835)
* Use a separated counter for abstract value Use a separated counter in `Models` to produce fresh names for abstract values in models. This fix is temporary as we plan to refactor the model generation in another PR. A better design consists in producing fresh names while computing the model. * Increase the counter * Promote tests I also add another tests to check if the counter increases properly. |