Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Complete model #1019

Merged
merged 13 commits into from
Jan 18, 2024
Prev Previous commit
Next Next commit
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.
Halbaroth committed Jan 17, 2024
commit 959bf7b5a53e037d6bda8c8699cae94cd635eaa9
58 changes: 42 additions & 16 deletions src/lib/frontend/d_cnf.ml
Original file line number Diff line number Diff line change
@@ -53,6 +53,12 @@ module HT = Hashtbl.Make(
let hash = Fun.id
end)

module DeclSet = Set.Make
(struct
type t = Id.typed
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need to use the type here? Can we have multiple declarations with the same name but different types?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If this is because we need the type in Uf, this should be a map from identifiers to types rather than a set of typed identifiers.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually this doesn't seem to be used.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I forgot to remove it ;)

let compare = Id.compare_typed
end)

(** Helper function: returns the basename of a dolmen path, since in AE
the problems are contained in one-file (for now at least), the path is
irrelevant and only the basename matters *)
@@ -701,8 +707,15 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
end
in
Cache.store_sy tcst sy;
Cache.store_ty_vars id_ty;
(* Adding polymorphic types to the cache. *)
Cache.store_ty_vars id_ty
let arg_tys, ret_ty =
match DT.view id_ty with
| `Arrow (arg_tys, ret_ty) ->
List.map dty_to_ty arg_tys, dty_to_ty ret_ty
| _ -> [], dty_to_ty id_ty
in
(Hstring.make name, arg_tys, ret_ty)

(** Handles the definitions of a list of mutually recursive types.
- If one of the types is an ADT, the ADTs that have only one case are
@@ -2087,14 +2100,24 @@ let make dloc_file acc stmt =
assert false
) defs

| {contents = `Decls [td]; _ } ->
begin match td with
| `Type_decl (td, _def) -> mk_ty_decl td
| `Term_decl td -> mk_term_decl td
end;
acc
| {contents = `Decls [td]; loc; _ } ->
let decl = match td with
| `Type_decl (td, _def) ->
mk_ty_decl td;
None

| `Term_decl td ->
Some (mk_term_decl td)
in
begin match decl with
| Some d ->
let st_loc = dl_to_ael dloc_file loc in
C.{ st_decl = Decl d; st_loc } :: acc
| None ->
acc
end
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need to build an option to destruct it immediately:

Suggested change
let decl = match td with
| `Type_decl (td, _def) ->
mk_ty_decl td;
None
| `Term_decl td ->
Some (mk_term_decl td)
in
begin match decl with
| Some d ->
let st_loc = dl_to_ael dloc_file loc in
C.{ st_decl = Decl d; st_loc } :: acc
| None ->
acc
end
begin match td with
| `Type_decl (td, _def) ->
mk_ty_decl td;
acc
| `Term_decl td ->
let d = mk_term_decl td in
let st_loc = dl_to_ael dloc_file loc in
C.{ st_decl = Decl d; st_loc } :: acc
end


| {contents = `Decls dcl; _ } ->
| {contents = `Decls dcl; loc; _ } ->
let rec aux acc tdl =
(* for now, when acc has more than one element it is assumed that the
types are mutually recursive. Which is not necessarily the case.
@@ -2107,21 +2130,24 @@ let make dloc_file acc stmt =
| [otd] -> mk_ty_decl otd
| _ -> mk_mr_ty_decls (List.rev acc)
end;
mk_term_decl td;
aux [] tl
let st_loc = dl_to_ael dloc_file loc in
C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl

| `Type_decl (td, _def) :: tl ->
aux (td :: acc) tl

| [] ->
begin match acc with
| [] -> ()
| [otd] -> mk_ty_decl otd
| _ -> mk_mr_ty_decls (List.rev acc)
begin
let () =
match acc with
| [] -> ()
| [otd] -> mk_ty_decl otd
| _ -> mk_mr_ty_decls (List.rev acc)
in
[]
end
in
aux [] dcl;
acc
aux [] dcl @ acc
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: acc could be passed as a new 3rd argument to aux here (to return instead of [] in the final case) so that we avoid building a list just to concatenate it to another one.


| { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc

8 changes: 8 additions & 0 deletions src/lib/frontend/frontend.ml
Original file line number Diff line number Diff line change
@@ -302,6 +302,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
else Ex.empty

let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
ignore loc;
match env.res with
| `Sat | `Unknown ->
SAT.declare env.sat_env id
| `Unsat -> ()

let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
ignore loc;
Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
@@ -443,6 +450,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
try
match d.st_decl with
| Decl id -> check_if_over (internal_decl ~loc:d.st_loc id) env
| Push n -> check_if_over (internal_push ~loc:d.st_loc n) env
| Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
| Assume (n, f, mf) ->
2 changes: 1 addition & 1 deletion src/lib/frontend/models.ml
Original file line number Diff line number Diff line change
@@ -43,7 +43,7 @@ type t = {

let empty = {
propositional = Expr.Set.empty;
model = ModelMap.empty ~suspicious:false;
model = ModelMap.empty ~suspicious:false [];
term_values = Expr.Map.empty;
}

9 changes: 6 additions & 3 deletions src/lib/reasoners/ccx.ml
Original file line number Diff line number Diff line change
@@ -86,7 +86,10 @@ module type S = sig
Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances

val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
val extract_concrete_model :
prop_model:Expr.Set.t ->
declared_ids:Id.typed list ->
t -> Models.t

end

@@ -748,6 +751,6 @@ module Main : S = struct
in
Uf.term_repr env.uf t

let extract_concrete_model ~prop_model env =
Uf.extract_concrete_model ~prop_model env.uf
let extract_concrete_model ~prop_model ~declared_ids env =
Uf.extract_concrete_model ~prop_model ~declared_ids env.uf
end
5 changes: 4 additions & 1 deletion src/lib/reasoners/ccx.mli
Original file line number Diff line number Diff line change
@@ -77,7 +77,10 @@ module type S = sig
Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances

val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
val extract_concrete_model :
prop_model:Expr.Set.t ->
declared_ids:Id.typed list ->
t -> Models.t

end

14 changes: 13 additions & 1 deletion src/lib/reasoners/fun_sat.ml
Original file line number Diff line number Diff line change
@@ -177,6 +177,8 @@ module Make (Th : Theory.S) = struct
unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
last_saved_model : Models.t Lazy.t option ref;
unknown_reason : Sat_solver_sig.unknown_reason option;
declare_ids : Id.typed Vec.t;
declare_lim : int Vec.t;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is no need to do this dance in Fun_sat which is used as a functional data structure, this can simply be a declare_ids : Id.typed list field that is updated functionally ({ env with declare_ids = id :: env.declare_ids }) in declare.

Copy link
Collaborator Author

@Halbaroth Halbaroth Jan 2, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was my first implementation and it didn't work. A functional solution would be to use a list of lists:

declare_stack: Id.typed list list

We have to pop/push this stack in Fun_sat.pop/Fun_sat.push.
I didn't adopt this solution because I was afraid that a list of lists isn't cache-friendly. I understand that you want to keep the environment of FunSAT as pure as possible.

Honestly, I believe we should pull up all the imperative stuff of FunSAT into Funsat_frontend and use a stack of environment of FunSAT to simulate the push and the pop functions. In this design, we'll use a vector for declarations in the imperative environment of Funsat_frontend.

I also tried to implement the feature in Funsat_frontend without modifying the environment of FunSAT but we have no access to the right environment of Theory here.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, right, push and pop forces us to be imperative. Oh well. I guess the way to do this while staying consistent with the current Fun_sat module is Id.typed list Stack.t rather than Id.typed list list then.

I didn't adopt this solution because I afraid that a list of lists isn't cache-friendly.

You did write too much C++ :) A list of lists (or a stack of lists, which is the same thing) is very probably not going to be an issue here because we never actually look at the lists until model generation (and also because this only impacts calls to push and pop, which is virtually 0% of Alt-Ergo's runtime).

In this design, we'll use a vector for declarations in the imperative environment of Funsat_frontend.

If we use Funsat_frontend for push and pop we don't need a separate vector for declarations in Funsat_frontend, we can simply have declare_ids : Id.typed list in Funsat which will get tracked by the main stack in the frontend, I believe.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree to use Id.typed list Stack.t :)

}

let reset_refs () =
@@ -1123,7 +1125,8 @@ module Make (Th : Theory.S) = struct
else begin
try
(* also performs case-split and pushes pending atoms to CS *)
let model, _ = Th.compute_concrete_model env.tbox in
let declared_ids = Vec.to_list env.declare_ids in
let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in
env.last_saved_model := Some model;
env
with Ex.Inconsistent (expl, classes) ->
@@ -1611,6 +1614,10 @@ module Make (Th : Theory.S) = struct
"solved with backward!";
raise e

let declare env id =
Vec.push env.declare_ids id;
env

let push env to_push =
if Options.get_tableaux_cdcl () then
Errors.run_error
@@ -1626,6 +1633,7 @@ module Make (Th : Theory.S) = struct
let guards = ME.add new_guard
(mk_gf new_guard "" true true,Ex.empty)
acc.guards.guards in
Vec.push env.declare_lim (Vec.size env.declare_ids);
{acc with guards =
{ acc.guards with
current_guard = new_guard;
@@ -1656,6 +1664,8 @@ module Make (Th : Theory.S) = struct
in
acc.model_gen_phase := false;
env.last_saved_model := None;
let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
Vec.shrink env.declare_ids lim;
{acc with inst;
guards =
{ acc.guards with
@@ -1837,6 +1847,8 @@ module Make (Th : Theory.S) = struct
add_inst = selector;
last_saved_model = ref None;
unknown_reason = None;
declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
declare_lim = Vec.make 17 ~dummy:(-1);
}
in
assume env gf_true Ex.empty
2 changes: 2 additions & 0 deletions src/lib/reasoners/fun_sat.mli
Original file line number Diff line number Diff line change
@@ -38,6 +38,8 @@ module Make (Th : Theory.S) : sig

val empty : ?selector:(Expr.t -> bool) -> unit -> t

val declare : t -> Id.typed -> t

val push : t -> int -> t

val pop : t -> int -> t
3 changes: 3 additions & 0 deletions src/lib/reasoners/fun_sat_frontend.ml
Original file line number Diff line number Diff line change
@@ -45,6 +45,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
| FS.Unsat expl -> raise (Unsat expl)
| FS.I_dont_know e -> env := e; raise I_dont_know

let declare t id =
t := FS.declare !t id

let push t i = exn_handler (fun env -> t := FS.push env i) t

let pop t i = exn_handler (fun env -> t := FS.pop env i) t
7 changes: 7 additions & 0 deletions src/lib/reasoners/sat_solver_sig.ml
Original file line number Diff line number Diff line change
@@ -78,6 +78,13 @@ module type S = sig
The optional argument [selector] is used to filter ground facts
discovered by the instantiation engine. *)

val declare : t -> Id.typed -> unit
(** [declare env id] declares a new identifier [id].

If the environment [env] isn't unsatisfiable and the model generation
is enabled, the solver produces a model term for [id] which can be
retrieved with [get_model]. *)

val push : t -> int -> unit
(** [push env n] adds [n] new assertion levels in [env].

7 changes: 7 additions & 0 deletions src/lib/reasoners/sat_solver_sig.mli
Original file line number Diff line number Diff line change
@@ -58,6 +58,13 @@ module type S = sig
The optional argument [selector] is used to filter ground facts
discovered by the instantiation engine. *)

val declare : t -> Id.typed -> unit
(** [declare env id] declares a new identifier [id].

If the environment [env] isn't unsatisfiable and the model generation
is enabled, the solver produces a model term for [id] which can be
retrieved with [get_model]. *)

val push : t -> int -> unit
(** [push env n] adds [n] new assertion levels in [env].

16 changes: 13 additions & 3 deletions src/lib/reasoners/satml_frontend.ml
Original file line number Diff line number Diff line change
@@ -67,6 +67,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
mutable unknown_reason : Sat_solver_sig.unknown_reason option;
(** The reason why satml raised [I_dont_know] if it does; [None] by
default. *)
declare_ids : Id.typed Vec.t;
declare_lim : int Vec.t;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be simpler to use a vector of lists here:

mutable declare_ids : Id.typed list ;
declare_queue : Id.typed list Vec.t ;

Copy link
Collaborator Author

@Halbaroth Halbaroth Jan 2, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Uhm, Id.typed list Vec.tis a stack, not a queue in your suggestion, right?

I adopt this solution because it's the current style of SatML.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes it's a stack (for some reasons they are called "queues" elsewhere in satML but we can use the proper teminology ;) ).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So why do we need an extra field declare_ids here? The top element of the stack can be accessed in O(1). I believe

declare_stack: Id.typed list Vec.t 

is sufficient.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Even if the algorithmic complexity is identical, the constant term is not the same; having a separate field here avoids having to check that the vector is not empty on all accesses. It probably does not matter here because we never look at the declarations except during model generation but for the other vectors in SatML which are accessed much more frequently it might matter.

It's fine to use a non-empty Vec.t here (or even a Stack.t from the stdlib actually).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I will use the current design with an extra field.

}

let empty_guards () = {
@@ -97,6 +99,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
last_saved_model = None;
last_saved_objectives = None;
unknown_reason = None;
declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
declare_lim = Vec.make 17 ~dummy:(-1);
}

exception Sat
@@ -965,8 +969,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
if compute then begin
try
(* also performs case-split and pushes pending atoms to CS *)
let declared_ids = Vec.to_list env.declare_ids in
let model, objectives =
Th.compute_concrete_model (SAT.current_tbox env.satml)
Th.compute_concrete_model ~declared_ids (SAT.current_tbox env.satml)
in
env.last_saved_model <- Some model;
env.last_saved_objectives <- Some objectives;
@@ -1204,14 +1209,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
expr_guard, atom_guard
| _ -> assert false

let declare env id = Vec.push env.declare_ids id

let push env to_push =
Util.loop ~f:(fun _n () () ->
try
let expr_guard, atom_guard = create_guard env in
SAT.push env.satml atom_guard;
Stack.push expr_guard env.guards.stack_guard;
Steps.push_steps ();
env.guards.current_guard <- expr_guard
env.guards.current_guard <- expr_guard;
Vec.push env.declare_lim (Vec.size env.declare_ids)
with
| Util.Step_limit_reached _ ->
(* This function should be called without step limit
@@ -1234,7 +1242,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
env.last_saved_model <- None;
env.last_saved_objectives <- None;
env.inst <- inst;
env.guards.current_guard <- b
env.guards.current_guard <- b;
let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
Vec.shrink env.declare_ids lim
)
~max:to_pop
~elt:()
11 changes: 8 additions & 3 deletions src/lib/reasoners/theory.ml
Original file line number Diff line number Diff line change
@@ -61,7 +61,10 @@ module type S = sig
val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t

val add_term : t -> Expr.t -> add_in_cs:bool -> t
val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
val compute_concrete_model :
t ->
declared_ids:Id.typed list ->
Models.t Lazy.t * Objective.Model.t

val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val theories_instances :
@@ -879,13 +882,14 @@ module Main_Default : S = struct
let get_real_env t = t.gamma
let get_case_split_env t = t.gamma_finite

let compute_concrete_model env =
let compute_concrete_model env ~declared_ids =
let { gamma_finite; assumed_set; objectives; _ }, _ =
do_case_split_aux env ~for_model:true
in
lazy (
CC_X.extract_concrete_model
~prop_model:assumed_set
~declared_ids
gamma_finite
), objectives

@@ -940,7 +944,8 @@ module Main_Empty : S = struct
let get_case_split_env _ = CC_X.empty
let do_case_split env _ = env, E.Set.empty
let add_term env _ ~add_in_cs:_ = env
let compute_concrete_model _env = lazy Models.empty, Objective.Model.empty
let compute_concrete_model _env ~declared_ids:_ =
lazy Models.empty, Objective.Model.empty

let assume_th_elt e _ _ = e
let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, []
5 changes: 4 additions & 1 deletion src/lib/reasoners/theory.mli
Original file line number Diff line number Diff line change
@@ -54,7 +54,10 @@ module type S = sig

val add_term : t -> Expr.t -> add_in_cs:bool -> t

val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
val compute_concrete_model :
t ->
declared_ids:Id.typed list ->
Models.t Lazy.t * Objective.Model.t

val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val theories_instances :
8 changes: 4 additions & 4 deletions src/lib/reasoners/uf.ml
Original file line number Diff line number Diff line change
@@ -1167,11 +1167,11 @@ let compute_concrete_model_of_val cache =
let extract_concrete_model cache =
let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
let get_abstract_for = Cache.get_abstract_for cache.abstracts
in fun ~prop_model env ->
in fun ~prop_model ~declared_ids env ->
let terms, suspicious = terms env in
let model, mrepr =
MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
terms (ModelMap.empty ~suspicious, ME.empty)
terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
in
let model =
Hashtbl.fold (fun t vals mdl ->
@@ -1212,9 +1212,9 @@ let extract_concrete_model cache =
in
{ Models.propositional = prop_model; model; term_values = mrepr }

let extract_concrete_model ~prop_model =
let extract_concrete_model ~prop_model ~declared_ids =
let cache : cache = {
array_selects = Hashtbl.create 17;
abstracts = Hashtbl.create 17;
}
in fun env -> extract_concrete_model cache ~prop_model env
in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
Loading