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

wip: feat(cdsat): core solver

Browse source
This commit is contained in:
Simon Cruanes 2022-10-29 22:49:04 -04:00
parent 903d12c39b
commit 2b4cbd9c05
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/cdsat/core.ml
View file

@ -26,16 +26,18 @@ end
type t = { type t = {
tst: Term.store; tst: Term.store;
vst: TVar.store; vst: TVar.store;
stats: Stat.t;
trail: Trail.t; trail: Trail.t;
plugins: Plugin.t Vec.t; plugins: Plugin.t Vec.t;
mutable last_res: Check_res.t option; mutable last_res: Check_res.t option;
proof_tracer: Proof.Tracer.t; proof_tracer: Proof.Tracer.t;
} }
let create tst vst ~proof_tracer () : t = let create ?(stats = Stat.create ()) tst vst ~proof_tracer () : t =
{ {
tst; tst;
vst; vst;
stats;
trail = Trail.create (); trail = Trail.create ();
plugins = Vec.create (); plugins = Vec.create ();
last_res = None; last_res = None;
@ -53,6 +55,7 @@ let[@inline] vst self = self.vst
let add_ty (_self : t) ~ty:_ : unit = () let add_ty (_self : t) ~ty:_ : unit = ()
let assert_clause (self : t) lits p : unit = assert false let assert_clause (self : t) lits p : unit = assert false
let assert_term (self : t) t : unit = assert false let assert_term (self : t) t : unit = assert false
let pp_stats out self = Stat.pp out self.stats
let solve ?on_exit ?on_progress ?should_stop ~assumptions (self : t) : let solve ?on_exit ?on_progress ?should_stop ~assumptions (self : t) :
Check_res.t = Check_res.t =
@ -73,6 +76,7 @@ let as_asolver (self : t) : Asolver.t =
method assert_term t : unit = assert_term self t method assert_term t : unit = assert_term self t
method last_res = self.last_res method last_res = self.last_res
method proof_tracer = self.proof_tracer method proof_tracer = self.proof_tracer
method pp_stats out () = pp_stats out self
method solve ?on_exit ?on_progress ?should_stop ~assumptions () method solve ?on_exit ?on_progress ?should_stop ~assumptions ()
: Check_res.t = : Check_res.t =

7
src/cdsat/core.mli
View file

@ -35,7 +35,12 @@ end
type t type t
val create : val create :
Term.store -> TVar.store -> proof_tracer:Sidekick_proof.Tracer.t -> unit -> t ?stats:Stat.t ->
Term.store ->
TVar.store ->
proof_tracer:Sidekick_proof.Tracer.t ->
unit ->
t
(** Create new solver *) (** Create new solver *)
val tst : t -> Term.store val tst : t -> Term.store

1
src/cdsat/sidekick_cdsat.ml
View file

@ -4,3 +4,4 @@ module Trail = Trail
module TVar = TVar module TVar = TVar
module Reason = Reason module Reason = Reason
module Value = Value module Value = Value
module Core = Core