From b97582daa26e875e31e7e72f9a10c8d3d7fb8bf4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 30 Jul 2022 00:19:29 -0400 Subject: [PATCH] wip: refactor(smt): remove layers of functors, split into modules --- src/smt/Sidekick_smt_solver.ml | 14 + src/smt/dune | 7 + src/smt/model.ml | 24 ++ src/smt/registry.ml | 37 ++ src/smt/registry.mli | 14 + src/smt/sigs.ml | 48 +++ src/smt/simplify.ml | 81 +++++ src/smt/simplify.mli | 39 +++ src/smt/solver.ml | 261 ++++++++++++++ src/smt/solver.mli | 189 ++++++++++ src/smt/solver_internal.ml | 608 +++++++++++++++++++++++++++++++++ src/smt/solver_internal.mli | 256 ++++++++++++++ src/smt/th_key.ml.bak | 145 ++++++++ src/smt/theory.ml | 44 +++ 14 files changed, 1767 insertions(+) create mode 100644 src/smt/Sidekick_smt_solver.ml create mode 100644 src/smt/dune create mode 100644 src/smt/model.ml create mode 100644 src/smt/registry.ml create mode 100644 src/smt/registry.mli create mode 100644 src/smt/sigs.ml create mode 100644 src/smt/simplify.ml create mode 100644 src/smt/simplify.mli create mode 100644 src/smt/solver.ml create mode 100644 src/smt/solver.mli create mode 100644 src/smt/solver_internal.ml create mode 100644 src/smt/solver_internal.mli create mode 100644 src/smt/th_key.ml.bak create mode 100644 src/smt/theory.ml diff --git a/src/smt/Sidekick_smt_solver.ml b/src/smt/Sidekick_smt_solver.ml new file mode 100644 index 00000000..9ab1530d --- /dev/null +++ b/src/smt/Sidekick_smt_solver.ml @@ -0,0 +1,14 @@ +(** Core of the SMT solver using Sidekick_sat + + Sidekick_sat (in src/sat/) is a modular SAT solver in + pure OCaml. + + This builds a SMT solver on top of it. +*) + +module Sigs = Sigs +module Model = Model +module Registry = Registry +module Simplify = Simplify +module Solver_internal = Solver_internal +module Solver = Solver diff --git a/src/smt/dune b/src/smt/dune new file mode 100644 index 00000000..0e86c9da --- /dev/null +++ b/src/smt/dune @@ -0,0 +1,7 @@ +(library + (name Sidekick_smt_solver) + (public_name sidekick.smt-solver) + (synopsis "main SMT solver") + (libraries containers iter sidekick.core sidekick.util sidekick.cc + sidekick.sat) + (flags :standard -w +32 -open Sidekick_util)) diff --git a/src/smt/model.ml b/src/smt/model.ml new file mode 100644 index 00000000..34cba314 --- /dev/null +++ b/src/smt/model.ml @@ -0,0 +1,24 @@ +open Sigs + +type t = Empty | Map of term Term.Tbl.t + +let empty = Empty + +let mem = function + | Empty -> fun _ -> false + | Map tbl -> Term.Tbl.mem tbl + +let find = function + | Empty -> fun _ -> None + | Map tbl -> Term.Tbl.get tbl + +let eval = find + +let pp out = function + | Empty -> Fmt.string out "(model)" + | Map tbl -> + let pp_pair out (t, v) = + Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp_debug t Term.pp_debug v + in + Fmt.fprintf out "(@[model@ %a@])" (Util.pp_iter pp_pair) + (Term.Tbl.to_iter tbl) diff --git a/src/smt/registry.ml b/src/smt/registry.ml new file mode 100644 index 00000000..f2450d1b --- /dev/null +++ b/src/smt/registry.ml @@ -0,0 +1,37 @@ + + (* registry keys *) + module type KEY = sig + type elt + + val id : int + + exception E of elt + end + + type 'a key = (module KEY with type elt = 'a) + type t = { tbl: exn Util.Int_tbl.t } [@@unboxed] + + let create () : t = { tbl = Util.Int_tbl.create 8 } + let n_ = ref 0 + + let create_key (type a) () : a key = + let id = !n_ in + incr n_; + let module K = struct + type elt = a + + exception E of a + + let id = id + end in + (module K) + + let get (type a) (self : t) (k : a key) : _ option = + let (module K : KEY with type elt = a) = k in + match Util.Int_tbl.get self.tbl K.id with + | Some (K.E x) -> Some x + | _ -> None + + let set (type a) (self : t) (k : a key) (v : a) : unit = + let (module K) = k in + Util.Int_tbl.replace self.tbl K.id (K.E v) diff --git a/src/smt/registry.mli b/src/smt/registry.mli new file mode 100644 index 00000000..0e41bcac --- /dev/null +++ b/src/smt/registry.mli @@ -0,0 +1,14 @@ + + +(** Registry to extract values *) + + type t + type 'a key + + val create_key : unit -> 'a key + (** Call this statically, typically at program initialization, for + each distinct key. *) + + val create : unit -> t + val get : t -> 'a key -> 'a option + val set : t -> 'a key -> 'a -> unit diff --git a/src/smt/sigs.ml b/src/smt/sigs.ml new file mode 100644 index 00000000..fb0ba9b6 --- /dev/null +++ b/src/smt/sigs.ml @@ -0,0 +1,48 @@ +(** Signature for the main SMT solver types. + + Theories and concrete solvers rely on an environment that defines + several important types: + + - sorts + - terms (to represent logic expressions and formulas) + - a congruence closure instance + - a bridge to some SAT solver + + In this module we collect signatures defined elsewhere and define + the module types for the main SMT solver. +*) + +include Sidekick_core +module CC = Sidekick_cc.CC +module E_node = Sidekick_cc.E_node +module CC_expl = Sidekick_cc.Expl + +type term = Term.t +type ty = term +type value = Term.t +type lit = Lit.t +type term_store = Term.store +type proof_trace = Proof_trace.t +type step_id = Proof_step.id + +(* actions from the sat solver *) +type sat_acts = Sidekick_sat.acts + +type th_combination_conflict = { + lits: lit list; + semantic: (bool * term * term) list; + (* set of semantic eqns/diseqns (ie true only in current model) *) +} +(** Conflict obtained during theory combination. It involves equalities + merged because of the current model so it's not a "true" conflict + and doesn't need to kill the current trail. *) + +(** Argument to pass to the functor {!Make} in order to create a + new Msat-based SMT solver. *) +module type ARG = sig + val view_as_cc : Sidekick_cc.view_as_cc + + val is_valid_literal : Term.t -> bool + (** Is this a valid boolean literal? (e.g. is it a closed term, not inside + a quantifier) *) +end diff --git a/src/smt/simplify.ml b/src/smt/simplify.ml new file mode 100644 index 00000000..2bbd3da8 --- /dev/null +++ b/src/smt/simplify.ml @@ -0,0 +1,81 @@ +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 diff --git a/src/smt/simplify.mli b/src/smt/simplify.mli new file mode 100644 index 00000000..4ecccd29 --- /dev/null +++ b/src/smt/simplify.mli @@ -0,0 +1,39 @@ +(** 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 diff --git a/src/smt/solver.ml b/src/smt/solver.ml new file mode 100644 index 00000000..f4741fb8 --- /dev/null +++ b/src/smt/solver.ml @@ -0,0 +1,261 @@ +open Sigs + +open struct + module P = Proof_trace + module Rule_ = Proof_core +end + +(* TODO + let mk_cc_acts_ (pr : P.t) (a : sat_acts) : CC.actions = + let (module A) = a in + + (module struct + module T = T + module Lit = Lit + + type nonrec lit = lit + type nonrec term = term + type nonrec proof_trace = Proof_trace.t + type nonrec step_id = step_id + + let proof_trace () = pr + let[@inline] raise_conflict lits (pr : step_id) = A.raise_conflict lits pr + + let[@inline] raise_semantic_conflict lits semantic = + raise (Semantic_conflict { lits; semantic }) + + let[@inline] propagate lit ~reason = + let reason = Sidekick_sat.Consequence reason in + A.propagate lit reason + end) +*) + +module Sat_solver = Sidekick_sat.Make_cdcl_t (Solver_internal) +(** the parametrized SAT Solver *) + +(** {2 Result} *) + +module Unknown = struct + type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop + + let pp out = function + | U_timeout -> Fmt.string out {|"timeout"|} + | U_max_depth -> Fmt.string out {|"max depth reached"|} + | U_incomplete -> Fmt.string out {|"incomplete fragment"|} + | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|} +end +[@@ocaml.warning "-37"] + +type res = + | Sat of Model.t + | Unsat of { + unsat_core: unit -> lit Iter.t; + (** Unsat core (subset of assumptions), or empty *) + unsat_step_id: unit -> step_id option; + (** Proof step for the empty clause *) + } + | Unknown of Unknown.t + (** Result of solving for the current set of clauses *) + +(* main solver state *) +type t = { + si: Solver_internal.t; + solver: Sat_solver.t; + mutable last_res: res option; + stat: Stat.t; + proof: P.t; + count_clause: int Stat.counter; + count_solve: int Stat.counter; (* config: Config.t *) +} + +type solver = t + +(** {2 Main} *) + +type theory = Theory.t + +let mk_theory = Theory.make + +let add_theory_p (type a) (self : t) (th : a Theory.p) : a = + let (module Th) = th in + Log.debugf 2 (fun k -> k "(@[smt-solver.add-theory@ :name %S@])" Th.name); + let st = Th.create_and_setup self.si in + (* add push/pop to the internal solver *) + Solver_internal.add_theory_state self.si ~st ~push_level:Th.push_level + ~pop_levels:Th.pop_levels; + st + +let add_theory (self : t) (th : theory) : unit = + let (module Th) = th in + ignore (add_theory_p self (module Th)) + +let add_theory_l self = List.iter (add_theory self) + +(* create a new solver *) +let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t = + Log.debug 5 "smt-solver.create"; + let si = Solver_internal.create arg ~stat ~proof tst () in + let self = + { + si; + proof; + last_res = None; + solver = Sat_solver.create ~proof ?size ~stat si; + stat; + count_clause = Stat.mk_int stat "solver.add-clause"; + count_solve = Stat.mk_int stat "solver.solve"; + } + in + add_theory_l self theories; + (* assert [true] and [not false] *) + (let tst = Solver_internal.tst self.si in + let t_true = Term.true_ tst in + Sat_solver.add_clause self.solver + [ Lit.atom t_true ] + (P.add_step self.proof @@ Rule_.lemma_true t_true)); + self + +let[@inline] solver self = self.solver +let[@inline] cc self = Solver_internal.cc self.si +let[@inline] stats self = self.stat +let[@inline] tst self = Solver_internal.tst self.si +let[@inline] proof self = self.proof +let[@inline] last_res self = self.last_res +let[@inline] registry self = Solver_internal.registry self.si +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 + +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 + lit + +(** {2 Main} *) + +let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self) + +(* add [c], without preprocessing its literals *) +let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit = + Stat.incr self.count_clause; + reset_last_res_ self; + Log.debugf 50 (fun k -> + k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c); + let pb = Profile.begin_ "add-clause" in + Sat_solver.add_clause_a self.solver (c :> lit array) proof; + Profile.exit pb + +let add_clause_nopreproc_l_ self c p = + add_clause_nopreproc_ self (CCArray.of_list c) p + +module Perform_delayed_ = Solver_internal.Perform_delayed (struct + type nonrec t = t + + let add_clause _si solver ~keep:_ c pr : unit = + add_clause_nopreproc_l_ solver c pr + + let add_lit _si solver ?default_pol lit : unit = + Sat_solver.add_lit solver.solver ?default_pol lit +end) + +let add_clause (self : t) (c : lit array) (proof : step_id) : unit = + let c, proof = preprocess_clause_ self c proof in + add_clause_nopreproc_ self c proof; + Perform_delayed_.top self.si self; + (* finish preproc *) + () + +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 pr_c = + P.add_step self.proof @@ A.Rule_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 () -> + let do_on_exit () = List.iter (fun f -> f ()) on_exit in + + let on_progress = + let resource_counter = ref 0 in + fun () -> + incr resource_counter; + on_progress self; + if should_stop self !resource_counter then + raise_notrace Resource_exhausted + in + self.si.on_progress <- on_progress; + + 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 -> + Log.debugf 1 (fun k -> + k + "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason \ + incomplete-fragment@])"); + Unknown Unknown.U_incomplete + | Sat_solver.Sat _ -> + Log.debug 1 "(sidekick.smt-solver: SAT)"; + + Log.debugf 5 (fun k -> + let ppc out n = + Fmt.fprintf out "{@[class@ %a@]}" (Util.pp_iter N.pp) + (N.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 + | Some m -> m + | None -> assert false + in + (* TODO: check model *) + let _ = check in + + do_on_exit (); + Sat m + | Sat_solver.Unsat (module UNSAT) -> + let unsat_core () = UNSAT.unsat_assumptions () in + let unsat_step_id () = Some (UNSAT.unsat_proof ()) in + do_on_exit (); + Unsat { unsat_core; unsat_step_id } + | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop + in + self.last_res <- Some res; + res + +let push_assumption self a = + reset_last_res_ self; + Sat_solver.push_assumption self.solver a + +let pop_assumptions self n = + reset_last_res_ self; + Sat_solver.pop_assumptions self.solver n + +type propagation_result = + | PR_sat + | PR_conflict of { backtracked: int } + | PR_unsat of { unsat_core: unit -> lit Iter.t } + +let check_sat_propagations_only ~assumptions self : propagation_result = + reset_last_res_ self; + match Sat_solver.check_sat_propagations_only ~assumptions self.solver with + | Sat_solver.PR_sat -> PR_sat + | Sat_solver.PR_conflict { backtracked } -> PR_conflict { backtracked } + | Sat_solver.PR_unsat (module UNSAT) -> + let unsat_core () = UNSAT.unsat_assumptions () in + PR_unsat { unsat_core } diff --git a/src/smt/solver.mli b/src/smt/solver.mli new file mode 100644 index 00000000..b645adb6 --- /dev/null +++ b/src/smt/solver.mli @@ -0,0 +1,189 @@ +(** Main solver type, user facing. + + This is the solver a user of sidekick can see, after instantiating + everything. The user can add some theories, clauses, etc. and asks + the solver to check satisfiability. + + Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) + +open Sigs + +type t +(** The solver's state. *) + +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 +(** 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 + + val pp : t CCFormat.printer + + (* + type unknown = + | U_timeout + | U_incomplete + *) +end + +(** {3 Main API} *) + +val stats : t -> Stat.t +val tst : t -> Term.store +val proof : t -> proof_trace + +val create : + (module ARG) -> + ?stat:Stat.t -> + ?size:[ `Big | `Tiny | `Small ] -> + (* TODO? ?config:Config.t -> *) + proof:proof_trace -> + theories:theory list -> + Term.store -> + unit -> + t +(** Create a new solver. + + It needs a term state and a type state to manipulate terms and types. + All terms and types interacting with this solver will need to come + from these exact states. + + @param store_proof if true, proofs from the SAT solver and theories + are retained and potentially accessible after {!solve} + returns UNSAT. + @param size influences the size of initial allocations. + @param theories theories to load from the start. Other theories + can be added using {!add_theory}. *) + +val add_theory : t -> theory -> 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 +(** Add the given theory and obtain its state *) + +val add_theory_l : t -> theory list -> unit + +val mk_lit_t : t -> ?sign:bool -> term -> lit +(** [mk_lit_t _ ~sign t] returns [lit'], + where [lit'] is [preprocess(lit)] and [lit] is + an internal representation of [± t]. + + The proof of [|- lit = lit'] is directly added to the solver's proof. *) + +val add_clause : t -> lit array -> step_id -> unit +(** [add_clause solver cs] adds a boolean clause to the solver. + Subsequent calls to {!solve} will need to satisfy this clause. *) + +val add_clause_l : t -> lit list -> step_id -> unit +(** Add a clause to the solver, given as a list. *) + +val assert_terms : t -> term list -> unit +(** Helper that turns each term into an atom, before adding the result + to the solver as an assertion *) + +val assert_term : t -> term -> unit +(** Helper that turns the term into an atom, before adding the result + to the solver as a unit clause assertion *) + +(** Result of solving for the current set of clauses *) +type res = + | Sat of Model.t (** Satisfiable *) + | Unsat of { + unsat_core: unit -> lit Iter.t; + (** Unsat core (subset of assumptions), or empty *) + unsat_step_id: unit -> step_id option; + (** Proof step for the empty clause *) + } (** Unsatisfiable *) + | Unknown of Unknown.t + (** Unknown, obtained after a timeout, memory limit, etc. *) + +(* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *) + +val solve : + ?on_exit:(unit -> unit) list -> + ?check:bool -> + ?on_progress:(t -> unit) -> + ?should_stop:(t -> int -> bool) -> + assumptions:lit list -> + t -> + res +(** [solve s] checks the satisfiability of the clauses added so far to [s]. + @param check if true, the model is checked before returning. + @param on_progress called regularly during solving. + @param assumptions a set of atoms held to be true. The unsat core, + if any, will be a subset of [assumptions]. + @param should_stop a callback regularly called with the solver, + and with a number of "steps" done since last call. The exact notion + of step is not defined, but is guaranteed to increase regularly. + The function should return [true] if it judges solving + must stop (returning [Unknown]), [false] if solving can proceed. + @param on_exit functions to be run before this returns *) + +val last_res : t -> res option +(** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *) + +val push_assumption : t -> lit -> unit +(** Pushes an assumption onto the assumption stack. It will remain + there until it's pop'd by {!pop_assumptions}. *) + +val pop_assumptions : t -> int -> unit +(** [pop_assumptions solver n] removes [n] assumptions from the stack. + It removes the assumptions that were the most + recently added via {!push_assumptions}. + Note that {!check_sat_propagations_only} can call this if it meets + a conflict. *) + +type propagation_result = + | PR_sat + | PR_conflict of { backtracked: int } + | PR_unsat of { unsat_core: unit -> lit Iter.t } + +val check_sat_propagations_only : + assumptions:lit list -> t -> propagation_result +(** [check_sat_propagations_only solver] uses assumptions (including + the [assumptions] parameter, and atoms previously added via {!push_assumptions}) + and boolean+theory propagation to quickly assess satisfiability. + It is not complete; calling {!solve} is required to get an accurate + result. + @returns one of: + + - [PR_sat] if the current state seems satisfiable + - [PR_conflict {backtracked=n}] if a conflict was found and resolved, + leading to backtracking [n] levels of assumptions + - [PR_unsat …] if the assumptions were found to be unsatisfiable, with + the given core. + *) + +(* TODO: allow on_progress to return a bool to know whether to stop? *) + +val pp_stats : t CCFormat.printer +(** Print some statistics. What it prints exactly is unspecified. *) diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml new file mode 100644 index 00000000..db0995e1 --- /dev/null +++ b/src/smt/solver_internal.ml @@ -0,0 +1,608 @@ +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 + module P = Proof_trace + module Rule_ = Proof_core +end + +type th_states = + | Ths_nil + | Ths_cons : { + st: 'a; + push_level: 'a -> unit; + pop_levels: 'a -> int -> unit; + next: th_states; + } + -> th_states + +(* actions from the sat solver *) +type sat_acts = Sidekick_sat.acts +type theory_actions = sat_acts +type simplify_hook = Simplify.hook + +module type PREPROCESS_ACTS = sig + val proof : proof_trace + val mk_lit : ?sign:bool -> term -> lit + val add_clause : lit list -> step_id -> unit + val add_lit : ?default_pol:bool -> lit -> unit +end + +type preprocess_actions = (module PREPROCESS_ACTS) + +module Registry = Registry + +(* delayed actions. We avoid doing them on the spot because, when + triggered by a theory, they might go back to the theory "too early". *) +type delayed_action = + | DA_add_clause of { c: lit list; pr: step_id; keep: bool } + | DA_add_lit of { default_pol: bool option; lit: lit } + +type t = { + tst: Term.store; (** state for managing terms *) + cc: CC.t; (** congruence closure *) + proof: proof_trace; (** proof logger *) + registry: Registry.t; + mutable on_progress: unit -> unit; + 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: + (t -> theory_actions -> (term * value) Iter.t) list; + mutable preprocess: preprocess_hook list; + mutable model_ask: model_ask_hook list; + mutable model_complete: model_completion_hook list; + simp: Simplify.t; + preprocessed: unit Term.Tbl.t; + delayed_actions: delayed_action Queue.t; + mutable last_model: Model.t option; + mutable th_states: th_states; (** Set of theories *) + mutable level: int; + mutable complete: bool; + stat: Stat.t; + count_axiom: int Stat.counter; + count_preprocess_clause: int Stat.counter; + count_conflict: int Stat.counter; + count_propagate: int Stat.counter; +} + +and preprocess_hook = t -> preprocess_actions -> term -> unit +and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option +and model_completion_hook = t -> add:(term -> term -> unit) -> unit + +type solver = t + +let[@inline] cc (self : t) = self.cc +let[@inline] tst self = self.tst +let[@inline] proof self = self.proof +let stats self = self.stat + +let[@inline] has_delayed_actions self = + not (Queue.is_empty self.delayed_actions) + +let registry self = self.registry +let simplifier self = self.simp +let simplify_t self (t : Term.t) : _ option = Simplify.normalize self.simp t +let simp_t self (t : Term.t) : Term.t * _ = Simplify.normalize_t self.simp t +let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f + +let on_th_combination self f = + self.on_th_combination <- f :: self.on_th_combination + +let on_preprocess self f = self.preprocess <- f :: self.preprocess + +let on_model ?ask ?complete self = + Option.iter (fun f -> self.model_ask <- f :: self.model_ask) ask; + Option.iter + (fun f -> self.model_complete <- f :: self.model_complete) + complete; + () + +let[@inline] raise_conflict self (acts : theory_actions) c proof : 'a = + let (module A) = acts in + Stat.incr self.count_conflict; + A.raise_conflict c proof + +let[@inline] propagate self (acts : theory_actions) p ~reason : unit = + let (module A) = acts in + Stat.incr self.count_propagate; + A.propagate p (Sidekick_sat.Consequence reason) + +let[@inline] propagate_l self acts p cs proof : unit = + propagate self acts p ~reason:(fun () -> cs, proof) + +let add_sat_clause_ self (acts : theory_actions) ~keep lits (proof : step_id) : + unit = + let (module A) = acts in + Stat.incr self.count_axiom; + A.add_clause ~keep lits proof + +let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) : unit + = + let (module A) = acts in + A.add_lit ?default_pol lit + +let delayed_add_lit (self : t) ?default_pol (lit : Lit.t) : unit = + Queue.push (DA_add_lit { default_pol; lit }) self.delayed_actions + +let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit = + Queue.push (DA_add_clause { c; pr; keep }) self.delayed_actions + +let preprocess_term_ (self : t) (t0 : term) : unit = + let module A = struct + let proof = self.proof + let mk_lit ?sign t : Lit.t = Lit.atom ?sign t + let add_lit ?default_pol lit : unit = delayed_add_lit self ?default_pol lit + let add_clause c pr : unit = delayed_add_clause self ~keep:true c pr + end in + let acts = (module A : PREPROCESS_ACTS) in + + (* how to preprocess a term and its subterms *) + let rec preproc_rec_ t = + if not (Term.Tbl.mem self.preprocessed t) then ( + Term.Tbl.add self.preprocessed t (); + + (* process sub-terms first *) + Term.iter_shallow t ~f:(fun _inb u -> preproc_rec_ u); + + Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp_debug t); + + (* signal boolean subterms, so as to decide them + in the SAT solver *) + if Ty.is_bool (Term.ty t) then ( + Log.debugf 5 (fun k -> + k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp_debug + t); + + (* make a literal *) + let lit = Lit.atom t in + (* ensure that SAT solver has a boolean atom for [u] *) + delayed_add_lit self lit; + + (* also map [sub] to this atom in the congruence closure, for propagation *) + let cc = cc self in + CC.set_as_lit cc (CC.add_term cc t) lit + ); + + List.iter (fun f -> f self acts t) self.preprocess + ) + in + 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 t = Lit.term lit in + let sign = Lit.sign lit in + let u, pr = + match simplify_t self t with + | None -> t, None + | Some (u, pr_t_u) -> + Log.debugf 30 (fun k -> + k "(@[smt-solver.simplify@ :t %a@ :into %a@])" Term.pp_debug t + Term.pp_debug u); + u, Some pr_t_u + in + preprocess_term_ self u; + Lit.atom ~sign u, pr + +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 sign = Lit.sign lit in + A.add_decision_lit (Lit.abs lit) sign + +module type ARR = sig + type 'a t + + val map : ('a -> 'b) -> 'a t -> 'b t + val to_iter : 'a t -> 'a Iter.t +end + +module Preprocess_clause (A : ARR) = struct + (* preprocess a clause's literals, possibly emitting a proof + for the preprocessing. *) + let top (self : t) (c : lit A.t) (pr_c : step_id) : lit A.t * step_id = + let steps = ref [] in + + (* simplify a literal, then preprocess it *) + let[@inline] simp_lit lit = + let lit, pr = simplify_and_preproc_lit_ self lit in + Option.iter (fun pr -> steps := pr :: !steps) pr; + lit + in + let c' = A.map simp_lit c in + + let pr_c' = + if !steps = [] then + pr_c + else ( + Stat.incr self.count_preprocess_clause; + P.add_step self.proof + @@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c') + ~using:(Iter.of_list !steps) + ) + in + c', pr_c' +end +[@@inline] + +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 + +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) = struct + (* perform actions that were delayed *) + let top (self : t) (acts : A.t) : unit = + while not (Queue.is_empty self.delayed_actions) do + 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 + A.add_clause self acts ~keep c' pr_c' + | DA_add_lit { default_pol; lit } -> + preprocess_term_ self (Lit.term lit); + A.add_lit self acts ?default_pol lit + done +end +[@@inline] + +module Perform_delayed_th = Perform_delayed (struct + type t = theory_actions + + let add_clause self acts ~keep c pr : unit = + add_sat_clause_ self acts ~keep c pr + + let add_lit self acts ?default_pol lit : unit = + add_sat_lit_ self acts ?default_pol lit +end) + +let[@inline] add_clause_temp self _acts c (proof : step_id) : unit = + 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 + delayed_add_clause self ~keep:true c proof + +let[@inline] mk_lit _ ?sign t : lit = Lit.atom ?sign t + +let[@inline] add_lit self _acts ?default_pol lit = + delayed_add_lit self ?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 + delayed_add_lit self lit + +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_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 +let on_cc_conflict self f = Event.on (CC.on_conflict (cc self)) ~f +let on_cc_propagate self f = Event.on (CC.on_propagate (cc self)) ~f +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 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) + +let cc_resolve_expl self e : lit list * _ = + let r = CC.explain_expl (cc self) e in + r.lits, r.pr self.proof + +(* + let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e + + let cc_merge_t self acts t1 t2 e = + let cc_acts = mk_cc_acts_ self.proof acts in + cc_merge self cc_acts (cc_add_term self t1) (cc_add_term self t2) e + + let cc_raise_conflict_expl self acts e = + let cc_acts = mk_cc_acts_ self.proof acts in + CC.raise_conflict_from_expl (cc self) cc_acts e + *) + +(** {2 Interface with the SAT solver} *) + +let rec push_lvl_ = function + | Ths_nil -> () + | Ths_cons r -> + r.push_level r.st; + push_lvl_ r.next + +let rec pop_lvls_ n = function + | Ths_nil -> () + | Ths_cons r -> + 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 *) +let mk_model_ (self : t) (lits : lit Iter.t) : Model.t = + Log.debug 1 "(smt.solver.mk-model)"; + Profile.with_ "smt-solver.mk-model" @@ fun () -> + let module M = Term.Tbl in + let { cc; tst; model_ask = model_ask_hooks; model_complete; _ } = self in + + let model = M.create 128 in + + (* first, add all literals to the model using the given propositional model + [lits]. *) + lits (fun lit -> + let t, sign = Lit.signed_term lit in + M.replace model t (Term.bool_val tst sign)); + + (* populate with information from the CC *) + (* FIXME + CC.get_model_for_each_class cc (fun (_, ts, v) -> + Iter.iter + (fun n -> + let t = N.term n in + M.replace model t v) + ts); + *) + + (* complete model with theory specific values *) + let complete_with f = + f self ~add:(fun t u -> + if not (M.mem model t) then ( + Log.debugf 20 (fun k -> + k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp_debug t + Term.pp_debug u); + M.replace model t u + )) + in + 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 repr = CC.find cc n in + Log.debugf 5 (fun k -> k "val-for-term.repr %a" N.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 + | 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 + | h :: hooks -> + (match h ~recurse:(fun _ n -> val_for_class n) self repr with + | None -> try_hooks_ hooks + | Some t -> t) + in + + let t_val = + try_hooks_ model_ask_hooks + (* 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)) + with + | Some v -> v + | None -> try_hooks_ model_ask_hooks + *) + in + + M.replace model (N.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 + in + + (* map terms of each CC class to the value computed for their class. *) + 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 + M.replace model t_u t_val)); + Model.Map model + +(* do theory combination using the congruence closure. Each theory + can merge classes, *) +let check_th_combination_ (self : t) (_acts : theory_actions) lits : + (Model.t, th_combination_conflict) result = + (* FIXME + + (* enter model mode, disabling most of congruence closure *) + CC.with_model_mode cc @@ fun () -> + let set_val (t, v) : unit = + Log.debugf 50 (fun k -> + k "(@[solver.th-comb.cc-set-term-value@ %a@ :val %a@])" Term.pp_debug t + Term.pp_debug v); + CC.set_model_value cc t v + in + + (* obtain assignments from the hook, and communicate them to the CC *) + let add_th_values f : unit = + let vals = f self acts in + Iter.iter set_val vals + in + try + List.iter add_th_values self.on_th_combination; + CC.check cc; + let m = mk_model_ self in + Ok m + with Semantic_conflict c -> Error c + *) + let m = mk_model_ self lits in + Ok m + +(* call congruence closure, perform the actions it scheduled *) +let check_cc_with_acts_ (self : t) (acts : theory_actions) = + let (module A) = acts in + let cc = cc self in + match CC.check cc with + | Ok acts -> + List.iter + (function + | CC.Result_action.Act_propagate { lit; reason } -> + let reason = Sidekick_sat.Consequence reason in + A.propagate lit reason) + acts + | Error (CC.Result_action.Conflict (lits, pr)) -> A.raise_conflict lits pr + +(* handle a literal assumed by the SAT solver *) +let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t) + : unit = + Log.debugf 2 (fun k -> + k "(@[@{smt-solver.assume_lits@}%s[lvl=%d]@ %a@])" + (if final then + "[final]" + else + "") + self.level + (Util.pp_iter ~sep:"; " Lit.pp) + lits); + (* transmit to CC *) + let cc = cc self in + + if not final then CC.assert_lits cc lits; + (* transmit to theories. *) + check_cc_with_acts_ self acts; + if final then ( + List.iter (fun f -> f self acts lits) self.on_final_check; + check_cc_with_acts_ self acts; + + (match check_th_combination_ self acts lits with + | Ok m -> self.last_model <- Some m + | Error { lits; semantic } -> + (* bad model, we add a clause to remove it *) + Log.debugf 5 (fun k -> + k "(@[solver.th-comb.conflict@ :lits (@[%a@])@ :same-val (@[%a@])@])" + (Util.pp_list Lit.pp) lits + (Util.pp_list @@ Fmt.Dump.(triple bool Term.pp_debug Term.pp_debug)) + semantic); + + let c1 = List.rev_map Lit.neg lits in + let c2 = + semantic + |> List.rev_map (fun (sign, t, u) -> + let eqn = Term.eq self.tst t u in + let lit = Lit.atom ~sign:(not sign) eqn in + (* make sure to consider the new lit *) + add_lit self acts lit; + lit) + in + + let c = List.rev_append c1 c2 in + let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in + + Log.debugf 20 (fun k -> + k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])" + (Util.pp_list Lit.pp) c); + (* will add a delayed action *) + add_clause_temp self acts c pr); + + Perform_delayed_th.top self acts + ) else ( + List.iter (fun f -> f self acts lits) self.on_partial_check; + Perform_delayed_th.top self acts + ); + () + +let[@inline] iter_atoms_ (acts : theory_actions) : _ Iter.t = + fun f -> + let (module A) = acts in + A.iter_assumptions f + +(* propagation from the bool solver *) +let check_ ~final (self : t) (acts : sat_acts) = + let pb = + if final then + Profile.begin_ "solver.final-check" + else + Profile.null_probe + in + let iter = iter_atoms_ acts in + Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter)); + self.on_progress (); + assert_lits_ ~final self acts iter; + Profile.exit pb + +(* propagation from the bool solver *) +let[@inline] partial_check (self : t) (acts : Sidekick_sat.acts) : unit = + check_ ~final:false self acts + +(* perform final check of the model *) +let[@inline] final_check (self : t) (acts : Sidekick_sat.acts) : unit = + check_ ~final:true self acts + +let declare_pb_is_incomplete self = + if self.complete then Log.debug 1 "(solver.declare-pb-is-incomplete)"; + self.complete <- false + +let add_theory_state ~st ~push_level ~pop_levels (self : t) = + self.th_states <- + Ths_cons { st; push_level; pop_levels; next = self.th_states } + +let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t = + let self = + { + tst; + cc = CC.create (module A : CC.ARG) ~size:`Big tst proof; + proof; + th_states = Ths_nil; + stat; + simp = Simplify.create tst ~proof; + last_model = None; + on_progress = (fun () -> ()); + preprocess = []; + model_ask = []; + model_complete = []; + registry = Registry.create (); + preprocessed = Term.Tbl.create 32; + delayed_actions = Queue.create (); + count_axiom = Stat.mk_int stat "solver.th-axioms"; + count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause"; + count_propagate = Stat.mk_int stat "solver.th-propagations"; + count_conflict = Stat.mk_int stat "solver.th-conflicts"; + on_partial_check = []; + on_final_check = []; + on_th_combination = []; + level = 0; + complete = true; + } + in + self diff --git a/src/smt/solver_internal.mli b/src/smt/solver_internal.mli new file mode 100644 index 00000000..508df6fc --- /dev/null +++ b/src/smt/solver_internal.mli @@ -0,0 +1,256 @@ +(** A view of the solver from a theory's point of view. + + Theories should interact with the solver via this module, to assert + new lemmas, propagate literals, access the congruence closure, etc. *) + +open Sigs + +type t +(** Main type for the SMT solver *) + +type solver = t + +val tst : t -> term_store +val stats : t -> Stat.t + +val proof : t -> proof_trace +(** Access the proof object *) + +val registry : t -> Registry.t +(** A solver contains a registry so that theories can share data *) + +(** {3 Actions for the theories} *) + +type theory_actions +(** Handle that the theories can use to perform actions. *) + +(** {3 Congruence Closure} *) + +val cc : t -> CC.t +(** Congruence closure for this solver *) + +(** {3 Backtracking} *) + +include Sidekick_sigs.BACKTRACKABLE0 with type t := t + +(** {3 Interface to SAT} *) + +include Sidekick_sat.PLUGIN_CDCL_T with type t := t + +(** {3 Simplifiers} *) + +type simplify_hook = Simplify.hook + +val add_simplifier : t -> Simplify.hook -> unit +(** Add a simplifier hook for preprocessing. *) + +val simplify_t : t -> term -> (term * step_id) option +(** Simplify input term, returns [Some u] if some + simplification occurred. *) + +val simp_t : t -> term -> term * step_id option +(** [simp_t si t] returns [u] even if no simplification occurred + (in which case [t == u] syntactically). + It emits [|- t=u]. + (see {!simplifier}) *) + +(** {3 Preprocessors} + These preprocessors turn mixed, raw literals (possibly simplified) into + literals suitable for reasoning. + Typically some clauses are also added to the solver. *) + +(* TODO: move into its own sig + library *) +module type PREPROCESS_ACTS = sig + val proof : proof_trace + + val mk_lit : ?sign:bool -> term -> lit + (** [mk_lit t] creates a new literal for a boolean term [t]. *) + + val add_clause : lit list -> step_id -> unit + (** pushes a new clause into the SAT solver. *) + + val add_lit : ?default_pol:bool -> lit -> unit + (** Ensure the literal will be decided/handled by the SAT solver. *) +end + +type preprocess_actions = (module PREPROCESS_ACTS) +(** Actions available to the preprocessor *) + +type preprocess_hook = t -> preprocess_actions -> term -> unit +(** Given a term, preprocess it. + + The idea is to add literals and clauses to help define the meaning of + the term, if needed. For example for boolean formulas, clauses + for their Tseitin encoding can be added, with the formula acting + as its own proxy symbol. + + @param preprocess_actions actions available during preprocessing. + *) + +val on_preprocess : t -> preprocess_hook -> unit +(** Add a hook that will be called when terms are preprocessed *) + +(** {3 hooks for the theory} *) + +val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a +(** Give a conflict clause to the solver *) + +val push_decision : t -> theory_actions -> lit -> unit +(** Ask the SAT solver to decide the given literal in an extension of the + current trail. This is useful for theory combination. + If the SAT solver backtracks, this (potential) decision is removed + and forgotten. *) + +val propagate : + t -> theory_actions -> lit -> reason:(unit -> lit list * step_id) -> unit +(** Propagate a boolean using a unit clause. + [expl => lit] must be a theory lemma, that is, a T-tautology *) + +val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit +(** Propagate a boolean using a unit clause. + [expl => lit] must be a theory lemma, that is, a T-tautology *) + +val add_clause_temp : t -> theory_actions -> lit list -> step_id -> unit +(** Add local clause to the SAT solver. This clause will be + removed when the solver backtracks. *) + +val add_clause_permanent : t -> theory_actions -> lit list -> step_id -> unit +(** Add toplevel clause to the SAT solver. This clause will + not be backtracked. *) + +val mk_lit : t -> ?sign:bool -> term -> lit +(** Create a literal. This automatically preprocesses the term. *) + +val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit +(** Add the given literal to the SAT solver, so it gets assigned + a boolean value. + @param default_pol default polarity for the corresponding atom *) + +val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit +(** Add the given (signed) bool term to the SAT solver, so it gets assigned + a boolean value *) + +val cc_find : t -> E_node.t -> E_node.t +(** Find representative of the node *) + +val cc_are_equal : t -> term -> term -> bool +(** Are these two terms equal in the congruence closure? *) + +val cc_resolve_expl : t -> CC_expl.t -> lit list * step_id + +(* + val cc_raise_conflict_expl : t -> theory_actions -> CC_expl.t -> 'a + (** Raise a conflict with the given congruence closure explanation. + it must be a theory tautology that [expl ==> absurd]. + To be used in theories. *) + + val cc_merge : + t -> theory_actions -> E_node.t -> E_node.t -> CC_expl.t -> unit + (** Merge these two nodes in the congruence closure, given this explanation. + It must be a theory tautology that [expl ==> n1 = n2]. + To be used in theories. *) + + val cc_merge_t : t -> theory_actions -> term -> term -> CC_expl.t -> unit + (** Merge these two terms in the congruence closure, given this explanation. + See {!cc_merge} *) + *) + +val cc_add_term : t -> term -> E_node.t +(** Add/retrieve congruence closure node for this term. + To be used in theories *) + +val cc_mem_term : t -> term -> bool +(** Return [true] if the term is explicitly in the congruence closure. + To be used in theories *) + +val on_cc_pre_merge : + t -> + (CC.t * E_node.t * E_node.t * CC_expl.t -> CC.Handler_action.or_conflict) -> + unit +(** Callback for when two classes containing data for this key are merged (called before) *) + +val on_cc_post_merge : + t -> (CC.t * E_node.t * E_node.t -> CC.Handler_action.t list) -> unit +(** Callback for when two classes containing data for this key are merged (called after)*) + +val on_cc_new_term : + t -> (CC.t * E_node.t * term -> CC.Handler_action.t list) -> unit +(** Callback to add data on terms when they are added to the congruence + closure *) + +val on_cc_is_subterm : + t -> (CC.t * E_node.t * term -> CC.Handler_action.t list) -> unit +(** Callback for when a term is a subterm of another term in the + congruence closure *) + +val on_cc_conflict : t -> (CC.ev_on_conflict -> unit) -> unit +(** Callback called on every CC conflict *) + +val on_cc_propagate : + t -> + (CC.t * lit * (unit -> lit list * step_id) -> CC.Handler_action.t list) -> + unit +(** Callback called on every CC propagation *) + +val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit +(** Register callbacked to be called with the slice of literals + newly added on the trail. + + This is called very often and should be efficient. It doesn't have + to be complete, only correct. It's given only the slice of + the trail consisting in new literals. *) + +val on_final_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit +(** Register callback to be called during the final check. + + Must be complete (i.e. must raise a conflict if the set of literals is + not satisfiable) and can be expensive. The function + is given the whole trail. + *) + +val on_th_combination : + t -> (t -> theory_actions -> (term * value) Iter.t) -> unit +(** Add a hook called during theory combination. + The hook must return an iterator of pairs [(t, v)] + which mean that term [t] has value [v] in the model. + + Terms with the same value (according to {!Term.equal}) will be + merged in the CC; if two terms with different values are merged, + we get a semantic conflict and must pick another model. *) + +val declare_pb_is_incomplete : t -> unit +(** Declare that, in some theory, the problem is outside the logic fragment + that is decidable (e.g. if we meet proper NIA formulas). + The solver will not reply "SAT" from now on. *) + +(** {3 Model production} *) + +type model_ask_hook = + recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option +(** A model-production hook to query values from a theory. + + It takes the solver, a class, and returns + a term for this class. For example, an arithmetic theory + might detect that a class contains a numeric constant, and return + this constant as a model value. + + If no hook assigns a value to a class, a fake value is created for it. + *) + +type model_completion_hook = t -> add:(term -> term -> unit) -> unit +(** A model production hook, for the theory to add values. + The hook is given a [add] function to add bindings to the model. *) + +val on_model : + ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit +(** Add model production/completion hooks. *) + +val add_theory_state : + st:'a -> + push_level:('a -> unit) -> + pop_levels:('a -> int -> unit) -> + t -> + unit + +val create : + (module ARG) -> stat:Stat.t -> proof:Proof_trace.t -> Term.store -> unit -> t diff --git a/src/smt/th_key.ml.bak b/src/smt/th_key.ml.bak new file mode 100644 index 00000000..cd8c7194 --- /dev/null +++ b/src/smt/th_key.ml.bak @@ -0,0 +1,145 @@ + + +module type S = sig + type ('term,'lit,'a) t + (** An access key for theories which have per-class data ['a] *) + + val create : + ?pp:'a Fmt.printer -> + name:string -> + eq:('a -> 'a -> bool) -> + merge:('a -> 'a -> 'a) -> + unit -> + ('term,'lit,'a) t + (** Generative creation of keys for the given theory data. + + @param eq : Equality. This is used to optimize backtracking info. + + @param merge : + [merge d1 d2] is called when merging classes with data [d1] and [d2] + respectively. The theory should already have checked that the merge + is compatible, and this produces the combined data for terms in the + merged class. + @param name name of the theory which owns this data + @param pp a printer for the data + *) + + val equal : ('t,'lit,_) t -> ('t,'lit,_) t -> bool + (** Checks if two keys are equal (generatively) *) + + val pp : _ t Fmt.printer + (** Prints the name of the key. *) +end + + +(** Custom keys for theory data. + This imitates the classic tricks for heterogeneous maps + https://blog.janestreet.com/a-universal-type/ + + It needs to form a commutative monoid where values are persistent so + they can be restored during backtracking. +*) +module Key = struct + module type KEY_IMPL = sig + type term + type lit + type t + val id : int + val name : string + val pp : t Fmt.printer + val equal : t -> t -> bool + val merge : t -> t -> t + exception Store of t + end + + type ('term,'lit,'a) t = + (module KEY_IMPL with type term = 'term and type lit = 'lit and type t = 'a) + + let n_ = ref 0 + + let create (type term)(type lit)(type d) + ?(pp=fun out _ -> Fmt.string out "") + ~name ~eq ~merge () : (term,lit,d) t = + let module K = struct + type nonrec term = term + type nonrec lit = lit + type t = d + let id = !n_ + let name = name + let pp = pp + let merge = merge + let equal = eq + exception Store of d + end in + incr n_; + (module K) + + let[@inline] id + : type term lit a. (term,lit,a) t -> int + = fun (module K) -> K.id + + let[@inline] equal + : type term lit a b. (term,lit,a) t -> (term,lit,b) t -> bool + = fun (module K1) (module K2) -> K1.id = K2.id + + let pp + : type term lit a. (term,lit,a) t Fmt.printer + = fun out (module K) -> Fmt.string out K.name +end + + + +(* + (** Map for theory data associated with representatives *) + module K_map = struct + type 'a key = (term,lit,'a) Key.t + type pair = Pair : 'a key * exn -> pair + + type t = pair IM.t + + let empty = IM.empty + + let[@inline] mem k t = IM.mem (Key.id k) t + + let find (type a) (k : a key) (self:t) : a option = + let (module K) = k in + match IM.find K.id self with + | Pair (_, K.Store v) -> Some v + | _ -> None + | exception Not_found -> None + + let add (type a) (k : a key) (v:a) (self:t) : t = + let (module K) = k in + IM.add K.id (Pair (k, K.Store v)) self + + let remove (type a) (k: a key) self : t = + let (module K) = k in + IM.remove K.id self + + let equal (m1:t) (m2:t) : bool = + IM.equal + (fun p1 p2 -> + let Pair ((module K1), v1) = p1 in + let Pair ((module K2), v2) = p2 in + assert (K1.id = K2.id); + match v1, v2 with K1.Store v1, K1.Store v2 -> K1.equal v1 v2 | _ -> false) + m1 m2 + + let merge ~f_both (m1:t) (m2:t) : t = + IM.merge + (fun _ p1 p2 -> + match p1, p2 with + | None, None -> None + | Some v, None + | None, Some v -> Some v + | Some (Pair ((module K1) as key1, pair1)), Some (Pair (_, pair2)) -> + match pair1, pair2 with + | K1.Store v1, K1.Store v2 -> + f_both K1.id pair1 pair2; (* callback for checking compat *) + let v12 = K1.merge v1 v2 in (* merge content *) + Some (Pair (key1, K1.Store v12)) + | _ -> assert false + ) + m1 m2 + end + *) diff --git a/src/smt/theory.ml b/src/smt/theory.ml new file mode 100644 index 00000000..7039ecb6 --- /dev/null +++ b/src/smt/theory.ml @@ -0,0 +1,44 @@ +(** Signatures for theory plugins *) + +(** A theory + + Theories are abstracted over the concrete implementation of the solver, + so they can work with any implementation. + + Typically a theory should be a functor taking an argument containing + a [SOLVER_INTERNAL] or even a full [SOLVER], + and some additional views on terms, literals, etc. + that are specific to the theory (e.g. to map terms to linear + expressions). + The theory can then be instantiated on any kind of solver for any + term representation that also satisfies the additional theory-specific + requirements. Instantiated theories (ie values of type {!SOLVER.theory}) + can be added to the solver. + *) +module type S = sig + type t + + val name : string + val create_and_setup : Solver_internal.t -> t + val push_level : t -> unit + val pop_levels : t -> int -> unit +end + +type t = (module S) +(** A theory that can be used for this particular solver. *) + +type 'a p = (module S with type t = 'a) +(** A theory that can be used for this particular solver, with state + of type ['a]. *) + +let make (type st) ~name ~create_and_setup ?(push_level = fun _ -> ()) + ?(pop_levels = fun _ _ -> ()) () : t = + let module Th = struct + type t = st + + let name = name + let create_and_setup = create_and_setup + let push_level = push_level + let pop_levels = pop_levels + end in + (module Th)