From 811c06b566d1e0ef8d640ab795a5381ad2f83099 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 28 Oct 2022 23:33:52 -0400 Subject: [PATCH] wip: feat(cdsat): plugins, main solver->Asolver.t --- src/cdsat/TVar.ml | 35 ++-------------- src/cdsat/TVar.mli | 15 ++----- src/cdsat/core.ml | 80 +++++++++++++++++++++++++++++++++++++ src/cdsat/core.mli | 57 ++++++++++++++++++++++++++ src/cdsat/reason.ml | 28 +++++++++++++ src/cdsat/reason.mli | 16 ++++++++ src/cdsat/sidekick_cdsat.ml | 2 +- 7 files changed, 189 insertions(+), 44 deletions(-) create mode 100644 src/cdsat/core.ml create mode 100644 src/cdsat/core.mli create mode 100644 src/cdsat/reason.ml create mode 100644 src/cdsat/reason.mli diff --git a/src/cdsat/TVar.ml b/src/cdsat/TVar.ml index 7cafa659..1b49d21d 100644 --- a/src/cdsat/TVar.ml +++ b/src/cdsat/TVar.ml @@ -8,6 +8,10 @@ module Vec_of = Veci (* TODO: GC API, + reuse existing slots that have been GC'd at the next [new_var_] allocation *) +type reason = + | Decide + | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id } + type store = { tst: Term.store; of_term: t Term.Weak_map.t; @@ -20,10 +24,6 @@ type store = { new_vars: Vec_of.t; } -and reason = - | Decide - | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id } - (* create a new variable *) let new_var_ (self : store) ~term:(term_for_v : Term.t) () : t = let v : t = Vec.size self.term in @@ -86,33 +86,6 @@ let pop_new_var self : _ option = else Some (Vec_of.pop self.new_vars) -module Reason = struct - type t = reason = - | Decide - | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id } - - let pp out (self : t) : unit = - match self with - | Decide -> Fmt.string out "decide" - | Propagate { level; hyps; proof = _ } -> - Fmt.fprintf out "(@[propagate[lvl=%d]@ :n-hyps %d@])" level - (Vec_of.size hyps) - - let decide : t = Decide - - let[@inline] propagate_ level v proof : t = - Propagate { level; hyps = v; proof } - - let propagate_v store v proof : t = - let level = Vec_of.fold_left (fun l v -> max l (level store v)) 0 v in - propagate_ level v proof - - let propagate_l store l proof : t = - let v = Vec_of.create ~cap:(List.length l) () in - List.iter (Vec_of.push v) l; - propagate_v store v proof -end - module Store = struct type t = store diff --git a/src/cdsat/TVar.mli b/src/cdsat/TVar.mli index 64b87738..425d98b3 100644 --- a/src/cdsat/TVar.mli +++ b/src/cdsat/TVar.mli @@ -20,18 +20,9 @@ module Vec_of : Vec_sig.S with type elt := t type store = Store.t -(** Reason for assignment *) -module Reason : sig - type t = - | Decide - | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id } - - include Sidekick_sigs.PRINT with type t := t - - val decide : t - val propagate_v : store -> Vec_of.t -> Sidekick_proof.step_id -> t - val propagate_l : store -> var list -> Sidekick_proof.step_id -> t -end +type reason = + | Decide + | Propagate of { level: int; hyps: Vec_of.t; proof: Sidekick_proof.step_id } val of_term : store -> Term.t -> t (** Obtain a variable for this term. *) diff --git a/src/cdsat/core.ml b/src/cdsat/core.ml new file mode 100644 index 00000000..398b131c --- /dev/null +++ b/src/cdsat/core.ml @@ -0,0 +1,80 @@ +open Sidekick_core +module Proof = Sidekick_proof +module Asolver = Sidekick_abstract_solver +module Check_res = Asolver.Check_res + +module Plugin_action = struct + type t = { propagate: TVar.t -> Value.t -> Reason.t -> unit } + + let propagate (self : t) var v reas : unit = self.propagate var v reas +end + +(** Core plugin *) +module Plugin = struct + type t = { + name: string; + push_level: unit -> unit; + pop_levels: int -> unit; + decide: TVar.t -> Value.t option; + propagate: Plugin_action.t -> TVar.t -> Value.t -> unit; + } + + let make ~name ~push_level ~pop_levels ~decide ~propagate () : t = + { name; push_level; pop_levels; decide; propagate } +end + +type t = { + tst: Term.store; + vst: TVar.store; + trail: Trail.t; + plugins: Plugin.t Vec.t; + mutable last_res: Check_res.t option; + proof_tracer: Proof.Tracer.t; +} + +let create tst vst ~proof_tracer () : t = + { + tst; + vst; + trail = Trail.create (); + plugins = Vec.create (); + last_res = None; + proof_tracer; + } + +let[@inline] trail self = self.trail +let add_plugin self p = Vec.push self.plugins p +let[@inline] iter_plugins self f = Vec.iter ~f self.plugins +let[@inline] tst self = self.tst +let[@inline] vst self = self.vst + +(* solving *) + +let add_ty (_self : t) ~ty:_ : unit = () +let assert_clause (self : t) lits p : unit = assert false +let assert_term (self : t) t : unit = assert false + +let solve ?on_exit ?on_progress ?should_stop ~assumptions (self : t) : + Check_res.t = + assert false + +(* asolver interface *) + +let as_asolver (self : t) : Asolver.t = + object (asolver) + method tst = self.tst + method assert_clause lits p : unit = assert_clause self lits p + + method assert_clause_l lits p : unit = + asolver#assert_clause (Array.of_list lits) p + + method add_ty ~ty : unit = add_ty self ~ty + method lit_of_term ?sign t = Lit.atom ?sign self.tst t + method assert_term t : unit = assert_term self t + method last_res = self.last_res + method proof_tracer = self.proof_tracer + + method solve ?on_exit ?on_progress ?should_stop ~assumptions () + : Check_res.t = + solve ?on_exit ?on_progress ?should_stop ~assumptions self + end diff --git a/src/cdsat/core.mli b/src/cdsat/core.mli new file mode 100644 index 00000000..eb399a89 --- /dev/null +++ b/src/cdsat/core.mli @@ -0,0 +1,57 @@ +(** Reasoning core *) + +open Sidekick_proof + +(** {2 Plugins} *) + +module Plugin_action : sig + type t + + val propagate : t -> TVar.t -> Value.t -> Reason.t -> unit +end + +(** Core plugin *) +module Plugin : sig + type t = private { + name: string; + push_level: unit -> unit; + pop_levels: int -> unit; + decide: TVar.t -> Value.t option; + propagate: Plugin_action.t -> TVar.t -> Value.t -> unit; + } + + val make : + name:string -> + push_level:(unit -> unit) -> + pop_levels:(int -> unit) -> + decide:(TVar.t -> Value.t option) -> + propagate:(Plugin_action.t -> TVar.t -> Value.t -> unit) -> + unit -> + t +end + +(** {2 Basics} *) + +type t + +val create : + Term.store -> TVar.store -> proof_tracer:Sidekick_proof.Tracer.t -> unit -> t +(** Create new solver *) + +val tst : t -> Term.store +val vst : t -> TVar.store +val trail : t -> Trail.t +val add_plugin : t -> Plugin.t -> unit +val iter_plugins : t -> Plugin.t Iter.t + +(** {2 Solving} *) + +val as_asolver : t -> Sidekick_abstract_solver.t + +(* + assert (term -> proof -> unit) + solve (assumptions:term list -> res) + + as_asolver (-> asolver) + +*) diff --git a/src/cdsat/reason.ml b/src/cdsat/reason.ml new file mode 100644 index 00000000..2bf11b5a --- /dev/null +++ b/src/cdsat/reason.ml @@ -0,0 +1,28 @@ +type t = TVar.reason = + | Decide + | Propagate of { + level: int; + hyps: TVar.Vec_of.t; + proof: Sidekick_proof.step_id; + } + +let pp out (self : t) : unit = + match self with + | Decide -> Fmt.string out "decide" + | Propagate { level; hyps; proof = _ } -> + Fmt.fprintf out "(@[propagate[lvl=%d]@ :n-hyps %d@])" level + (TVar.Vec_of.size hyps) + +let decide : t = Decide +let[@inline] propagate_ level v proof : t = Propagate { level; hyps = v; proof } + +let propagate_v store v proof : t = + let level = + TVar.Vec_of.fold_left (fun l v -> max l (TVar.level store v)) 0 v + in + propagate_ level v proof + +let propagate_l store l proof : t = + let v = TVar.Vec_of.create ~cap:(List.length l) () in + List.iter (TVar.Vec_of.push v) l; + propagate_v store v proof diff --git a/src/cdsat/reason.mli b/src/cdsat/reason.mli new file mode 100644 index 00000000..53c8a123 --- /dev/null +++ b/src/cdsat/reason.mli @@ -0,0 +1,16 @@ +(** Reason for assignment *) + +(** Reason for assignment *) +type t = TVar.reason = + | Decide + | Propagate of { + level: int; + hyps: TVar.Vec_of.t; + proof: Sidekick_proof.step_id; + } + +include Sidekick_sigs.PRINT with type t := t + +val decide : t +val propagate_v : TVar.store -> TVar.Vec_of.t -> Sidekick_proof.step_id -> t +val propagate_l : TVar.store -> TVar.t list -> Sidekick_proof.step_id -> t diff --git a/src/cdsat/sidekick_cdsat.ml b/src/cdsat/sidekick_cdsat.ml index ec81534a..284bd31c 100644 --- a/src/cdsat/sidekick_cdsat.ml +++ b/src/cdsat/sidekick_cdsat.ml @@ -2,5 +2,5 @@ module Trail = Trail module TVar = TVar -module Reason = TVar.Reason +module Reason = Reason module Value = Value