First version of full incremental solving loop

src/lib/frontend/d_cnf.mli

@@ -44,22 +44,71 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t
       individually.
 *)
 
+(** [ make_defs dlist loc ]
+    Transforms the dolmen definition list [dlist] into an Alt-Ergo definition.
+    Dolmen definitions can be:
+    - Definitions, that either are predicates (transformed in `PredDef) or
+      simple definitions (transformed in `Assume);
+    - Type aliases (filtered out);
+    - Statements used in models (they must not be in the input list, otherwise
+      this function fails). *)
+val make_defs :
+  D_loop.Typer_Pipe.def list ->
+  Loc.t ->
+  [> `Assume of string * Expr.t  | `PredDef of Expr.t * string ] list
+
+(** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term]
+
+    Builds an Alt-Ergo hashconsed expression from a dolmen term
+*)
+val make_expr :
+  ?loc:Loc.t ->
+  ?name_base:string ->
+  ?toplevel:bool ->
+  decl_kind:Expr.decl_kind -> D_loop.DStd.Expr.term -> Expr.t
+
+(** [make_form name term loc decl_kind]
+    Same as `make_expr`, but for formulas. It applies a purification step and
+    processes free variables by adding a forall quantifier. *)
 val make_form :
   string ->
   D_loop.DStd.Expr.term ->
   Loc.t ->
   decl_kind:Expr.decl_kind ->
   Expr.t
 
-val make :
-  D_loop.DStd.Loc.file ->
-  Commands.sat_tdecl list ->
-  [< D_loop.Typer_Pipe.typechecked
-  | `Optimize of Dolmen.Std.Expr.term * bool
-  | `Goal  of Dolmen.Std.Expr.term
-  | `Check of Dolmen.Std.Expr.term list
-         > `Hyp ] D_loop.Typer_Pipe.stmt ->
-  Commands.sat_tdecl list
+(** Preprocesses the body of a goal by:
+    - removing the top-level universal quantifiers and considering their
+      quantified variables as uninsterpreted symbols.
+    - transforming a given formula: [a[1] -> a[2] -> ... -> a[n]] in which
+      the [a[i]]s are subformulas and [->] is a logical implication, to a set of
+      hypotheses [{a[1]; ...; a[n-1]}], and a goal [a[n]] whose validity is
+      verified by the solver.
+      If additional hypotheses are provided in [hyps], they are preprocessed and
+      added to the set of hypotheses in the same way as the left-hand side of
+      implications. In other words, [pp_query ~hyps:[h1; ...; hn] t] is the same
+      as [pp_query (h1 -> ... -> hn t)], but more convenient if the some
+      hypotheses are already separated from the goal.
+      Returns a list of hypotheses and the new goal body
+*)
+val pp_query :
+  ?hyps:D_loop.DStd.Expr.term list ->
+  D_loop.DStd.Expr.term ->
+  D_loop.DStd.Expr.term list * D_loop.DStd.Expr.term
+
+(** 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 :
+ *   D_loop.DStd.Loc.file ->
+ *   Commands.sat_tdecl list ->
+ *   [< D_loop.Typer_Pipe.typechecked
+ *   | `Goal  of Dolmen.Std.Expr.term
+ *   | `Check of Dolmen.Std.Expr.term list
+ *          > `Hyp ] D_loop.Typer_Pipe.stmt ->
+ *   Commands.sat_tdecl list *)
 (** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the
     type-checked statement [stmt] and appends them to [acc].
 *)
@@ -68,3 +117,5 @@ val builtins :
   Dolmen_loop.State.t ->
   D_loop.Typer.lang ->
   Dolmen_loop.Typer.T.builtin_symbols
+
+val is_pure_term : Expr.t -> bool

src/lib/frontend/d_state_option.ml

@@ -32,6 +32,13 @@ module O = Options
 module State = D_loop.State
 module Typer = D_loop.Typer
 
+type 'a hook =
+  'a D_loop.State.key ->
+  old:'a ->
+  new_:'a ->
+  D_loop.Typer.state ->
+  D_loop.Typer.state
+
 module type Accessor = sig
   (** The data saved in the state. *)
   type t
@@ -45,34 +52,64 @@ module type S = sig
   include Accessor
 
   (** Sets the option on the dolmen state. *)
-  val set : t -> D_loop.Typer.state -> D_loop.Typer.state
+  val set : t -> Typer.state -> Typer.state
 
   (** Clears the option from the state. *)
-  val clear : D_loop.Typer.state -> D_loop.Typer.state
+  val clear : Typer.state -> Typer.state
+end
+
+module type S_with_hooks = sig
+  include S
+
+  val reset_hooks : unit -> unit
+
+  val add_hook : t hook -> unit
 end
 
 let create_opt
     (type t)
-    ?(on_update=(fun _ _ -> Fun.id))
+    ?on_update
     (key : string)
-    (get : unit -> t) : (module S with type t = t) =
+    (default_get : unit -> t) : (module S_with_hooks with type t = t) =
   (module struct
     type nonrec t = t
 
+    let on_update_base =
+      match on_update with
+      | None -> []
+      | Some f -> [f]
+
+    let on_update_list = ref on_update_base
+
     let key = State.create_key ~pipe:"" key
 
-    let set opt st =
-      st
-      |> on_update key opt
-      |> State.set key opt
+    let apply_hooks ~old ~new_ st =
+      List.fold_left
+        (fun acc f -> f key ~old ~new_ acc)
+        st
+        !on_update_list
 
     let unsafe_get st = State.get key st
 
-    let clear st = State.update_opt key (fun _ -> None) st
-
     let get st =
       try unsafe_get st with
-      | State.Key_not_found _ -> get ()
+      | State.Key_not_found _ -> default_get ()
+
+    let set new_ st =
+      let old = get st in
+      let st = apply_hooks ~old ~new_ st in
+      State.set key new_ st
+
+    let clear st =
+      let old = get st in
+      let new_ = default_get () in
+      st
+      |> apply_hooks ~old ~new_
+      |> State.update_opt key (fun _ -> None)
+
+    let reset_hooks () = on_update_list := on_update_base
+
+    let add_hook h = on_update_list := h :: !on_update_list
   end)
 
 (* The current mode of the sat solver. Serves as a flag for some options that
@@ -83,12 +120,12 @@ module Mode = (val (create_opt "start_mode") (fun _ -> Util.Start))
    in start mode. *)
 let create_opt_only_start_mode
     (type t)
-    ?(on_update=(fun _ _ -> Fun.id))
+    ?(on_update=(fun _ ~old:_ ~new_:_ -> Fun.id))
     (key : string)
-    (get : unit -> t) : (module S with type t = t) =
-  let on_update k opt st =
+    (get : unit -> t) : (module S_with_hooks with type t = t) =
+  let on_update k ~old ~new_ st =
     match Mode.get st with
-    | Util.Start -> on_update k opt st
+    | Util.Start -> on_update k ~old ~new_ st
     | curr_mode -> Errors.invalid_set_option curr_mode key
   in
   create_opt ~on_update key get
@@ -103,14 +140,28 @@ module Optimize =
 module ProduceAssignment =
   (val (create_opt_only_start_mode "produce_assignment" (fun _ -> false)))
 
+module type Sat_solver_api = sig
+  module SAT : Sat_solver_sig.S
+  module FE : Frontend.S with type sat_env = SAT.t
+
+  val env : FE.env
+end
+
 let get_sat_solver
     ?(sat = O.get_sat_solver ())
     ?(no_th = O.get_no_theory ())
-    () =
+    () : (module Sat_solver_api) =
   let module SatCont =
     (val (Sat_solver.get sat) : Sat_solver_sig.SatContainer) in
   let module TH = (val Sat_solver.get_theory ~no_th) in
-  (module SatCont.Make(TH) : Sat_solver_sig.S)
+  let module SAT : Sat_solver_sig.S = SatCont.Make(TH) in
+  let module FE : Frontend.S with type sat_env = SAT.t = Frontend.Make (SAT) in
+  (module struct
+    module SAT = SAT
+    module FE = FE
+
+    let env = FE.init_env (Frontend.init_all_used_context ())
+  end)
 
 module SatSolverModule =
   (val (
@@ -119,15 +170,15 @@ module SatSolverModule =
        (fun _ -> get_sat_solver ())))
 
 let msatsolver =
-  let on_update _ sat st =
-    SatSolverModule.set (get_sat_solver ~sat ()) st
+  let on_update _ ~old:_ ~new_ st =
+    SatSolverModule.set (get_sat_solver ~sat:new_ ()) st
   in
   (create_opt_only_start_mode ~on_update "sat_solver" O.get_sat_solver)
 
 module SatSolver = (val msatsolver)
 
 let msteps =
-  let on_update _ sat st = Steps.set_steps_bound sat; st in
+  let on_update _ ~old:_ ~new_ st = Steps.set_steps_bound new_; st in
   (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound)
 
 module Steps = (val msteps)

src/lib/frontend/d_state_option.mli

@@ -32,6 +32,14 @@
     an option that can be set, fetched et reset independently from the
     Options module, which is used as a static reference. *)
 
+(** A hook which is called when an option is updated. *)
+type 'a hook =
+  'a D_loop.State.key ->
+  old:'a ->
+  new_:'a ->
+  D_loop.Typer.state ->
+  D_loop.Typer.state
+
 module type Accessor = sig
   (** The data saved in the state. *)
   type t
@@ -51,8 +59,18 @@ module type S = sig
   val clear : D_loop.Typer.state -> D_loop.Typer.state
 end
 
+module type S_with_hooks = sig
+  include S
+
+  (** Resets all hooks, except the one registered at initialization. *)
+  val reset_hooks : unit -> unit
+
+  (** Adds a hook which is called during the update of the value. *)
+  val add_hook : t hook -> unit
+end
+
 (** The current mode of the solver. *)
-module Mode : S with type t = Util.mode
+module Mode : S_with_hooks with type t = Util.mode
 
 (** Options are divided in two categories:
     1. options that can be updated anytime;
@@ -71,9 +89,17 @@ module ProduceAssignment : S with type t = bool
 (** The Sat solver used. When set, updates the SatSolverModule defined below. *)
 module SatSolver : S with type t = Util.sat_solver
 
+module type Sat_solver_api = sig
+  module SAT : Sat_solver_sig.S
+
+  module FE : Frontend.S with type sat_env = SAT.t
+
+  val env : FE.env
+end
+
 (** The Sat solver module used for the calculation. This option's value depends
     on SatSolver: when SatSolver is updated, this one also is. *)
-module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)
+module SatSolverModule : Accessor with type t = (module Sat_solver_api)
 
 (** Option for setting the max number of steps. Interfaces with the toplevel
     Steps module.

src/lib/frontend/frontend.ml

@@ -239,6 +239,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       expl = Explanation.empty
     }
 
+  let set_result env res = env.res <- res
+
   let output_used_context g_name dep =
     if not (Options.get_js_mode ()) then begin
       let f = Options.get_used_context_file () in
@@ -315,7 +317,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         ~max:n ~elt:() ~init:(env.res, env.expl)
     in
     SAT.pop env.sat_env n;
-    env.res <- res;
+    set_result env res;
     env.expl <- expl
 
   let internal_assume
@@ -382,7 +384,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     in
     if get_debug_unsat_core () then check_produced_unsat_core expl;
     if get_save_used_context () then output_used_context n expl;
-    env.res <- `Unsat;
+    set_result env `Unsat;
     env.expl <- expl
 
   let internal_th_assume
@@ -413,12 +415,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let handle_sat_exn f ?loc x env =
     try f ?loc x env with
-    | SAT.Sat -> env.res <- `Sat
+    | SAT.Sat -> set_result env `Sat
     | SAT.Unsat expl ->
-      env.res <- `Unsat;
+      set_result env `Unsat;
       env.expl <- Ex.union expl env.expl
-    | SAT.I_dont_know ->
-      env.res <- `Unknown
+    | SAT.I_dont_know -> set_result env `Unknown
+    | Util.Step_limit_reached _ -> set_result env `Unknown
+  (* The SAT.Timeout exception is not catched. *)
 
   (* Wraps the function f to check if the step limit is reached (in which case,
      don't do anything), and then calls the function & catches the
@@ -477,7 +480,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       (* This case should mainly occur when a query has a non-unsat result,
          so we want to print the status in this case. *)
       hook_on_status (Sat (d, env.sat_env)) (Steps.get_steps ());
-      env.res <- `Sat
+      set_result env `Sat
 
     | SAT.Unsat expl' ->
       (* This case should mainly occur when a new assumption results in an unsat
@@ -486,7 +489,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       let expl = Ex.union env.expl expl' in
       if get_debug_unsat_core () then check_produced_unsat_core expl;
       (* print_status (Inconsistent d) (Steps.get_steps ()); *)
-      env.res <- `Unsat;
+      set_result env `Unsat;
       env.expl <- expl
 
     | SAT.I_dont_know ->
@@ -500,7 +503,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       hook_on_status status (Steps.get_steps ());
       (* TODO: Is it an appropriate behaviour? *)
       (*       if timeout != NoTimeout then raise Util.Timeout; *)
-      env.res <- `Unknown
+      set_result env `Unknown
 
     | Util.Timeout as e ->
       (* In this case, we obviously want to print the status,