Complete model #1019

@A

This PR fixes the issue OCamlPro#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 OCamlPro#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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Complete model #1019

Complete model #1019

Commits on Jan 17, 2024