Adding reset and exit instructions

src/bin/common/solving_loop.ml

@@ -100,9 +100,12 @@ let main () =
       | `Sat partial_model | `Unknown partial_model ->
         Some partial_model
       | `Unsat -> None
-    with Util.Timeout ->
+    with
+    | Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142;
       None
+    | Exit ->
+      exit 0
   in
 
   let typed_loop all_context state td =

src/lib/frontend/cnf.ml

@@ -460,6 +460,8 @@ let make acc (d : (_ Typed.tdecl, _) Typed.annoted) =
   | TGoal(loc, sort, n, f) -> mk_query acc n f loc sort
   | TPredicate_def(loc, n, _args, f) -> mk_preddef acc f n loc
   | TFunction_def(loc, n, _args, _rety, f) -> mk_function acc f n loc
+  | TReset st_loc -> Commands.{st_decl=Reset; st_loc} :: acc
+  | TExit st_loc -> Commands.{st_decl=Exit; st_loc} :: acc
   | TTypeDecl _ | TLogic _  -> acc
 
 let make_list l = List.fold_left make [] (List.rev l)

src/lib/frontend/d_cnf.ml

@@ -2058,6 +2058,16 @@ let make dloc_file acc stmt =
       aux [] dcl;
       acc
 
+    | {contents = `Reset; loc; _} ->
+      let st_loc = dl_to_ael dloc_file loc in
+      let st_decl = C.Reset in
+      C.{ st_decl; st_loc } :: acc
+
+    | {contents = `Exit; loc; _} ->
+      let st_loc = dl_to_ael dloc_file loc in
+      let st_decl = C.Exit in
+      C.{ st_decl; st_loc } :: acc
+
     | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc
 
     | { contents = #Typer_Pipe.typechecked; _ } as stmt ->

src/lib/frontend/frontend.ml

@@ -254,17 +254,25 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         env, `Unsat, dep
 
       | ThAssume ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) ->
-        if unused_context ax_name used_context then
-          acc
-        else
-          match consistent with
-          | `Sat _ | `Unknown _ ->
-            let dep = mk_root_dep ax_name ax_form d.st_loc in
-            let env = SAT.assume_th_elt env th_elt dep in
-            env, consistent, dep
-          | `Unsat ->
-            env, consistent, dep
+        begin
+          if unused_context ax_name used_context then
+            acc
+          else
+            match consistent with
+            | `Sat _ | `Unknown _ ->
+              let dep = mk_root_dep ax_name ax_form d.st_loc in
+              let env = SAT.assume_th_elt env th_elt dep in
+              env, consistent, dep
+            | `Unsat ->
+              env, consistent, dep
+        end
+
+      | Reset ->
+        let env = SAT.empty () in
+        env, `Unknown env, Ex.empty
 
+      | Exit ->
+        raise Exit
     with
     | SAT.Sat t ->
       (* This case should mainly occur when a query has a non-unsat result,

src/lib/frontend/typechecker.ml

@@ -2217,7 +2217,7 @@ let type_one_th_decl env e =
   | Function_def(loc,_,_,_,_)
   | MutRecDefs ((loc,_,_,_,_) :: _)
   | TypeDecl ((loc, _, _, _)::_)
-  | Push (loc,_) | Pop (loc,_) ->
+  | Push (loc,_) | Pop (loc,_) | Reset loc | Exit loc ->
     Errors.typing_error WrongDeclInTheory loc
   | MutRecDefs []
   | TypeDecl [] -> assert false
@@ -2552,6 +2552,14 @@ let rec type_decl (acc, env) d assertion_stack =
          type_user_defined_type_body ~is_recursive:true env acc ty_d)
       (acc, env) are_rec
 
+  | Reset l ->
+    let td = {c = TReset l; annot = new_id () } in
+    (td,Env.empty) :: acc, Env.empty
+
+  | Exit l ->
+    let td = {c = TExit l; annot = new_id () } in
+    (td,env) :: acc, env
+
 let type_parsed env s d =
   let l, env' = type_decl ([], env) d s in
   List.rev_map fst l, env'

src/lib/structures/commands.ml

@@ -38,6 +38,8 @@ type sat_decl_aux =
   | ThAssume of Expr.th_elt
   | Push of int
   | Pop of int
+  | Reset
+  | Exit
 
 type sat_tdecl = {
   st_loc : Loc.t;
@@ -62,6 +64,8 @@ let print_aux fmt = function
     Format.fprintf fmt "th assume %a" Expr.print_th_elt t
   | Push n -> Format.fprintf fmt "Push %d" n
   | Pop n ->  Format.fprintf fmt "Pop %d" n
+  | Reset -> Format.fprintf fmt "Reset"
+  | Exit -> Format.fprintf fmt "Exit"
 
 let print fmt decl = print_aux fmt decl.st_decl
 

src/lib/structures/commands.mli

@@ -38,6 +38,8 @@ type sat_decl_aux =
   | ThAssume of Expr.th_elt
   | Push of int
   | Pop of int
+  | Reset
+  | Exit
 
 type sat_tdecl = {
   st_loc : Loc.t;

src/lib/structures/parsed.ml

@@ -276,5 +276,7 @@ type decl =
   | TypeDecl of type_decl list
   | Push of Loc.t * int
   | Pop of Loc.t * int
+  | Reset of Loc.t
+  | Exit of Loc.t
 
 type file = decl list

src/lib/structures/parsed.mli

@@ -137,5 +137,7 @@ type decl =
   | TypeDecl of type_decl list
   | Push of Loc.t * int
   | Pop of Loc.t * int
+  | Reset of Loc.t
+  | Exit of Loc.t
 
 type file = decl list

src/lib/structures/typed.ml

@@ -173,6 +173,8 @@ and 'a tdecl =
   | TTypeDecl of Loc.t * Ty.t
   | TPush of Loc.t * int
   | TPop of Loc.t * int
+  | TReset of Loc.t
+  | TExit of Loc.t
 
 (*****)
 

src/lib/structures/typed.mli

@@ -280,6 +280,10 @@ and 'a tdecl =
   (** [push (loc,n)] pushs n new assertions levels onto the assertion stack *)
   | TPop of Loc.t * int
   (** [pop (loc,n)] pops n assertions levels from the assertion stack *)
+  | TReset of Loc.t
+  (** Resets the assertions and the variable declarations. *)
+  | TExit of Loc.t
+  (** Exits alt-ergo. *)
 
 (** Typed declarations. *)
 (* TODO: wrap this in a record to factorize away

src/parsers/psmt2_to_alt_ergo.ml

@@ -434,6 +434,8 @@ module Translate = struct
     | Cmd_DefineFunsRec(fun_def_list,term_list) ->
       let l = List.map2 translate_fun_def fun_def_list term_list in
       l @ acc
+    | Cmd_Reset -> Reset (pos command) :: acc
+    | Cmd_Exit -> Exit (pos command) :: acc
     | Cmd_DefineSort _ -> acc
     | Cmd_GetModel -> requires_dolmen "get-model"; acc
     | Cmd_Echo _ -> not_supported "echo"; acc
@@ -445,7 +447,6 @@ module Translate = struct
     | Cmd_GetOption _ -> not_supported "get-option"; acc
     | Cmd_GetInfo _ -> not_supported "get-info"; acc
     | Cmd_GetUnsatAssumptions -> not_supported "get-unsat-assumptions"; acc
-    | Cmd_Reset -> not_supported "reset"; assert false
     | Cmd_ResetAssert -> not_supported "reset-asserts"; assert false
     | Cmd_SetLogic _ -> not_supported "set-logic"; acc
     | Cmd_SetOption _ -> not_supported "set-option"; acc
@@ -455,7 +456,6 @@ module Translate = struct
     | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; acc
     | Cmd_Maximize _ -> not_supported "maximize"; acc
     | Cmd_Minimize _ -> not_supported "minimize"; acc
-    | Cmd_Exit -> acc
 
   let init () =
     if Psmt2Frontend.Options.get_is_int_real () then