Reactivating abstract value printing and update tests

src/bin/common/dune

@@ -21,8 +21,7 @@
    Parse_command
    Input_frontend
    Signals_profiling
-   Solving_loop
-   Solving_loop_imperative)
+   Solving_loop)
 )
 
 (generate_sites_module

src/bin/common/solving_loop.ml

@@ -1199,9 +1199,12 @@ let main () =
         in
         st
 
-      | {contents = `Decls l; _} ->
+      | {contents = `Decls l; loc; _} ->
         let st = DO.Mode.set Util.Assert st in
-        D_cnf.cache_decls l;
+        let decls = D_cnf.make_decls l in
+        let module Api = (val DO.SatSolverModule.get st) in
+        let loc = dl_to_ael file_loc loc in
+        List.iter (fun decl -> Api.FE.declare ~loc decl Api.env) decls;
         st
 
       (* When the next statement is a goal, the solver is called and provided
@@ -1371,7 +1374,7 @@ let main () =
             let st = handle_reset st in
             let whole_path = List.rev_append prefix tl in
             Format.eprintf "Restarting with %i instructions@." (List.length whole_path);
-            aux (State.get named_terms st) st whole_path
+            aux Util.MS.empty st whole_path
           | {contents; _ } ->
             let st =
               let new_current_path =

src/lib/frontend/d_cnf.ml

@@ -697,14 +697,14 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
   in
   Cache.store_sy tcst sy;
   (* 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) *)
+  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
@@ -1898,16 +1898,16 @@ let make_form name_base f loc ~decl_kind =
   else
     E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind
 
-let cache_decls = function
+let make_decls = function
   | [] -> assert false (* We could probably just return (). *)
   | [td] ->
     begin
       match td with
-      | `Type_decl (td, _def) -> mk_ty_decl td
-      | `Term_decl td -> mk_term_decl td;
+      | `Type_decl (td, _def) -> mk_ty_decl td; []
+      | `Term_decl td -> [mk_term_decl td];
     end
   | dcl ->
-    let rec aux acc tdl =
+    let rec aux term_acc 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.
          But it doesn't affect the execution.
@@ -1919,20 +1919,21 @@ let cache_decls = function
           | [otd] -> mk_ty_decl otd
           | _ -> mk_mr_ty_decls (List.rev acc)
         end;
-        mk_term_decl td;
-        aux [] tl
+        let t = mk_term_decl td in
+        aux (t :: term_acc) [] tl
 
       | `Type_decl (td, _def) :: tl ->
-        aux (td :: acc) tl
+        aux term_acc (td :: acc) tl
 
       | [] ->
         begin match acc with
           | [] -> ()
           | [otd] -> mk_ty_decl otd
           | _ ->  mk_mr_ty_decls (List.rev acc)
-        end
+        end;
+        term_acc
     in
-    aux [] dcl
+    aux [] [] dcl
 
 (* Helper function used to check if the expression defining an objective
    function is a pure term. *)

src/lib/frontend/d_cnf.mli

@@ -99,7 +99,7 @@ val pp_query :
 (** Registers the declarations in the cache. If there are more than one element
     in the list, it is assumed they are mutually recursive (but if it is not the
     case, it still work). *)
-val cache_decls : D_loop.Typer_Pipe.decl list -> unit
+val make_decls : D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list
 
 val builtins :
   Dolmen_loop.State.t ->

src/lib/frontend/frontend.ml

@@ -146,6 +146,8 @@ module type S = sig
 
   val init_env : ?sat_env:sat_env -> used_context -> env
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process
@@ -436,6 +438,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let wrap_f f ?loc x env =
     check_if_over (handle_sat_exn f ?loc x) env
 
+  let declare = wrap_f internal_decl
+
   let push = wrap_f internal_push
 
   let pop = wrap_f internal_pop

src/lib/frontend/frontend.mli

@@ -70,6 +70,8 @@ module type S = sig
       the user. *)
   type 'a process = ?loc:Loc.t -> 'a -> env -> unit
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process

tests/cram.t/run.t

@@ -11,7 +11,7 @@ appropriate here.
   (
     (define-fun x () Int 0)
     (define-fun y () Int 0)
-    (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
     (define-fun a2 () (Array Int Int) (as @a0 (Array Int Int)))
   )
 

tests/issues/555.models.expected

@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
 )

tests/issues/854/function.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun f ((_arg_0 Int)) Int 0)
   (define-fun a1 () Int 0)

tests/issues/854/original.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )

tests/issues/854/twice_eq.models.expected

@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )

tests/models/array/array1.models.expected

@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
 )

tests/models/array/embedded-array.models.expected

@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun s () S (as @a0 S))
+  (define-fun s () S (as @a2 S))
   (define-fun x () Pair
-   (pair (store (as @a1 (Array Int S)) 0 s)
-         (store (as @a1 (Array Int S)) 0 s)))
+   (pair (store (as @a3 (Array Int S)) 0 s)
+         (store (as @a3 (Array Int S)) 0 s)))
 )