Adding (reset) and (exit) statements (#852)

This patch adds support for the `(reset)` and `(exit)` statements in the SMT-LIB format to both frontends.

src/bin/common/solving_loop.ml

@@ -103,7 +103,8 @@ 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
   in
@@ -134,6 +135,9 @@ let main () =
       | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s ->
         let cnf = Cnf.make state.solver_ctx.local td in
         { state with solver_ctx = { state.solver_ctx with local = cnf; }}
+      | Typed.TReset _ ->
+        { state with solver_ctx = {ctx = []; local = []; global = []}}
+      | Typed.TExit _ -> raise Exit
       | _ ->
         let cnf = Cnf.make state.solver_ctx.ctx td in
         { state with solver_ctx = { state.solver_ctx with ctx = cnf; }}
@@ -206,6 +210,7 @@ let main () =
           if e != Warning_as_error then
             Printer.print_err "%a" Errors.report e;
           exit 1
+        | Exit -> exit 0
       end
     in
 
@@ -260,6 +265,7 @@ let main () =
     | Errors.Error e ->
       Printer.print_err "%a" Errors.report e;
       exit 1
+    | Exit -> exit 0
     | _ as exn -> Printexc.raise_with_backtrace exn bt
   in
   let finally ~handle_exn st e =
@@ -550,6 +556,13 @@ let main () =
             st
           end
 
+      | {contents = `Reset; _} ->
+        st
+        |> State.set partial_model_key None
+        |> State.set solver_ctx_key empty_solver_ctx
+
+      | {contents = `Exit; _} -> raise Exit
+
       | {contents = `Get_info kind; _ } ->
         handle_get_info st kind;
         st

src/lib/frontend/cnf.ml

@@ -461,5 +461,11 @@ let make acc (d : (_ Typed.tdecl, _) Typed.annoted) =
   | 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
   | TTypeDecl _ | TLogic _  -> acc
+  | TReset _
+  | TExit _ ->
+    (* These cases only appear on smt2 files, which are handled by
+       Solving_loop. *)
+    Printer.print_wrn "Ignoring instruction %a" Typed.print_atdecl d;
+    acc
 
 let make_list l = List.fold_left make [] (List.rev l)

src/lib/frontend/cnf.mli

@@ -31,10 +31,10 @@
 (* used in the typechecker for the text-mode *)
 val make :
   Commands.sat_tdecl list ->
-  (int Typed.tdecl, 'a) Typed.annoted ->
+  _ Typed.atdecl ->
   Commands.sat_tdecl list
 
 (* used in the GUI *)
 val make_list :
-  (int Typed.tdecl, 'a) Typed.annoted list ->
+  _ Typed.atdecl list ->
   Commands.sat_tdecl list

src/lib/frontend/frontend.ml

@@ -262,17 +262,18 @@ 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
     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/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
 
 (*****)
 
@@ -338,23 +340,28 @@ and print_formula =
       fprintf fmt "%a" print_formula f
     | _ -> fprintf fmt "(formula pprint not implemented)"
 
-(*
+
 let rec print_tdecl fmt = function
   | TTheory (_, name, _, l) ->
     Format.fprintf fmt "th %s: @[<v>%a@]" name
       (Util.print_list_pp ~sep:Format.pp_print_space ~pp:print_atdecl) l
-  | TAxiom (_, name, kind, f) ->
+  | TAxiom (_, name, _kind, f) ->
     Format.fprintf fmt "ax %s: @[<hov>%a@]" name print_formula f
   | TRewriting (_, name, l) ->
     Format.fprintf fmt "rwt %s: @[<hov>%a@]" name
       (Util.print_list_pp ~sep:Format.pp_print_space
          ~pp:(print_rwt print_term)) l
-  | TGoal (_, sort, name, f) ->
+  | TGoal (_, _sort, name, f) ->
     Format.fprintf fmt "goal %s: @[<hov>%a@]" name print_formula f
   | TPush (_loc,n) ->
     Format.fprintf fmt "push %d" n
   | TPop (_loc,n) ->
-    Format.fprintf fmt "pop %d" n
+    Format.fprintf fmt "pop %d"n
+  | TLogic _ -> Format.fprintf fmt "logic"
+  | TPredicate_def _ -> Format.fprintf fmt "predicate def"
+  | TFunction_def _ -> Format.fprintf fmt "function def"
+  | TTypeDecl _ -> Format.fprintf fmt "type decl"
+  | TReset _ -> Format.fprintf fmt "reset"
+  | TExit _ -> Format.fprintf fmt "exit"
 
 and print_atdecl fmt a = print_tdecl fmt a.c
-*)

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 all the context. *)
+  | TExit of Loc.t
+  (** Exits the solver. *)
 
 (** Typed declarations. *)
 (* TODO: wrap this in a record to factorize away
@@ -304,3 +308,6 @@ val print_rwt :
   (Format.formatter -> 'a -> unit) ->
   Format.formatter -> 'a rwt_rule -> unit
 (** Print a rewrite rule *)
+
+val print_atdecl : Format.formatter -> _ atdecl -> unit
+(** Print an annoted term decl. *)

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