Skip to content

Commit

Permalink
First version of full incremental solving loop
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevendeo committed Mar 21, 2024
1 parent adafb41 commit b917b79
Show file tree
Hide file tree
Showing 17 changed files with 955 additions and 574 deletions.
541 changes: 426 additions & 115 deletions src/bin/common/solving_loop.ml

Large diffs are not rendered by default.

569 changes: 205 additions & 364 deletions src/lib/frontend/d_cnf.ml

Large diffs are not rendered by default.

61 changes: 50 additions & 11 deletions src/lib/frontend/d_cnf.mli
Original file line number Diff line number Diff line change
Expand Up @@ -44,27 +44,66 @@ 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

(** [make_expr ~loc ~name_base ~toplevel ~decl_kind term]
Builds an Alt-Ergo hashconsed expression from a dolmen term
*)
val mk_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
(** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the
type-checked statement [stmt] and appends them to [acc].
(** 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 builtins :
Dolmen_loop.State.t ->
D_loop.Typer.lang ->
Dolmen_loop.Typer.T.builtin_symbols

val is_pure_term : Expr.t -> bool
91 changes: 71 additions & 20 deletions src/lib/frontend/d_state_option.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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 (
Expand All @@ -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)
Expand Down
30 changes: 28 additions & 2 deletions src/lib/frontend/d_state_option.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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;
Expand All @@ -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.
Expand Down
21 changes: 12 additions & 9 deletions src/lib/frontend/frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -322,7 +324,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
Expand Down Expand Up @@ -389,7 +391,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
Expand Down Expand Up @@ -420,12 +422,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
Expand Down Expand Up @@ -485,7 +488,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
Expand All @@ -494,7 +497,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 ->
Expand All @@ -508,7 +511,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,
Expand Down
Loading

0 comments on commit b917b79

Please sign in to comment.