Incremental smt2

alt-ergo-parsers.opam

@@ -17,7 +17,7 @@ depends: [
   "ocaml" {>= "4.04.0"}
   "dune" {>= "2.0"}
   "alt-ergo-lib" {= version}
-  "psmt2-frontend" {>= "0.2"}
+  "psmt2-frontend" {>= "0.3"}
   "camlzip" {>= "1.07"}
   "menhir"
   "stdlib-shims"

dune-project

@@ -76,7 +76,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (ocaml (>= 4.04.0))
   (dune (>= 2.0))
   (alt-ergo-lib (= :version))
-  (psmt2-frontend (>= 0.2))
+  (psmt2-frontend (>= 0.3))
   (camlzip (>= 1.07))
   menhir
   stdlib-shims

examples/lib_usage.ml

@@ -64,10 +64,11 @@ let () =
     (fun (pb, goal_name) ->
        let ctxt = FE.init_all_used_context () in
        let acc0 = SAT.empty (), true, Explanation.empty in
+       let s = Stack.create () in
        let _, consistent, ex =
          List.fold_left
            (fun acc d ->
-              FE.process_decl (fun _ _ -> ()) ctxt acc d
+              FE.process_decl (fun _ _ -> ()) ctxt s acc d
            )acc0 pb
        in
        Format.printf "%s@."

src/bin/gui/annoted_ast.ml

@@ -863,6 +863,10 @@ let rec print_typed_decl fmt td = match td.Typed.c with
     fprintf fmt "theory %s extends %s =\n%a\nend@."
       (Util.string_of_th_ext th_ext) name
       (fun fmt -> List.iter (print_typed_decl fmt)) decls
+  | TPush (_loc,n) ->
+    fprintf fmt "push %d" n
+  | TPop (_loc,n) ->
+    fprintf fmt "pop %d" n
 
 let print_typed_decl_list fmt = List.iter (fprintf fmt "%a@." print_typed_decl)
 
@@ -1247,6 +1251,8 @@ let rec annot_of_typed_decl (buffer:sbuffer) td =
     | TTypeDecl (loc, ty) ->
       let ls, s, lc = downgrade_type_decl ty in
       ATypeDecl (loc, ls, s, lc, ty)
+    | TPush _ | TPop _ ->
+      Gui_config.not_supported "Incremental commands"
   in
   new_annot buffer c td.Typed.annot ptag
 

src/bin/gui/main_gui.ml

@@ -641,15 +641,17 @@ let run_replay env used_context =
       "AST : @ -----@ %a" print_typed_decl_list ast;
 
   let ast_pruned = [ast] in
+  let consistent_dep = Stack.create () in
 
   Options.Time.start ();
   Options.Time.set_timeout ~is_gui:true (Options.get_timelimit ());
   List.iter
     (fun dcl ->
        let cnf = Cnf.make_list dcl in
        ignore (List.fold_left
-                 (FE.process_decl FE.print_status used_context)
-                 (empty_sat_inst env.insts, true, Explanation.empty) cnf)
+                 (FE.process_decl FE.print_status used_context consistent_dep)
+                 (empty_sat_inst env.insts, true, Explanation.empty)
+                 cnf)
     ) ast_pruned;
   Options.Time.unset_timeout ~is_gui:true
 
@@ -703,14 +705,15 @@ let run buttonrun buttonstop buttonclean inst_model timers_model
                Timers.set_timer_start (Timers.start timers_model.timers);
                Timers.set_timer_pause (Timers.pause timers_model.timers);
 
+               let consistent_dep = Stack.create () in
                List.iter
                  (fun dcl ->
                     let cnf = Cnf.make_list dcl in
                     ignore
                       (List.fold_left
                          (FE.process_decl
                             (wrapper_update_status image label buttonclean env)
-                            used_context)
+                            used_context consistent_dep)
                          (empty_sat_inst inst_model, true, Explanation.empty)
                          cnf)
                  ) ast_pruned;

src/bin/text/main_text.ml

@@ -72,6 +72,7 @@ type 'a state = {
 
 let solve all_context (cnf, goal_name) =
   let used_context = FE.choose_used_context all_context ~goal_name in
+  let consistent_dep_stack = Stack.create () in
   init_profiling ();
   try
     if Options.get_timelimit_per_goal() then
@@ -82,7 +83,7 @@ let solve all_context (cnf, goal_name) =
     SAT.reset_refs ();
     let _ =
       List.fold_left
-        (FE.process_decl FE.print_status used_context)
+        (FE.process_decl FE.print_status used_context consistent_dep_stack)
         (SAT.empty (), true, Explanation.empty) cnf
     in
     if Options.get_timelimit_per_goal() then
@@ -157,10 +158,11 @@ let () =
   let all_used_context = FE.init_all_used_context () in
   if Options.get_timelimit_per_goal() then
     FE.print_status FE.Preprocess 0;
+  let assertion_stack = Stack.create () in
   let typing_loop state p =
     if get_parse_only () then state else begin
       try
-        let l, env = I.type_parsed state.env p in
+        let l, env = I.type_parsed state.env assertion_stack p in
         List.fold_left (typed_loop all_used_context) { state with env; } l
       with
       | Errors.Error e ->

src/lib/frontend/cnf.ml

@@ -118,7 +118,7 @@ module ME =
     end)
 
 (* clean trigger:
-     remove useless terms in multi-triggers after inlining of lets*)
+   remove useless terms in multi-triggers after inlining of lets*)
 let clean_trigger ~in_theory name trig =
   if in_theory then trig
   else
@@ -542,6 +542,8 @@ let mk_theory acc l th_name extends _loc =
 
 let make acc d =
   match d.c with
+  | TPush (loc,n) -> {st_decl=Push n; st_loc=loc} :: acc
+  | TPop (loc,n) -> {st_decl=Pop n; st_loc=loc} :: acc
   | TTheory(loc, name, ext, l) -> mk_theory acc l name ext loc
   | TAxiom(loc, name, Util.Default, f) -> mk_assume acc f name loc
   | TAxiom(_, _, Util.Propagator, _) -> assert false

src/lib/frontend/frontend.ml

@@ -49,7 +49,9 @@ module type S = sig
   val process_decl:
     (status -> int -> unit) ->
     used_context ->
-    sat_env * bool * Ex.t -> Commands.sat_tdecl ->
+    (bool * Ex.t) Stack.t ->
+    sat_env * bool * Ex.t ->
+    Commands.sat_tdecl ->
     sat_env * bool * Ex.t
 
   val print_status : status -> int -> unit
@@ -140,9 +142,20 @@ 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 f_name)
     else Ex.empty
 
-  let process_decl print_status used_context ((env, consistent, dep) as acc) d =
+  let process_decl print_status used_context consistent_dep_stack
+      ((env, consistent, dep) as acc) d =
     try
       match d.st_decl with
+      | Push n ->
+        Util.loop ~f:(fun _n env () -> Stack.push env consistent_dep_stack)
+          ~max:n ~elt:(consistent,dep) ~init:();
+        SAT.push env n, consistent, dep
+      | Pop n ->
+        let consistent,dep =
+          Util.loop ~f:(fun _n () _env -> Stack.pop consistent_dep_stack)
+            ~max:n ~elt:() ~init:(consistent,dep)
+        in
+        SAT.pop env n, consistent, dep
       | Assume(n, f, mf) ->
         let is_hyp = try (Char.equal '@' n.[0]) with _ -> false in
         if not is_hyp && unused_context n used_context then

src/lib/frontend/frontend.mli

@@ -43,7 +43,9 @@ module type S = sig
   val process_decl:
     (status -> int -> unit) ->
     used_context ->
-    sat_env * bool * Explanation.t -> Commands.sat_tdecl ->
+    (bool * Explanation.t) Stack.t ->
+    sat_env * bool * Explanation.t ->
+    Commands.sat_tdecl ->
     sat_env * bool * Explanation.t
 
   val print_status : status -> int -> unit

src/lib/frontend/input.ml

@@ -26,7 +26,8 @@ module type S = sig
 
   val empty_env : env
 
-  val type_parsed : env -> parsed -> int Typed.atdecl list * env
+  val type_parsed :
+    env -> env Stack.t -> parsed -> int Typed.atdecl list * env
 
 end
 

src/lib/frontend/input.mli

@@ -43,8 +43,10 @@ module type S = sig
   val empty_env : env
   (** The empty/initial environment *)
 
-  val type_parsed : env -> parsed -> int Typed.atdecl list * env
-  (** Parse and typecheck some input file, together with some prelude files. *)
+  val type_parsed :
+    env -> env Stack.t -> parsed -> int Typed.atdecl list * env
+    (** Parse and typecheck some input file,
+        together with some prelude files. *)
 
 end
 

src/lib/frontend/parsed_interface.ml

@@ -91,6 +91,13 @@ let mk_theory_axiom loc name expr =
 let mk_theory_case_split loc name expr =
   Axiom (loc, name, Util.Default, expr)
 
+(** Declaration of stack assertions commands *)
+
+let mk_push loc n =
+  Push (loc, n)
+
+let mk_pop loc n =
+  Pop (loc, n)
 
 (** Making pure and logic types *)
 

src/lib/frontend/parsed_interface.mli

@@ -66,6 +66,11 @@ val mk_theory_axiom : Loc.t -> string -> lexpr -> decl
 
 val mk_theory_case_split : Loc.t -> string -> lexpr -> decl
 
+(** Declaration of stack assertions commands *)
+
+val mk_push : Loc.t -> int -> decl
+
+val mk_pop : Loc.t -> int -> decl
 
 (** Making pure and logic types *)
 

src/lib/frontend/typechecker.ml

@@ -1994,7 +1994,8 @@ let type_one_th_decl env e =
   | Goal(loc, _, _)
   | Predicate_def(loc,_,_,_)
   | Function_def(loc,_,_,_,_)
-  | TypeDecl ((loc, _, _, _)::_) ->
+  | TypeDecl ((loc, _, _, _)::_)
+  | Push (loc,_) | Pop (loc,_) ->
     typing_error WrongDeclInTheory loc
   | TypeDecl [] -> assert false
 
@@ -2143,9 +2144,30 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
     assert (not is_recursive); (* Abstract types are not recursive *)
     acc, env
 
-let rec type_decl (acc, env) d =
+let rec type_decl (acc, env) d assertion_stack =
   Types.to_tyvars := MString.empty;
   match d with
+  | Push (loc,n) ->
+    if n < 0 then
+      typing_error (ShouldBePositive n) loc;
+    Util.loop ~f:(fun _n env () -> Stack.push env assertion_stack)
+      ~max:n ~elt:env ~init:();
+    let td = {c = TPush(loc,n); annot = new_id () } in
+    (td,env) :: acc, env
+  | Pop (loc,n) ->
+    if n < 0 then
+      typing_error (ShouldBePositive n) loc;
+    let assertion_context_number = Stack.length assertion_stack in
+    if n > assertion_context_number then
+      typing_error (BadPopCommand
+                      {pushed = assertion_context_number; to_pop = n}) loc
+    else
+      let old_env = env in
+      let env = Util.loop ~f:(fun _n () _env -> Stack.pop assertion_stack)
+          ~max:n ~elt:() ~init:env in
+      let td = {c = TPop(loc,n); annot = new_id () } in
+      (td,old_env) :: acc, env
+
   | Theory (loc, name, ext, l) ->
     Options.tool_req 1 "TR-Typing-TheoryDecl$_F$";
     let tl = List.map (type_one_th_decl env) l in
@@ -2247,7 +2269,8 @@ let rec type_decl (acc, env) d =
     (* A. Typing types that are not recursive *)
     let acc, env =
       List.fold_left
-        (fun accu x -> type_decl accu (TypeDecl [x])) (acc, env) not_rec
+        (fun accu x ->
+           type_decl accu (TypeDecl [x]) assertion_stack) (acc, env) not_rec
     in
 
     (* B. Typing types that are recursive *)
@@ -2279,14 +2302,16 @@ let rec type_decl (acc, env) d =
          type_user_defined_type_body ~is_recursive:true env acc ty_d)
       (acc, env) are_rec
 
-let type_parsed env d =
-  let l, env' = type_decl ([], env) d in
+let type_parsed env s d =
+  let l, env' = type_decl ([], env) d s in
   List.rev_map fst l, env'
 
 let type_file ld =
   let env = Env.empty in
+  let assertion_stack = Stack.create () in
   let ltd, env =
-    List.fold_left type_decl ([], env) ld
+    List.fold_left
+      (fun acc d -> type_decl acc d assertion_stack) ([], env) ld
   in
   List.rev ltd, env
 

src/lib/frontend/typechecker.mli

@@ -41,7 +41,8 @@ val type_expr :
 (* TODO: give the env a proper module with binding functions,
          so that the list argument can be ommitted ? *)
 
-val type_parsed : env -> Parsed.decl -> int Typed.atdecl list * env
+val type_parsed :
+  env -> env Stack.t -> Parsed.decl -> int Typed.atdecl list * env
 (** Type a single declaration.
     @raise Typing_error {!Errors.Typing_error} *)