mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
373f90351a
* 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