Use a stack of the stdlib for declared symbols in SatML

src/lib/reasoners/fun_sat.ml

@@ -177,7 +177,12 @@ 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 list Stack.t;
+
+    declare_top : Id.typed list ref;
+    declare_tail : Id.typed list Stack.t;
+    (** Stack of the declared symbols by the user. The field [declare_top]
+        is the top of the stack and [declare_tail] is tail. In particular, this
+        stack is never empty. *)
   }
 
   let reset_refs () =
@@ -1124,8 +1129,9 @@ module Make (Th : Theory.S) = struct
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
-        let declared_ids = Stack.top env.declare_ids in
-        let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in
+        let model, _ =
+          Th.compute_concrete_model ~declared_ids:!(env.declare_top) env.tbox
+        in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->
@@ -1614,10 +1620,7 @@ module Make (Th : Theory.S) = struct
       raise e
 
   let declare env id =
-    (* As we guarantee that the stack [env.declare_ids] is never empty,
-       we don't need to catch the [Stack.Empty] exception here. *)
-    let l = Stack.pop env.declare_ids in
-    Stack.push (id :: l) env.declare_ids;
+    env.declare_top := id :: !(env.declare_top);
     env
 
   let push env to_push =
@@ -1628,17 +1631,14 @@ module Make (Th : Theory.S) = struct
             Tableaux(CDCL) solver ! \
             Please use the Tableaux or CDLC SAT solvers instead"
         );
-    (* As we guarantee that the stack [env.declare_ids] is never empty,
-       we don't need to catch the [Stack.Empty] exception here. *)
-    let declare_ids = Stack.top env.declare_ids in
     Util.loop
       ~f:(fun _n () acc ->
           let new_guard = E.fresh_name Ty.Tbool in
           save_guard_and_refs acc new_guard;
           let guards = ME.add new_guard
               (mk_gf new_guard "" true true,Ex.empty)
               acc.guards.guards in
-          Stack.push declare_ids env.declare_ids;
+          Stack.push !(env.declare_top) env.declare_tail;
           {acc with guards =
                       { acc.guards with
                         current_guard = new_guard;
@@ -1670,7 +1670,7 @@ module Make (Th : Theory.S) = struct
           acc.model_gen_phase := false;
           env.last_saved_model := None;
           let () =
-            try ignore (Stack.pop env.declare_ids)
+            try env.declare_top := Stack.pop env.declare_tail
             with Stack.Empty ->
               (* Happens if we perform more pops than pushes. *)
               invalid_arg "Fun_sat.pop"
@@ -1856,10 +1856,10 @@ module Make (Th : Theory.S) = struct
       add_inst = (fun _ -> true);
       last_saved_model = ref None;
       unknown_reason = None;
-      declare_ids = Stack.create ();
+      declare_top = ref [];
+      declare_tail = Stack.create ();
     }
     in
-    Stack.push [] env.declare_ids;
     assume env gf_true Ex.empty
   (*maybe usefull when -no-theory is on*)
 

src/lib/reasoners/sat_solver_sig.ml

@@ -87,7 +87,9 @@ module type S = sig
 
   (** [pop env n] remove an assertion level.
       Internally, the guard g introduced in the push correponsding to this pop
-      will be propagated to false (at level 0) *)
+      will be propagated to false (at level 0)
+
+      @raise invalid_arg if there is no [n] assertion levels in [env]. *)
   val pop : t -> int -> unit
 
   (* [assume env f] assume a new formula [f] in [env]. Raises Unsat if

src/lib/reasoners/sat_solver_sig.mli

@@ -69,7 +69,7 @@ module type S = sig
       Internally, the guard g introduced in the push correponsding to this pop
       will be propagated to false (at level 0)
 
-      May raise [invalid_arg] if there is no [n] assertion levels in [env]. *)
+      @raise invalid_arg if there is no [n] assertion levels in [env]. *)
   val pop : t -> int -> unit
 
   (** [assume env f] assume a new formula [f] in [env]. Raises Unsat if

src/lib/reasoners/satml_frontend.ml

@@ -67,8 +67,12 @@ 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;
+
+    mutable declare_top : Id.typed list;
+    declare_tail : Id.typed list Stack.t;
+    (** Stack of the declared symbols by the user. The field [declare_top]
+        is the top of the stack and [declare_tail] is tail. In particular, this
+        stack is never empty. *)
   }
 
   let empty_guards () = {
@@ -99,8 +103,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);
+      declare_top = [];
+      declare_tail = Stack.create ();
     }
 
   let empty_with_inst add_inst =
@@ -972,9 +976,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 ~declared_ids (SAT.current_tbox env.satml)
+          Th.compute_concrete_model ~declared_ids:env.declare_top
+            (SAT.current_tbox env.satml)
         in
         env.last_saved_model <- Some model;
         env.last_saved_objectives <- Some objectives;
@@ -1212,7 +1216,8 @@ 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 declare env id =
+    env.declare_top <- id :: env.declare_top
 
   let push env to_push =
     Util.loop ~f:(fun _n () () ->
@@ -1222,7 +1227,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           Stack.push expr_guard env.guards.stack_guard;
           Steps.push_steps ();
           env.guards.current_guard <- expr_guard;
-          Vec.push env.declare_lim (Vec.size env.declare_ids)
+          Stack.push env.declare_top env.declare_tail;
         with
         | Util.Step_limit_reached _ ->
           (* This function should be called without step limit
@@ -1246,8 +1251,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           env.last_saved_objectives <- None;
           env.inst <- inst;
           env.guards.current_guard <- b;
-          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
-          Vec.shrink env.declare_ids lim
+          let declare_top =
+            try Stack.pop env.declare_tail
+            with Stack.Empty -> invalid_arg "Satml_frontend.pop"
+          in
+          env.declare_top <- declare_top;
         )
       ~max:to_pop
       ~elt:()

tests/cram.t/run.t

@@ -13,7 +13,7 @@ appropriate here.
     (define-fun x () Int 0)
     (define-fun y () Int 0)
     (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
-    (define-fun a2 () (Array Int Int) (as @a3 (Array Int Int)))
+    (define-fun a2 () (Array Int Int) (as @a0 (Array Int Int)))
   )
 
 Now we will test some semantic triggers.

tests/models/arith/arith11.optimize.expected

@@ -4,7 +4,7 @@ unknown
   (define-fun p1 () Bool false)
   (define-fun p2 () Bool true)
   (define-fun x () Real 2.0)
-  (define-fun y () Real (as @a3 Real))
+  (define-fun y () Real (as @a0 Real))
 )
 (objectives 
   (x 2.0)

tests/models/bool/bool2.models.expected

@@ -2,7 +2,7 @@
 unknown
 (
   (define-fun x () Bool false)
-  (define-fun y () Bool (as @a1 Bool))
+  (define-fun y () Bool (as @a0 Bool))
 )
 ((notx true))
 

tests/models/complete_2.models.expected

@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Int (as @a0 Int))
-  (define-fun f ((_arg_0 Int)) Int (as @a2 Int))
+  (define-fun x () Int (as @a2 Int))
+  (define-fun f ((_arg_0 Int)) Int (as @a1 Int))
 )