simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(smt): remove functor, split into modules

Browse source
This commit is contained in:
Simon Cruanes 2022-07-30 21:18:30 -04:00
parent 6e1da96e7e
commit 05faac97e7
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
10 changed files with 125 additions and 199 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/dune
View file

@ -3,5 +3,5 @@
(public_name sidekick.smt-solver)
(synopsis "main SMT solver")
(libraries containers iter sidekick.core sidekick.util sidekick.cc
sidekick.sat)
sidekick.sat sidekick.simplify)
(flags :standard -w +32 -open Sidekick_util))

4
src/smt/model.ml
View file

@ -22,3 +22,7 @@ let pp out = function
in
Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
(Term.Tbl.to_iter tbl)
module Internal_ = struct
let of_tbl t = Map t
end

18
src/smt/model.mli Normal file
View file

@ -0,0 +1,18 @@
(** Models
A model can be produced when the solver is found to be in a
satisfiable state after a call to {!solve}. *)
open Sigs
type t
val empty : t
val mem : t -> term -> bool
val find : t -> term -> term option
val eval : t -> term -> term option
val pp : t Fmt.printer
module Internal_ : sig
val of_tbl : term Term.Tbl.t -> t
end

1
src/smt/sigs.ml
View file

@ -13,6 +13,7 @@
*)
include Sidekick_core
module Simplify = Sidekick_simplify
module CC = Sidekick_cc.CC
module E_node = Sidekick_cc.E_node
module CC_expl = Sidekick_cc.Expl

81
src/smt/simplify.ml
View file

@ -1,81 +0,0 @@
open Sidekick_core
open Sigs
open struct
module P = Proof_trace
module Rule_ = Proof_core
end
type t = {
tst: term_store;
proof: proof_trace;
mutable hooks: hook list;
(* store [t --> u by step_ids] in the cache.
We use a bag for the proof steps because it gives us structural
sharing of subproofs. *)
cache: (Term.t * step_id Bag.t) Term.Tbl.t;
}
and hook = t -> term -> (term * step_id Iter.t) option
let create tst ~proof : t =
{ tst; proof; hooks = []; cache = Term.Tbl.create 32 }
let[@inline] tst self = self.tst
let[@inline] proof self = self.proof
let add_hook self f = self.hooks <- f :: self.hooks
let clear self = Term.Tbl.clear self.cache
let normalize (self : t) (t : Term.t) : (Term.t * step_id) option =
(* compute and cache normal form of [t] *)
let rec loop t : Term.t * _ Bag.t =
match Term.Tbl.find self.cache t with
| res -> res
| exception Not_found ->
let steps_u = ref Bag.empty in
let u = aux_rec ~steps:steps_u t self.hooks in
Term.Tbl.add self.cache t (u, !steps_u);
u, !steps_u
and loop_add ~steps t =
let u, pr_u = loop t in
steps := Bag.append !steps pr_u;
u
(* try each function in [hooks] successively, and rewrite subterms *)
and aux_rec ~steps t hooks : Term.t =
match hooks with
| [] ->
let u =
Term.map_shallow self.tst ~f:(fun _inb u -> loop_add ~steps u) t
in
if Term.equal t u then
t
else
loop_add ~steps u
| h :: hooks_tl ->
(match h self t with
| None -> aux_rec ~steps t hooks_tl
| Some (u, _) when Term.equal t u -> aux_rec ~steps t hooks_tl
| Some (u, pr_u) ->
let bag_u = Bag.of_iter pr_u in
steps := Bag.append !steps bag_u;
let v, pr_v = loop u in
(* fixpoint *)
steps := Bag.append !steps pr_v;
v)
in
let u, pr_u = loop t in
if Term.equal t u then
None
else (
(* proof: [sub_proofs |- t=u] by CC + subproof *)
let step =
P.add_step self.proof
@@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u)
in
Some (u, step)
)
let normalize_t self t =
match normalize self t with
| Some (u, pr_u) -> u, Some pr_u
| None -> t, None

39
src/smt/simplify.mli
View file

@ -1,39 +0,0 @@
(** Term simplifier *)
open Sidekick_core
open Sigs
type t
val tst : t -> term_store
val clear : t -> unit
(** Reset internal cache, etc. *)
val proof : t -> proof_trace
(** Access proof *)
type hook = t -> term -> (term * step_id Iter.t) option
(** Given a term, try to simplify it. Return [None] if it didn't change.
A simple example could be a hook that takes a term [t],
and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
returns [Some (const (x+y))], and [None] otherwise.
The simplifier will take care of simplifying the resulting term further,
caching (so that work is not duplicated in subterms), etc.
*)
val add_hook : t -> hook -> unit
val normalize : t -> term -> (term * step_id) option
(** Normalize a term using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside
the term. *)
val normalize_t : t -> term -> term * step_id option
(** Normalize a term using all the hooks, along with a proof that the
simplification is correct.
returns [t, ø] if no simplification occurred. *)
val create : Term.store -> proof:Proof_trace.t -> t

25
src/smt/solver.ml
View file

@ -1,6 +1,7 @@
open Sigs
open struct
module SI = Solver_internal
module P = Proof_trace
module Rule_ = Proof_core
end
@ -30,7 +31,7 @@ end
end)
*)
module Sat_solver = Sidekick_sat.Make_cdcl_t (Solver_internal)
module Sat_solver = Sidekick_sat
(** the parametrized SAT Solver *)
(** {2 Result} *)
@ -100,7 +101,7 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
si;
proof;
last_res = None;
solver = Sat_solver.create ~proof ?size ~stat si;
solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
stat;
count_clause = Stat.mk_int stat "solver.add-clause";
count_solve = Stat.mk_int stat "solver.solve";
@ -127,11 +128,11 @@ let reset_last_res_ self = self.last_res <- None
(* preprocess clause, return new proof *)
let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) :
lit array * step_id =
Solver_internal.preprocess_clause_iarray_ self.si c pr
Solver_internal.preprocess_clause_array self.si c pr
let mk_lit_t (self : t) ?sign (t : term) : lit =
let lit = Lit.atom ?sign t in
let lit, _ = Solver_internal.simplify_and_preproc_lit_ self.si lit in
let lit, _ = Solver_internal.simplify_and_preproc_lit self.si lit in
lit
(** {2 Main} *)
@ -171,16 +172,14 @@ let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
let add_clause_l self c p = add_clause self (CCArray.of_list c) p
let assert_terms self c =
let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
let c = CCList.map Lit.atom c in
let pr_c =
P.add_step self.proof @@ A.Rule_sat.sat_input_clause (Iter.of_list c)
P.add_step self.proof @@ Proof_sat.sat_input_clause (Iter.of_list c)
in
add_clause_l self c pr_c
let assert_term self t = assert_terms self [ t ]
exception Resource_exhausted = Sidekick_sat.Resource_exhausted
let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
?(should_stop = fun _ _ -> false) ~assumptions (self : t) : res =
Profile.with_ "smt-solver.solve" @@ fun () ->
@ -194,14 +193,14 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
if should_stop self !resource_counter then
raise_notrace Resource_exhausted
in
self.si.on_progress <- on_progress;
Event.on ~f:on_progress (SI.on_progress self.si);
let res =
match
Stat.incr self.count_solve;
Sat_solver.solve ~on_progress ~assumptions (solver self)
with
| Sat_solver.Sat _ when not self.si.complete ->
| Sat_solver.Sat _ when not (SI.is_complete self.si) ->
Log.debugf 1 (fun k ->
k
"(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason \
@ -212,14 +211,14 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
Log.debugf 5 (fun k ->
let ppc out n =
Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter N.pp)
(N.iter_class n)
Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter E_node.pp)
(E_node.iter_class n)
in
k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" (Util.pp_iter ppc)
(CC.all_classes @@ Solver_internal.cc self.si));
let m =
match self.si.last_model with
match SI.last_model self.si with
| Some m -> m
| None -> assert false
in

27
src/smt/solver.mli
View file

@ -14,32 +14,15 @@ type t
val registry : t -> Registry.t
(** A solver contains a registry so that theories can share data *)
type theory = Theory.t
type 'a theory_p = 'a Theory.p
val mk_theory :
name:string ->
create_and_setup:(Solver_internal.t -> 'th) ->
?push_level:('th -> unit) ->
?pop_levels:('th -> int -> unit) ->
unit ->
theory
Theory.t
(** Helper to create a theory. *)
(** Models
A model can be produced when the solver is found to be in a
satisfiable state after a call to {!solve}. *)
module Model : sig
type t
val empty : t
val mem : t -> term -> bool
val find : t -> term -> term option
val eval : t -> term -> term option
val pp : t Fmt.printer
end
(* TODO *)
module Unknown : sig
type t
@ -65,7 +48,7 @@ val create :
?size:[ `Big | `Tiny | `Small ] ->
(* TODO? ?config:Config.t -> *)
proof:proof_trace ->
theories:theory list ->
theories:Theory.t list ->
Term.store ->
unit ->
t
@ -82,15 +65,15 @@ val create :
@param theories theories to load from the start. Other theories
can be added using {!add_theory}. *)
val add_theory : t -> theory -> unit
val add_theory : t -> Theory.t -> unit
(** Add a theory to the solver. This should be called before
any call to {!solve} or to {!add_clause} and the likes (otherwise
the theory will have a partial view of the problem). *)
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_p : t -> 'a Theory.p -> 'a
(** Add the given theory and obtain its state *)
val add_theory_l : t -> theory list -> unit
val add_theory_l : t -> Theory.t list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
(** [mk_lit_t _ ~sign t] returns [lit'],

97
src/smt/solver_internal.ml
View file

@ -1,7 +1,6 @@
open Sigs
module Proof_rules = Sidekick_core.Proof_sat
module P_core_rules = Sidekick_core.Proof_core
module N = Sidekick_cc.E_node
module Ty = Term
open struct
@ -46,7 +45,7 @@ type t = {
cc: CC.t; (** congruence closure *)
proof: proof_trace; (** proof logger *)
registry: Registry.t;
mutable on_progress: unit -> unit;
on_progress: (unit, unit) Event.Emitter.t;
mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_th_combination:
@ -69,7 +68,10 @@ type t = {
}
and preprocess_hook = t -> preprocess_actions -> term -> unit
and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option
and model_ask_hook =
recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option
and model_completion_hook = t -> add:(term -> term -> unit) -> unit
type solver = t
@ -172,8 +174,7 @@ let preprocess_term_ (self : t) (t0 : term) : unit =
preproc_rec_ t0
(* simplify literal, then preprocess the result *)
let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : Lit.t * step_id option
=
let simplify_and_preproc_lit (self : t) (lit : Lit.t) : Lit.t * step_id option =
let t = Lit.term lit in
let sign = Lit.sign lit in
let u, pr =
@ -191,7 +192,7 @@ let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : Lit.t * step_id option
let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit =
let (module A) = acts in
(* make sure the literal is preprocessed *)
let lit, _ = simplify_and_preproc_lit_ self lit in
let lit, _ = simplify_and_preproc_lit self lit in
let sign = Lit.sign lit in
A.add_decision_lit (Lit.abs lit) sign
@ -210,7 +211,7 @@ module Preprocess_clause (A : ARR) = struct
(* simplify a literal, then preprocess it *)
let[@inline] simp_lit lit =
let lit, pr = simplify_and_preproc_lit_ self lit in
let lit, pr = simplify_and_preproc_lit self lit in
Option.iter (fun pr -> steps := pr :: !steps) pr;
lit
in
@ -233,8 +234,8 @@ end
module PC_list = Preprocess_clause (CCList)
module PC_arr = Preprocess_clause (CCArray)
let preprocess_clause_ = PC_list.top
let preprocess_clause_iarray_ = PC_arr.top
let preprocess_clause = PC_list.top
let preprocess_clause_array = PC_arr.top
module type PERFORM_ACTS = sig
type t
@ -250,7 +251,7 @@ module Perform_delayed (A : PERFORM_ACTS) = struct
let act = Queue.pop self.delayed_actions in
match act with
| DA_add_clause { c; pr = pr_c; keep } ->
let c', pr_c' = preprocess_clause_ self c pr_c in
let c', pr_c' = preprocess_clause self c pr_c in
A.add_clause self acts ~keep c' pr_c'
| DA_add_lit { default_pol; lit } ->
preprocess_term_ self (Lit.term lit);
@ -270,11 +271,11 @@ module Perform_delayed_th = Perform_delayed (struct
end)
let[@inline] add_clause_temp self _acts c (proof : step_id) : unit =
let c, proof = preprocess_clause_ self c proof in
let c, proof = preprocess_clause self c proof in
delayed_add_clause self ~keep:false c proof
let[@inline] add_clause_permanent self _acts c (proof : step_id) : unit =
let c, proof = preprocess_clause_ self c proof in
let c, proof = preprocess_clause self c proof in
delayed_add_clause self ~keep:true c proof
let[@inline] mk_lit _ ?sign t : lit = Lit.atom ?sign t
@ -284,7 +285,7 @@ let[@inline] add_lit self _acts ?default_pol lit =
let add_lit_t self _acts ?sign t =
let lit = Lit.atom ?sign t in
let lit, _ = simplify_and_preproc_lit_ self lit in
let lit, _ = simplify_and_preproc_lit self lit in
delayed_add_lit self lit
let on_final_check self f = self.on_final_check <- f :: self.on_final_check
@ -292,6 +293,7 @@ let on_final_check self f = self.on_final_check <- f :: self.on_final_check
let on_partial_check self f =
self.on_partial_check <- f :: self.on_partial_check
let on_progress self = Event.of_emitter self.on_progress
let on_cc_new_term self f = Event.on (CC.on_new_term (cc self)) ~f
let on_cc_pre_merge self f = Event.on (CC.on_pre_merge (cc self)) ~f
let on_cc_post_merge self f = Event.on (CC.on_post_merge (cc self)) ~f
@ -301,11 +303,13 @@ let on_cc_is_subterm self f = Event.on (CC.on_is_subterm (cc self)) ~f
let cc_add_term self t = CC.add_term (cc self) t
let cc_mem_term self t = CC.mem_term (cc self) t
let cc_find self n = CC.find (cc self) n
let is_complete self = self.complete
let last_model self = self.last_model
let cc_are_equal self t1 t2 =
let n1 = cc_add_term self t1 in
let n2 = cc_add_term self t2 in
N.equal (cc_find self n1) (cc_find self n2)
E_node.equal (cc_find self n1) (cc_find self n2)
let cc_resolve_expl self e : lit list * _ =
let r = CC.explain_expl (cc self) e in
@ -337,19 +341,6 @@ let rec pop_lvls_ n = function
r.pop_levels r.st n;
pop_lvls_ n r.next
let push_level (self : t) : unit =
self.level <- 1 + self.level;
CC.push_level (cc self);
push_lvl_ self.th_states
let pop_levels (self : t) n : unit =
self.last_model <- None;
self.level <- self.level - n;
CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states
let n_levels self = self.level
(** {2 Model construction and theory combination} *)
(* make model from the congruence closure *)
@ -372,7 +363,7 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
CC.get_model_for_each_class cc (fun (_, ts, v) ->
Iter.iter
(fun n ->
let t = N.term n in
let t = E_node.term n in
M.replace model t v)
ts);
*)
@ -390,20 +381,20 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
List.iter complete_with model_complete;
(* compute a value for [n]. *)
let rec val_for_class (n : N.t) : term =
Log.debugf 5 (fun k -> k "val-for-term %a" N.pp n);
let rec val_for_class (n : E_node.t) : term =
Log.debugf 5 (fun k -> k "val-for-term %a" E_node.pp n);
let repr = CC.find cc n in
Log.debugf 5 (fun k -> k "val-for-term.repr %a" N.pp repr);
Log.debugf 5 (fun k -> k "val-for-term.repr %a" E_node.pp repr);
(* see if a value is found already (always the case if it's a boolean) *)
match M.get model (N.term repr) with
match M.get model (E_node.term repr) with
| Some t_val ->
Log.debugf 5 (fun k -> k "cached val is %a" Term.pp_debug t_val);
t_val
| None ->
(* try each model hook *)
let rec try_hooks_ = function
| [] -> N.term repr
| [] -> E_node.term repr
| h :: hooks ->
(match h ~recurse:(fun _ n -> val_for_class n) self repr with
| None -> try_hooks_ hooks
@ -415,15 +406,15 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
(* FIXME: the more complete version?
match
(* look for a value in the model for any term in the class *)
N.iter_class repr
|> Iter.find_map (fun n -> M.get model (N.term n))
E_node.iter_class repr
|> Iter.find_map (fun n -> M.get model (E_node.term n))
with
| Some v -> v
| None -> try_hooks_ model_ask_hooks
*)
in
M.replace model (N.term repr) t_val;
M.replace model (E_node.term repr) t_val;
(* be sure to cache the value *)
Log.debugf 5 (fun k -> k "val is %a" Term.pp_debug t_val);
t_val
@ -433,11 +424,11 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
CC.all_classes cc (fun repr ->
let t_val = val_for_class repr in
(* value for this class *)
N.iter_class repr (fun u ->
let t_u = N.term u in
if (not (N.equal u repr)) && not (Term.equal t_u t_val) then
E_node.iter_class repr (fun u ->
let t_u = E_node.term u in
if (not (E_node.equal u repr)) && not (Term.equal t_u t_val) then
M.replace model t_u t_val));
Model.Map model
Model.Internal_.of_tbl model
(* do theory combination using the congruence closure. Each theory
can merge classes, *)
@ -557,7 +548,7 @@ let check_ ~final (self : t) (acts : sat_acts) =
in
let iter = iter_atoms_ acts in
Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter));
self.on_progress ();
Event.emit self.on_progress ();
assert_lits_ ~final self acts iter;
Profile.exit pb
@ -569,6 +560,28 @@ let[@inline] partial_check (self : t) (acts : Sidekick_sat.acts) : unit =
let[@inline] final_check (self : t) (acts : Sidekick_sat.acts) : unit =
check_ ~final:true self acts
let push_level self : unit =
self.level <- 1 + self.level;
CC.push_level (cc self);
push_lvl_ self.th_states
let pop_levels self n : unit =
self.last_model <- None;
self.level <- self.level - n;
CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states
let n_levels self = self.level
let to_sat_plugin (self : t) : (module Sidekick_sat.PLUGIN) =
(module struct
let has_theory = true
let push_level () = push_level self
let pop_levels n = pop_levels self n
let partial_check acts = partial_check self acts
let final_check acts = final_check self acts
end)
let declare_pb_is_incomplete self =
if self.complete then Log.debug 1 "(solver.declare-pb-is-incomplete)";
self.complete <- false
@ -587,7 +600,7 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
stat;
simp = Simplify.create tst ~proof;
last_model = None;
on_progress = (fun () -> ());
on_progress = Event.Emitter.create ();
preprocess = [];
model_ask = [];
model_complete = [];

30
src/smt/solver_internal.mli
View file

@ -35,12 +35,14 @@ include Sidekick_sigs.BACKTRACKABLE0 with type t := t
(** {3 Interface to SAT} *)
include Sidekick_sat.PLUGIN_CDCL_T with type t := t
val to_sat_plugin : t -> (module Sidekick_sat.PLUGIN)
(** {3 Simplifiers} *)
type simplify_hook = Simplify.hook
val simplifier : t -> Simplify.t
val add_simplifier : t -> Simplify.hook -> unit
(** Add a simplifier hook for preprocessing. *)
@ -90,6 +92,12 @@ type preprocess_hook = t -> preprocess_actions -> term -> unit
val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *)
val preprocess_clause : t -> lit list -> step_id -> lit list * step_id
val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id
val simplify_and_preproc_lit : t -> lit -> lit * step_id option
(** Simplify literal then preprocess it *)
(** {3 hooks for the theory} *)
val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a
@ -245,6 +253,26 @@ val on_model :
?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit
(** Add model production/completion hooks. *)
val on_progress : t -> (unit, unit) Event.t
val is_complete : t -> bool
(** Are we still in a complete logic fragment? *)
val last_model : t -> Model.t option
(** {2 Delayed actions} *)
module type PERFORM_ACTS = sig
type t
val add_clause : solver -> t -> keep:bool -> lit list -> step_id -> unit
val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit
end
module Perform_delayed (A : PERFORM_ACTS) : sig
val top : t -> A.t -> unit
end
val add_theory_state :
st:'a ->
push_level:('a -> unit) ->