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

refactor: continue functorization of sidekick

Browse source
This commit is contained in:
Simon Cruanes 2019-05-27 19:55:21 -05:00
parent e4f20d08c7
commit 080a20480f
19 changed files with 886 additions and 1003 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/base-term/Sidekick_base_term.ml Normal file
View file

@ -0,0 +1,27 @@
module ID = ID
module Ty_card = Ty_card
module Cst = Cst
module Stat = Stat
module Model = Model
module Ast = Ast
module Term = Term
module Value = Value
module Term_cell = Term_cell
module Ty = Ty
module Lit = Lit
module Value = Value
module Arg
: Sidekick_core.TERM_LIT
with type Term.t = Term.t
and type Lit.t = Lit.t
and type Fun.t = Cst.t
and type Ty.t = Ty.t
= struct
module Term = Term
module Lit = Lit
module Fun = Cst
module Ty = Ty
end

2
src/base-term/dune
View file

@ -4,4 +4,4 @@
(synopsis "Basic term definitions for the standalone SMT solver")
(libraries containers containers.data
sidekick.core sidekick.util zarith)
(flags :standard -open Sidekick_util))
(flags :standard -w -32 -open Sidekick_util))

13
src/cc/Sidekick_cc.ml
View file

@ -245,7 +245,7 @@ module Make(A: ARG) = struct
See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *)
and ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit
and ev_on_new_term = t -> N.t -> term -> th_data -> th_data option
and ev_on_new_term = t -> N.t -> term -> th_data option
let[@inline] size_ (r:repr) = r.n_size
let[@inline] true_ cc = Lazy.force cc.true_
@ -505,9 +505,9 @@ module Make(A: ARG) = struct
let th_data =
List.fold_left
(fun data f ->
match f cc n t data with
match f cc n t with
| None -> data
| Some d -> d)
| Some d -> A.Data.merge data d)
A.Data.empty cc.on_new_term
in
n.n_th_data <- th_data;
@ -527,7 +527,7 @@ module Make(A: ARG) = struct
sub
in
let[@inline] return x = Some x in
match T.cc_view n.n_term with
match A.cc_view n.n_term with
| Bool _ | Opaque _ -> None
| Eq (a,b) ->
let a = deref_sub a in
@ -820,7 +820,7 @@ module Make(A: ARG) = struct
let t = A.Lit.term lit in
Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" A.Lit.pp lit);
let sign = A.Lit.sign lit in
begin match T.cc_view t with
begin match A.cc_view t with
| Eq (a,b) when sign ->
let a = add_term cc a in
let b = add_term cc b in
@ -850,7 +850,8 @@ module Make(A: ARG) = struct
let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
let create ?(stat=Stat.global)
?(on_merge=[]) ?(on_new_term=[]) ?(size=`Big) (tst:term_state) : t =
?(on_merge=[]) ?(on_new_term=[]) ?(size=`Big)
(tst:term_state) : t =
let size = match size with `Small -> 128 | `Big -> 2048 in
let rec cc = {
tst;

111
src/core/Sidekick_core.ml
View file

@ -93,6 +93,9 @@ module type TERM_LIT = sig
val apply_sign : t -> bool -> t
val norm_sign : t -> t * bool
(** Invariant: if [u, sign = norm_sign t] then [apply_sign u sign = t] *)
val atom : Term.state -> ?sign:bool -> Term.t -> t
end
end
@ -111,7 +114,6 @@ module type TERM_LIT_PROOF = sig
end
end
module type CC_ARG = sig
include TERM_LIT_PROOF
@ -120,7 +122,9 @@ module type CC_ARG = sig
(** Monoid embedded in every node *)
module Data : sig
include MERGE_PP
type t
val merge : t -> t -> t
val pp : t Fmt.printer
val empty : t
end
@ -335,9 +339,6 @@ module type SOLVER_INTERNAL = sig
type t
type solver = t
(** {3 Utils} *)
val tst : t -> term_state
(**/**)
module Debug_ : sig
val on_check_invariants : t -> (unit -> unit) -> unit
@ -364,19 +365,17 @@ module type SOLVER_INTERNAL = sig
module Key : sig
type 'a t
type 'a ev_on_merge = solver -> CC.N.t -> 'a -> CC.N.t -> 'a -> CC.Expl.t -> unit
type 'a data = (module MERGE_PP with type t = 'a)
val create :
solver ->
'a data ->
on_merge:'a ev_on_merge ->
'a t
val create : solver -> 'a data -> 'a t
(** Create a key for storing and accessing data of type ['a].
Values have to be mergeable (but only if [on_merge] does not
raise a conflict) *)
Values have to be mergeable. *)
end
(** {3 Actions available to theories} *)
val tst : t -> term_state
val cc : t -> CC.t
(** Congruence closure for this solver *)
@ -410,11 +409,14 @@ module type SOLVER_INTERNAL = sig
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
val raise_conflict : t -> Expl.t -> unit
val raise_conflict : t -> Expl.t -> 'a
(** Raise a conflict with the given explanation
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
val cc_find : t -> N.t -> N.t
(** Find representative of the node *)
val cc_merge : t -> N.t -> N.t -> Expl.t -> unit
(** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
@ -424,6 +426,13 @@ module type SOLVER_INTERNAL = sig
(** Add/retrieve congruence closure node for this term.
To be used in theories *)
val cc_data : t -> k:'a Key.t -> N.t -> 'a option
(** Theory specific data for the given node *)
val cc_add_data : t -> k:'a Key.t -> N.t -> 'a -> unit
(** Add data for this node. This might trigger a conflict if the class
already contains data that is not compatible. *)
val cc_merge_t : t -> term -> term -> Expl.t -> unit
(** Merge these two terms in the congruence closure, given this explanation.
See {!cc_merge} *)
@ -435,6 +444,9 @@ module type SOLVER_INTERNAL = sig
unit
(** Callback for when two classes containing data for this key are merged *)
val on_cc_merge_all : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit
(** Callback for when any two classes are merged *)
val on_cc_new_term :
t ->
k:'a Key.t ->
@ -444,26 +456,28 @@ module type SOLVER_INTERNAL = sig
closure *)
val on_partial_check : t -> (t -> lit Iter.t -> unit) -> unit
(** Called with the slice of literals newly added on the trail *)
(** 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 -> lit Iter.t -> unit) -> unit
(** Final check, must be complete (i.e. must raise a conflict
if the set of literals is not satisfiable) *)
(** Register callback to be called during the final check.
(* TODO?
val on_mk_model : t -> (lit Iter.t -> Model.t -> Model.t) -> unit
(** Update the given model *)
*)
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. *)
end
(** Public view of the solver *)
module type SOLVER = sig
module Internal : SOLVER_INTERNAL
(** Extensive view of the solver. This should mostly be used
by the theories *)
module Solver_internal : SOLVER_INTERNAL
(** Internal solver, available to theories. *)
module A = Internal.A
type t = Internal.t
module A = Solver_internal.A
type t
type solver = t
type term = A.Term.t
type ty = A.Ty.t
@ -492,8 +506,8 @@ module type SOLVER = sig
val name : string
(** Name of the theory *)
val create_and_setup : solver -> t
(** Instantiate the theory's state for the given solver,
val create_and_setup : Solver_internal.t -> t
(** Instantiate the theory's state for the given (internal) solver,
register callbacks, create keys, etc. *)
val push_level : t -> unit
@ -514,45 +528,13 @@ module type SOLVER = sig
val mk_theory :
name:string ->
create_and_setup:(t -> 'th) ->
create_and_setup:(Solver_internal.t -> 'th) ->
?push_level:('th -> unit) ->
?pop_levels:('th -> int -> unit) ->
unit ->
theory
(** Helper to create a theory *)
(* TODO: remove?
let make
(type st)
?(check_invariants=fun _ -> ())
?(on_new_term=fun _ _ _ -> ())
?(on_merge=fun _ _ _ _ _ -> ())
?(partial_check=fun _ _ _ -> ())
?(mk_model=fun _ _ m -> m)
?(push_level=fun _ -> ())
?(pop_levels=fun _ _ -> ())
?(cc_th=fun _->[])
~name
~final_check
~create
() : t =
let module A = struct
type nonrec t = st
let name = name
let create = create
let on_new_term = on_new_term
let on_merge = on_merge
let partial_check = partial_check
let final_check = final_check
let mk_model = mk_model
let check_invariants = check_invariants
let push_level = push_level
let pop_levels = pop_levels
let cc_th = cc_th
end in
(module A : S)
*)
(** {3 Boolean Atoms} *)
module Atom : sig
type t
@ -591,9 +573,9 @@ module type SOLVER = sig
val pp : t CCFormat.printer
(*
type unknown =
| U_timeout
| U_incomplete
type unknown =
| U_timeout
| U_incomplete
*)
end
@ -607,6 +589,7 @@ module type SOLVER = sig
(* TODO? ?config:Config.t -> *)
?store_proof:bool ->
theories:theory list ->
A.Term.state ->
unit ->
t
(** Create a new solver.

3
src/main/dune
View file

@ -5,8 +5,7 @@
(public_name sidekick)
(package sidekick)
(libraries containers iter result msat sidekick.core
sidekick.base-term sidekick.msat-solver sidekick.smtlib
sidekick.smt.th-ite sidekick.dimacs)
sidekick.base-term sidekick.msat-solver sidekick.smtlib sidekick.dimacs)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8
-safe-string -color always -open Sidekick_util)
(ocamlopt_flags :standard -O3 -color always

16
src/mini-cc/Mini_cc.ml
View file

@ -4,7 +4,12 @@ type res =
| Unsat
module CC_view = Sidekick_core.CC_view
module type TERM = Sidekick_core.TERM
module type ARG = sig
include Sidekick_core.TERM
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
end
module type S = sig
type term
@ -23,8 +28,7 @@ module type S = sig
val classes : t -> term Iter.t Iter.t
end
module Make(A: TERM) = struct
module Make(A: ARG) = struct
open CC_view
module Fun = A.Fun
@ -150,7 +154,7 @@ module Make(A: TERM) = struct
self
let sub_ t k : unit =
match T.cc_view t with
match A.cc_view t with
| Bool _ | Opaque _ -> ()
| App_fun (_, args) -> args k
| App_ho (f, args) -> k f; args k
@ -202,7 +206,7 @@ module Make(A: TERM) = struct
let compute_sig (self:t) (n:node) : Signature.t option =
let[@inline] return x = Some x in
match T.cc_view n.n_t with
match A.cc_view n.n_t with
| Bool _ | Opaque _ -> None
| Eq (a,b) ->
let a = find_t_ self a in
@ -293,7 +297,7 @@ module Make(A: TERM) = struct
(* API *)
let add_lit (self:t) (p:T.t) (sign:bool) : unit =
match T.cc_view p with
match A.cc_view p with
| Eq (t1,t2) when sign ->
let n1 = add_t self t1 in
let n2 = add_t self t2 in

9
src/mini-cc/Mini_cc.mli
View file

@ -11,7 +11,12 @@ type res =
| Unsat
module CC_view = Sidekick_core.CC_view
module type TERM = Sidekick_core.TERM
module type ARG = sig
include Sidekick_core.TERM
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
end
module type S = sig
type term
@ -35,7 +40,7 @@ module type S = sig
This should be called only if {!check} returned [Sat]. *)
end
module Make(A: TERM)
module Make(A: ARG)
: S with type term = A.Term.t
and type fun_ = A.Fun.t
and type term_state = A.Term.state

18
src/msat-solver/CC.ml
View file

@ -1,18 +0,0 @@
module Arg = struct
module Fun = Cst
module Term = Term
module Lit = Lit
module Value = Value
module Ty = Ty
module Model = Model
module Proof = struct
type t = Solver_types.proof
let pp = Solver_types.pp_proof
let default = Solver_types.Proof_default
end
end
(* include Sidekick_cc.Make(Arg) *)
module Mini_cc = Sidekick_cc.Mini_cc.Make(Arg)

16
src/msat-solver/CC.mli
View file

@ -1,16 +0,0 @@
(*
include Sidekick_cc.S
with type term = Term.t
and type model = Model.t
and type lit = Lit.t
and type fun_ = Cst.t
and type term_state = Term.state
and type proof = Solver_types.proof
and module Key = Sidekick_cc.Key
*)
module Mini_cc : Sidekick_cc.Mini_cc.S
with type term = Term.t
and type fun_ = Cst.t
and type term_state = Term.state

547
src/msat-solver/Sidekick_msat_solver.ml Normal file
View file

@ -0,0 +1,547 @@
(** {1 Implementation of a Solver using Msat} *)
module Vec = Msat.Vec
module Log = Msat.Log
module IM = Util.Int_map
module type ARG = sig
include Sidekick_core.TERM_LIT_PROOF
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) Sidekick_core.CC_view.t
end
module type S = Sidekick_core.SOLVER
module Make(A : ARG)
(* : S with type A.Term.t = A.Term.t *)
= struct
module T = A.Term
module Lit = A.Lit
type lit = Lit.t
(** 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 CC_key = struct
type 'a data = (module Sidekick_core.MERGE_PP with type t = 'a)
module type KEY_IMPL = sig
include Sidekick_core.MERGE_PP
val id : int
exception Store of t
end
type 'a t = (module KEY_IMPL with type t = 'a)
let n_ = ref 0
let create (type d) (x:d data) : d t =
let (module D) = x in
let module K = struct
include D
let id = !n_
exception Store of t
end in
incr n_;
(module K)
let[@inline] id : type a. a t -> int = fun (module K) -> K.id
let[@inline] equal
: type a b. a t -> b t -> bool
= fun (module K1) (module K2) -> K1.id = K2.id
let pp
: type a. a t -> a Fmt.printer
= fun (module K) out x -> K.pp out x
end
(** Map for theory data associated with representatives, given
to the congruence closure. *)
module Key_set = struct
type 'a key = 'a CC_key.t
type k1 =
| K1 : {
k: 'a key;
e: exn;
} -> k1
type t = k1 IM.t
let empty = IM.empty
let[@inline] mem k t = IM.mem (CC_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
| K1 {e=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 (K1 {k; e=K.Store v}) self
let remove (type a) (k: a key) self : t =
let (module K) = k in
IM.remove K.id self
let merge (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 (K1 {k=(module K1) as key1; e=pair1; }), Some (K1{e=pair2;_}) ->
match pair1, pair2 with
| K1.Store v1, K1.Store v2 ->
let v12 = K1.merge v1 v2 in (* merge content *)
Some (K1 {k=key1; e=K1.Store v12; })
| _ -> assert false)
m1 m2
let pp_pair out (K1 {k=(module K);e=x; _}) =
match x with
| K.Store x -> K.pp out x
| _ -> assert false
let pp out (self:t) =
if IM.is_empty self then Fmt.string out "{}"
else Fmt.fprintf out "{@[%a@]}" (Util.pp_seq pp_pair) (IM.values self)
end
(* the full argument to the congruence closure *)
module A = struct
include A
module Data = Key_set
module Actions = struct
type t = {
raise_conflict : 'a. Lit.t list -> Proof.t -> 'a;
propagate : Lit.t -> reason:Lit.t Iter.t -> Proof.t -> unit;
}
let[@inline] raise_conflict a lits p = a.raise_conflict lits p
let[@inline] propagate a lit ~reason p = a.propagate lit ~reason p
end
end
module CC = Sidekick_cc.Make(A)
module Expl = CC.Expl
module N = CC.N
(** Internal solver, given to theories and to Msat *)
module Solver_internal = struct
module A = A
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 msat *)
type msat_acts = (Msat.void, Lit.t, Msat.void, A.Proof.t) Msat.acts
type t = {
tst: T.state; (** state for managing terms *)
cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t;
count_axiom: int Stat.counter;
count_conflict: int Stat.counter;
count_propagate: int Stat.counter;
cc_acts: CC.actions lazy_t;
mutable th_states : th_states; (** Set of theories *)
mutable msat_acts: msat_acts option;
mutable on_partial_check: (t -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> lit Iter.t -> unit) list;
mutable on_cc_merge: on_cc_merge list IM.t;
mutable on_cc_new_term : on_cc_new_term IM.t;
}
and on_cc_merge = On_cc_merge : {
k: 'a CC_key.t;
f: t -> CC.N.t -> 'a -> CC.N.t -> 'a -> CC.Expl.t -> unit;
} -> on_cc_merge
and on_cc_new_term = On_cc_new_term : {
k: 'a CC_key.t;
f: t -> N.t -> T.t -> 'a option;
} -> on_cc_new_term
module Formula = struct
include Lit
let norm lit =
let lit', sign = norm_sign lit in
lit', if sign then Msat.Same_sign else Msat.Negated
end
module Eq_class = CC.N
module Expl = CC.Expl
type formula = Lit.t
type proof = A.Proof.t
type conflict = lit list
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] raise_conflict self c : 'a =
Stat.incr self.count_conflict;
match self.msat_acts with
| None -> assert false
| Some acts ->
acts.Msat.acts_raise_conflict c A.Proof.default
let[@inline] propagate self p cs : unit =
Stat.incr self.count_propagate;
match self.msat_acts with
| None -> assert false
| Some acts ->
acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), A.Proof.default))
let[@inline] propagate_l self p cs : unit = propagate self p (fun()->cs)
let add_axiom_ self ~keep lits : unit =
Stat.incr self.count_axiom;
match self.msat_acts with
| None -> assert false
| Some acts ->
acts.Msat.acts_add_clause ~keep lits A.Proof.default
let[@inline] mk_lit self ?sign t = Lit.atom self.tst ?sign t
let[@inline] add_local_axiom self lits : unit =
add_axiom_ self ~keep:false lits
let[@inline] add_persistent_axiom self lits : unit =
add_axiom_ self ~keep:true lits
let[@inline] add_lit self lit : unit =
match self.msat_acts with
| None -> assert false
| Some acts -> acts.Msat.acts_mk_lit lit
let add_lit_t self ?sign t = add_lit self (mk_lit self ?sign t)
(** {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 =
CC.push_level (cc self);
push_lvl_ self.th_states
let pop_levels (self:t) n : unit =
CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (lits:Lit.t Iter.t) : unit =
Msat.Log.debugf 2
(fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
(if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
let cc = cc self in
if not final then (
CC.assert_lits cc lits;
);
(* transmit to theories. *)
CC.check cc (Lazy.force self.cc_acts);
if final then (
List.iter (fun f -> f self lits) self.on_final_check;
) else (
List.iter (fun f -> f self lits) self.on_partial_check;
);
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f ->
acts.Msat.acts_iter_assumptions
(function
| Msat.Lit a -> f a
| Msat.Assign _ -> assert false)
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
let old_acts = self.msat_acts in
self.msat_acts <- Some acts;
try
let iter = iter_atoms_ acts in
(* TODO if Config.progress then print_progress(); *)
Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter));
assert_lits_ ~final self iter;
self.msat_acts <- old_acts;
()
with e ->
self.msat_acts <- old_acts;
raise e
let add_formula (self:t) (lit:Lit.t) =
let t = Lit.term lit in
let lazy cc = self.cc in
let n = CC.add_term cc t in
CC.set_as_lit cc n (Lit.abs lit);
()
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:false self acts
(* perform final check of the model *)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts
(* TODO
let mk_model (self:t) lits : Model.t =
let m =
Iter.fold
(fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
Model.empty (theories self)
in
(* now complete model using CC *)
CC.mk_model (cc self) m
*)
let cc_raise_conflict self lits _p =
raise_conflict self lits
let cc_propagate self p ~reason _p =
let reason() = Iter.to_list reason in
propagate self p reason
let create ~stat (tst:A.Term.state) () : t =
let rec self = {
tst;
cc = lazy (
(* lazily tie the knot *)
CC.create ~size:`Big self.tst;
);
cc_acts=lazy {
raise_conflict=cc_raise_conflict self;
propagate=cc_propagate self;
};
th_states=Ths_nil;
stat;
count_axiom = Stat.mk_int stat "th-axioms";
count_propagate = Stat.mk_int stat "th-propagations";
count_conflict = Stat.mk_int stat "th-conflicts";
msat_acts=None;
on_partial_check=[];
on_final_check=[];
on_cc_merge=IM.empty;
on_cc_new_term=IM.empty;
} in
ignore (Lazy.force @@ self.cc : CC.t);
self
end
type conflict = lit list
(** the Main Solver *)
module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = Sat_solver.Proof
(* main solver state *)
type t = {
si: Solver_internal.t;
solver: Sat_solver.t;
stat: Stat.t;
(* config: Config.t *)
}
type solver = t
module type THEORY = 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 theory = (module THEORY)
(** {2 Main} *)
let add_theory (self:t) (th:theory) : unit =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
let st = Th.create_and_setup self.si in
(* add push/pop to the internal solver *)
begin
let open Solver_internal in
self.si.th_states <- Ths_cons {
st;
push_level=Th.push_level;
pop_levels=Th.pop_levels;
next=self.si.th_states;
};
end;
()
let add_theory_l self = List.iter (add_theory self)
(* create a new solver *)
let create ?(stat=Stat.global) ?size ?store_proof ~theories tst () : t =
Log.debug 5 "th_combine.create";
let si = Solver_internal.create ~stat tst () in
let self = {
si;
solver=Sat_solver.create ?store_proof ?size si;
stat;
} in
add_theory_l self theories;
(* assert [true] and [not false] *)
begin
let tst = Solver_internal.tst self.si in
Sat_solver.assume self.solver [
[Lit.atom tst @@ T.bool tst true];
] A.Proof.default;
end;
self
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
CC.Debug_.check_invariants (Solver_internal.cc self.si);
)
let[@inline] solver self = self.solver
let[@inline] cc self = Solver_internal.cc self.si
let stats self = self.stat
let[@inline] tst self = Solver_internal.tst self.si
let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom (tst self) ?sign t in
mk_atom_lit self lit
(** {2 Result} *)
module Unknown = struct
type t =
| U_timeout
| U_max_depth
| U_incomplete
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"
end
(* TODO *)
module Model = struct
type t = unit
let empty = ()
let mem _ _ = false
let find _ _ = None
let eval _ _ = None
let pp out _ = Fmt.string out "<model>"
end
(* TODO
type model = A.Model.t
let pp_model = Model.pp
*)
type res = (Model.t, Proof.t, lit IArray.t, Unknown.t) Sidekick_core.solver_res
(** {2 Main} *)
(* convert unsat-core *)
let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
Iter.of_list core
|> Iter.map clause_of_mclause
(* print all terms reachable from watched literals *)
let pp_term_graph _out (_:t) =
()
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:T.t) : unit =
Term.iter_dag t
|> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t)
|> Iter.filter
(fun t -> match Term.view t with
| Term.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub);
ignore (mk_atom_t self sub : Sat_solver.atom))
let assume (self:t) (c:Lit.t IArray.t) : unit =
let sat = solver self in
IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
Stat.incr self.count_clause;
Sat_solver.add_clause_a sat c Proof_default
(* TODO: remove? use a special constant + micro theory instead?
let[@inline] assume_distinct self l ~neq lit : unit =
CC.assert_distinct (cc self) l lit ~neq
*)
let check_model (_s:t) : unit =
Log.debug 1 "(smt.solver.check-model)";
(* TODO
Sat_solver.check_model s.solver
*)
()
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let do_on_exit () =
List.iter (fun f->f()) on_exit;
in
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat st ->
Log.debugf 1 (fun k->k "SAT");
let lits f = st.iter_trail f (fun _ -> ()) in
let m = Theory_combine.mk_model (th_combine self) lits in
do_on_exit ();
Sat m
(*
let env = Ast.env_empty in
let m = Model.make ~env in
…
Unknown U_incomplete (* TODO *)
*)
| Sat_solver.Unsat us ->
let pr =
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
with Msat.Solver_intf.No_proof -> None
in
do_on_exit ();
Unsat pr
end

25
src/msat-solver/Sidekick_smt.ml
View file

@ -1,25 +0,0 @@
module ID = ID
module Ty_card = Ty_card
module Cst = Cst
module Stat = Stat
module Model = Model
module Ast = Ast
module Term = Term
module Value = Value
module Term_cell = Term_cell
module Ty = Ty
module Lit = Lit
module Theory_combine = Theory_combine
module Theory = Theory
module Solver = Solver
module CC = CC
module Solver_types = Solver_types
type theory = Theory.t
(**/**)
module Vec = Msat.Vec
module Log = Msat.Log
(**/**)

279
src/msat-solver/Solver.ml
View file

@ -1,279 +0,0 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Main Solver} *)
[@@@warning "-32"]
open Solver_types
let get_time : unit -> float = Sys.time
(** {2 The Main Solver} *)
module Sat_solver = Msat.Make_cdcl_t(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = Sat_solver.Proof
(* main solver state *)
type t = {
solver: Sat_solver.t;
stat: Stat.t;
count_clause: int Stat.counter;
count_solve: int Stat.counter;
config: Config.t
}
let[@inline] solver self = self.solver
let[@inline] th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
let[@inline] add_theory self th = Theory_combine.add_theory (th_combine self) th
let[@inline] cc self = Theory_combine.cc (th_combine self)
let stats self = self.stat
let[@inline] tst self = Theory_combine.tst (th_combine self)
let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom (tst self) ?sign t in
mk_atom_lit self lit
let create ?(stat=Stat.global) ?size ?(config=Config.empty) ?store_proof ~theories () : t =
let th_combine = Theory_combine.create ~stat () in
let self = {
solver=Sat_solver.create ?store_proof ?size th_combine;
stat;
count_clause=Stat.mk_int stat "input-clauses";
count_solve=Stat.mk_int stat "solve";
config;
} in
(* now add the theories *)
Theory_combine.add_theory_l th_combine theories;
(* assert [true] and [not false] *)
let tst = tst self in
Sat_solver.assume self.solver [
[Lit.atom tst @@ Term.true_ tst];
] Proof_default;
self
(** {2 Toplevel Goals}
List of toplevel goals to satisfy. Mainly used for checking purpose
*)
module Top_goals: sig
val push : term -> unit
val to_seq : term Iter.t
val check: unit -> unit
end = struct
(* list of terms to fully evaluate *)
let toplevel_goals_ : term list ref = ref []
(* add [t] to the set of terms that must be evaluated *)
let push (t:term): unit =
toplevel_goals_ := t :: !toplevel_goals_;
()
let to_seq k = List.iter k !toplevel_goals_
(* FIXME
(* check that this term fully evaluates to [true] *)
let is_true_ (t:term): bool = match CC.normal_form t with
| None -> false
| Some (NF_bool b) -> b
| Some (NF_cstor _) -> assert false (* not a bool *)
let check () =
if not (List.for_all is_true_ !toplevel_goals_)
then (
if Config.progress then flush_progress();
Log.debugf 1
(fun k->
let pp_lit out t =
let nf = CC.normal_form t in
Format.fprintf out "(@[term: %a@ nf: %a@])"
Term.pp t (Fmt.opt pp_term_nf) nf
in
k "(@[<hv1>Top_goals.check@ (@[<v>%a@])@])"
(Util.pp_list pp_lit) !toplevel_goals_);
assert false;
)
*)
let check () : unit = ()
end
(** {2 Conversion} *)
(* list of constants we are interested in *)
let model_support_ : Cst.t list ref = ref []
let model_env_ : Ast.env ref = ref Ast.env_empty
let add_cst_support_ (c:cst): unit =
CCList.Ref.push model_support_ c
let add_ty_support_ (_ty:Ty.t): unit = ()
(** {2 Result} *)
type unknown =
| U_timeout
| U_max_depth
| U_incomplete
let pp_unknown out = function
| U_timeout -> Fmt.string out "timeout"
| U_max_depth -> Fmt.string out "max depth reached"
| U_incomplete -> Fmt.string out "incomplete fragment"
type model = Model.t
let pp_model = Model.pp
type res =
| Sat of model
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
(* convert unsat-core *)
let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
Iter.of_list core
|> Iter.map clause_of_mclause
(* print all terms reachable from watched literals *)
let pp_term_graph _out (_:t) =
()
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let do_on_exit ~on_exit =
List.iter (fun f->f()) on_exit;
()
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:Term.t) : unit =
Term.iter_dag t
|> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t)
|> Iter.filter
(fun t -> match Term.view t with
| Term.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub);
ignore (mk_atom_t self sub : Sat_solver.atom))
let assume (self:t) (c:Lit.t IArray.t) : unit =
let sat = solver self in
IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
Stat.incr self.count_clause;
Sat_solver.add_clause_a sat c Proof_default
(* TODO: remove? use a special constant + micro theory instead?
let[@inline] assume_distinct self l ~neq lit : unit =
CC.assert_distinct (cc self) l lit ~neq
*)
let check_model (_s:t) : unit =
Log.debug 1 "(smt.solver.check-model)";
(* TODO
Sat_solver.check_model s.solver
*)
()
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat st ->
Log.debugf 1 (fun k->k "SAT");
let lits f = st.iter_trail f (fun _ -> ()) in
let m = Theory_combine.mk_model (th_combine self) lits in
do_on_exit ~on_exit;
Sat m
(*
let env = Ast.env_empty in
let m = Model.make ~env in
…
Unknown U_incomplete (* TODO *)
*)
| Sat_solver.Unsat us ->
let pr =
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
with Msat.Solver_intf.No_proof -> None
in
do_on_exit ~on_exit;
Unsat pr
(* FIXME:
(* TODO: max_depth should actually correspond to the maximum depth
of un-expanded terms (expand in body of t --> depth = depth(t)+1),
so it corresponds to unfolding call graph to some depth *)
let solve ?(on_exit=[]) ?(check=true) () =
let n_iter = ref 0 in
let rec check_cc (): res =
assert (Backtrack.at_level_0 ());
if !n_iter > Config.max_depth then Unknown U_max_depth (* exceeded limit *)
else begin match CC.check () with
| CC.Unsat _ -> Unsat (* TODO proof *)
| CC.Sat lemmas ->
add_cc_lemmas lemmas;
check_solver()
end
and check_solver (): res =
(* assume all literals [expanded t] are false *)
let assumptions =
Terms_to_expand.to_seq
|> Iter.map (fun {Terms_to_expand.lit; _} -> Lit.neg lit)
|> Iter.to_rev_list
in
incr n_iter;
Log.debugf 2
(fun k->k
"(@[<1>@{<Yellow>solve@}@ @[:with-assumptions@ (@[%a@])@ n_iter: %d]@])"
(Util.pp_list Lit.pp) assumptions !n_iter);
begin match M.solve ~assumptions() with
| M.Sat _ ->
Log.debugf 1 (fun k->k "@{<Yellow>** found SAT@}");
do_on_exit ~on_exit;
let m = Model_build.make () in
if check then Model_build.check m;
Sat m
| M.Unsat us ->
let p = us.SI.get_proof () in
Log.debugf 4 (fun k->k "proof: @[%a@]@." pp_proof p);
let core = p |> M.unsat_core in
(* check if unsat because of assumptions *)
expand_next core
end
(* pick a term to expand, or UNSAT *)
and expand_next (core:unsat_core) =
begin match find_to_expand core with
| None -> Unsat (* TODO proof *)
| Some to_expand ->
let t = to_expand.Terms_to_expand.term in
Log.debugf 2 (fun k->k "(@[<1>@{<green>expand_next@}@ :term %a@])" Term.pp t);
CC.expand_term t;
Terms_to_expand.remove t;
Clause.push_new (Clause.make [to_expand.Terms_to_expand.lit]);
Backtrack.backtrack_to_level_0 ();
check_cc () (* recurse *)
end
in
check_cc()
*)

77
src/msat-solver/Solver.mli
View file

@ -1,77 +0,0 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Solver}
The solving algorithm, based on MCSat *)
module Sat_solver : Msat.S
with type Formula.t = Lit.t
and type theory = Theory_combine.t
and type lemma = Theory_combine.proof
(** {2 Result} *)
type model = Model.t
module Atom = Sat_solver.Atom
module Proof : sig
type t = Sat_solver.Proof.t
val check : t -> unit
end
type unknown =
| U_timeout
| U_max_depth
| U_incomplete
type res =
| Sat of Model.t
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
type t
(** Solver state *)
val create :
?stat:Stat.t ->
?size:[`Big | `Tiny | `Small] ->
?config:Config.t ->
?store_proof:bool ->
theories:Theory.t list ->
unit -> t
val solver : t -> Sat_solver.t
val th_combine : t -> Theory_combine.t
val add_theory : t -> Theory.t -> unit
val cc : t -> CC.t
val stats : t -> Stat.t
val tst : t -> Term.state
val mk_atom_lit : t -> Lit.t -> Atom.t
val mk_atom_t : t -> ?sign:bool -> Term.t -> Atom.t
val assume : t -> Lit.t IArray.t -> unit
(* TODO: use the theory instead
val assume_distinct : t -> Term.t list -> neq:Term.t -> Lit.t -> unit
*)
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
assumptions:Atom.t list ->
t ->
res
(** [solve s] checks the satisfiability of the statement added so far to [s]
@param check if true, the model is checked before returning
@param on_exit functions to be run before this returns *)
val check_model : t -> unit
val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer
val pp_unknown : unknown CCFormat.printer

182
src/msat-solver/Solver_types.ml
View file

@ -1,182 +0,0 @@
module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
(* main term cell. *)
type term = {
mutable term_id: int; (* unique ID *)
mutable term_ty: ty;
term_view : term term_view;
}
(* term shallow structure *)
and 'a term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t (* full, first-order application *)
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
(* boolean literal *)
and lit = {
lit_term: term;
lit_sign: bool;
}
and cst = {
cst_id: ID.t;
cst_view: cst_view;
}
and cst_view =
| Cst_undef of fun_ty (* simple undefined constant *)
| Cst_def of {
pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
ty : ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
}
(** Methods on the custom term view whose arguments are ['a].
Terms must be printable, and provide some additional theory handles.
- [relevant] must return a subset of [args] (possibly the same set).
The terms it returns will be activated and evaluated whenever possible.
Terms in [args \ relevant args] are considered for
congruence but not for evaluation.
*)
(** Function type *)
and fun_ty = {
fun_ty_args: ty list;
fun_ty_ret: ty;
}
(** Hashconsed type *)
and ty = {
mutable ty_id: int;
ty_view: ty_view;
}
and ty_view =
| Ty_prop
| Ty_atomic of {
def: ty_def;
args: ty list;
card: ty_card lazy_t;
}
and ty_def =
| Ty_uninterpreted of ID.t
| Ty_def of {
id: ID.t;
pp: ty Fmt.printer -> ty list Fmt.printer;
default_val: value list -> value; (* default value of this type *)
card: ty list -> ty_card;
}
and ty_card =
| Finite
| Infinite
(** Semantic values, used for models (and possibly model-constructing calculi) *)
and value =
| V_bool of bool
| V_element of {
id: ID.t;
ty: ty;
} (** a named constant, distinct from any other constant *)
| V_custom of {
view: value_custom_view;
pp: value_custom_view Fmt.printer;
eq: value_custom_view -> value_custom_view -> bool;
hash: value_custom_view -> int;
} (** Custom value *)
and value_custom_view = ..
type proof = Proof_default
type sat_actions = (Msat.void, lit, Msat.void, proof) Msat.acts
let[@inline] term_equal_ (a:term) b = a==b
let[@inline] term_hash_ a = a.term_id
let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id
let cmp_lit a b =
let c = CCBool.compare a.lit_sign b.lit_sign in
if c<>0 then c
else term_cmp_ a.lit_term b.lit_term
let cst_compare a b = ID.compare a.cst_id b.cst_id
let hash_lit a =
let sign = a.lit_sign in
Hash.combine3 2 (Hash.bool sign) (term_hash_ a.lit_term)
let pp_cst out a = ID.pp out a.cst_id
let id_of_cst a = a.cst_id
let[@inline] eq_ty a b = a.ty_id = b.ty_id
let eq_value a b = match a, b with
| V_bool a, V_bool b -> a=b
| V_element e1, V_element e2 ->
ID.equal e1.id e2.id && eq_ty e1.ty e2.ty
| V_custom x1, V_custom x2 ->
x1.eq x1.view x2.view
| V_bool _, _ | V_element _, _ | V_custom _, _
-> false
let hash_value a = match a with
| V_bool a -> Hash.bool a
| V_element e -> ID.hash e.id
| V_custom x -> x.hash x.view
let pp_value out = function
| V_bool b -> Fmt.bool out b
| V_element e -> ID.pp out e.id
| V_custom c -> c.pp out c.view
let pp_db out (i,_) = Format.fprintf out "%%%d" i
let rec pp_ty out t = match t.ty_view with
| Ty_prop -> Fmt.string out "prop"
| Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
| Ty_atomic {def=Ty_uninterpreted id; args; _} ->
Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
| Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args
let pp_term_view_gen ~pp_id ~pp_t out = function
| Bool true -> Fmt.string out "true"
| Bool false -> Fmt.string out "false"
| App_cst ({cst_view=Cst_def {pp=Some pp_custom;_};_},l) -> pp_custom pp_t out l
| App_cst (c, a) when IArray.is_empty a ->
pp_id out (id_of_cst c)
| App_cst (f,l) ->
Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_cst f) (Util.pp_iarray pp_t) l
| Eq (a,b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
| If (a, b, c) ->
Fmt.fprintf out "(@[if %a@ %a@ %a@])" pp_t a pp_t b pp_t c
| Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
let pp_term_top ~ids out t =
let rec pp out t =
pp_rec out t;
(* FIXME if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id; *)
and pp_rec out t = pp_term_view_gen ~pp_id ~pp_t:pp_rec out t.term_view
and pp_id = if ids then ID.pp else ID.pp_name in
pp out t
let pp_term = pp_term_top ~ids:false
let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
let pp_lit out l =
if l.lit_sign then pp_term out l.lit_term
else Format.fprintf out "(@[@<1>¬@ %a@])" pp_term l.lit_term
let pp_proof out = function
| Proof_default -> Fmt.fprintf out "<default proof>"

132
src/msat-solver/Theory.ml
View file

@ -1,132 +0,0 @@
(** {1 All the context for a theory} *)
module type ENV = sig
include Sidekick_cc.TERM_LIT
module CC : Sidekick_cc.S
(* TODO: useful?
module Th_clause : sig
type t = Lit.t IArray.t
val pp : t CCFormat.printer
end
= struct
type t = Lit.t IArray.t
let pp out c =
if IArray.length c = 0 then CCFormat.string out "false"
else if IArray.length c = 1 then Lit.pp out (IArray.get c 0)
else (
Format.fprintf out "[@[<hv>%a@]]"
(Util.pp_iarray ~sep:" ∨ " Lit.pp) c
)
end
*)
(** Unsatisfiable conjunction.
Its negation will become a conflict clause *)
type conflict = Lit.t list
(** {3 Actions available to some of the theory's callbacks} *)
module type ACTIONS = sig
val cc : CC.t
val raise_conflict: conflict -> 'a
(** Give a conflict clause to the solver *)
val propagate: Lit.t -> (unit -> Lit.t list) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: Lit.t -> Lit.t list -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_lit : Lit.t -> unit
(** Add the given literal to the SAT solver, so it gets assigned
a boolean value *)
val add_local_axiom: Lit.t list -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_persistent_axiom: Lit.t list -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
end
type actions = (module ACTIONS)
(** {3 Context given to a theory} *)
module Ctx : sig
type t
val cc : t -> CC.t
val on_partial_check : t -> (actions -> Lit.t Iter.t -> unit) -> unit
(** Called when a literal becomes true *)
val on_final_check: t -> (actions -> Lit.t Iter.t -> unit) -> unit
(** Final check, must be complete (i.e. must raise a conflict
if the set of literals is not satisfiable) *)
val on_mk_model : t -> (Lit.t Iter.t -> Model.t -> Model.t) -> unit
(** Update the given model *)
(**/**)
val on_check_invariants : t -> (unit -> unit) -> unit
(**/**)
end
(** {3 A theory's state} *)
module type THEORY = sig
type t
val name : string
(** Name of the theory *)
val create : Term.state -> t
(** Instantiate the theory's state *)
val setup : t -> Ctx.t -> unit
(** Setup the theory with the given context, including a
congruence closure *)
val push_level : t -> unit
val pop_levels : t -> int -> unit
end
type theory = (module THEORY)
(* TODO: remove?
let make
(type st)
?(check_invariants=fun _ -> ())
?(on_new_term=fun _ _ _ -> ())
?(on_merge=fun _ _ _ _ _ -> ())
?(partial_check=fun _ _ _ -> ())
?(mk_model=fun _ _ m -> m)
?(push_level=fun _ -> ())
?(pop_levels=fun _ _ -> ())
?(cc_th=fun _->[])
~name
~final_check
~create
() : t =
let module A = struct
type nonrec t = st
let name = name
let create = create
let on_new_term = on_new_term
let on_merge = on_merge
let partial_check = partial_check
let final_check = final_check
let mk_model = mk_model
let check_invariants = check_invariants
let push_level = push_level
let pop_levels = pop_levels
let cc_th = cc_th
end in
(module A : S)
*)
end

162
src/msat-solver/Theory_combine.ml
View file

@ -1,162 +0,0 @@
(** {1 Main theory} *)
(** Combine the congruence closure with a number of plugins *)
open Solver_types
module Proof = struct
type t = Solver_types.proof
let default = Proof_default
end
module Formula = Lit
module Eq_class = CC.N
module Expl = CC.Expl
type formula = Lit.t
type proof = Proof.t
type conflict = Theory.conflict
type theory_state =
| Th_state : ('a Theory.t1 * 'a) -> theory_state
(* TODO: first-class module instead *)
type t = {
tst: Term.state; (** state for managing terms *)
cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t;
count_axiom: int Stat.counter;
count_conflict: int Stat.counter;
count_propagate: int Stat.counter;
mutable theories : theory_state list; (** Set of theories *)
}
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] theories (self:t) : theory_state Iter.t =
fun k -> List.iter k self.theories
(** {2 Interface with the SAT solver} *)
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) acts (lits:Lit.t Iter.t) : unit =
Msat.Log.debugf 2
(fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
(if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
let cc = cc self in
if not final then (
CC.assert_lits cc lits;
);
(* transmit to theories. *)
CC.check cc acts;
let module A = struct
let cc = cc
let[@inline] raise_conflict c : 'a =
Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c Proof_default
let[@inline] propagate p cs : unit =
Stat.incr self.count_propagate;
acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), Proof_default))
let[@inline] propagate_l p cs : unit = propagate p (fun()->cs)
let[@inline] add_local_axiom lits : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep:false lits Proof_default
let[@inline] add_persistent_axiom lits : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep:true lits Proof_default
let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit
end in
let acts = (module A : Theory.ACTIONS) in
theories self
(fun (Th_state ((module Th),st)) ->
(* give new merges, then call {final,partial}-check *)
if final then Th.final_check st acts lits else Th.partial_check st acts lits);
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f ->
acts.Msat.acts_iter_assumptions
(function
| Msat.Lit a -> f a
| Msat.Assign _ -> assert false)
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts:_ Msat.acts) =
let iter = iter_atoms_ acts in
(* TODO if Config.progress then print_progress(); *)
Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter));
assert_lits_ ~final self acts iter
let add_formula (self:t) (lit:Lit.t) =
let t = Lit.term lit in
let lazy cc = self.cc in
let n = CC.add_term cc t in
CC.set_as_lit cc n (Lit.abs lit);
()
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:false self acts
(* perform final check of the model *)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts
let push_level (self:t) : unit =
CC.push_level (cc self);
theories self (fun (Th_state ((module Th), st)) -> Th.push_level st)
let pop_levels (self:t) n : unit =
CC.pop_levels (cc self) n;
theories self (fun (Th_state ((module Th), st)) -> Th.pop_levels st n)
let mk_model (self:t) lits : Model.t =
let m =
Iter.fold
(fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
Model.empty (theories self)
in
(* now complete model using CC *)
CC.mk_model (cc self) m
(** {2 Interface to Congruence Closure} *)
(** {2 Main} *)
(* create a new theory combination *)
let create ?(stat=Stat.global) () : t =
Log.debug 5 "th_combine.create";
let rec self = {
tst=Term.create ~size:1024 ();
cc = lazy (
(* lazily tie the knot *)
(* TODO: pass theories *)
CC.create ~size:`Big self.tst;
);
theories = [];
stat;
count_axiom = Stat.mk_int stat "th-axioms";
count_propagate = Stat.mk_int stat "th-propagations";
count_conflict = Stat.mk_int stat "th-conflicts";
} in
ignore (Lazy.force @@ self.cc : CC.t);
self
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
CC.check_invariants (cc self);
)
let add_theory (self:t) (th:Theory.t) : unit =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
let st = Th.create self.tst in
(* add micro theories *)
List.iter (CC.add_th (cc self)) (Th.cc_th st);
(* re-pack as a [Theory.t1] *)
self.theories <- (Th_state ((module Th),st)) :: self.theories
let add_theory_l self = List.iter (add_theory self)

29
src/msat-solver/Theory_combine.mli
View file

@ -1,29 +0,0 @@
(** {1 Main theory} *)
(** Combine the congruence closure with a number of plugins *)
module Proof : sig
type t = Solver_types.proof (* dummy proofs, for now *)
end
include Msat.Solver_intf.PLUGIN_CDCL_T
with module Formula = Lit
and type proof = Proof.t
val create : ?stat:Stat.t -> unit -> t
val cc : t -> CC.t
val tst : t -> Term.state
type theory_state =
| Th_state : ('a Theory.t1 * 'a) -> theory_state
val theories : t -> theory_state Iter.t
val mk_model : t -> Lit.t Iter.t -> Model.t
val add_theory : t -> Theory.t -> unit
(** How to add new theories *)
val add_theory_l : t -> Theory.t list -> unit

239
src/smtlib/Sidekick_smtlib.ml
View file

@ -2,11 +2,16 @@
(** {1 Process Statements} *)
module Fmt = CCFormat
module Ast = Sidekick_smt.Ast
module Ast = Sidekick_base_term.Ast
module E = CCResult
module Loc = Locations
module Process = Process
module Proof = struct
type t = Proof_default
let default = Proof_default
end
type 'a or_error = ('a, string) CCResult.t
module Parse = struct
@ -45,5 +50,237 @@ module Parse = struct
with e -> Result.Error (Printexc.to_string e)
end
module Term_bool : sig
open Sidekick_th_bool
type 'a view = 'a Bool_intf.view
type term = Sidekick_smt.Term.t
include Bool_intf.BOOL_TERM
with type t = term
and type state = Sidekick_smt.Term.state
val and_ : state -> term -> term -> term
val or_ : state -> term -> term -> term
val not_ : state -> term -> term
val imply : state -> term -> term -> term
val imply_a : state -> term IArray.t -> term -> term
val imply_l : state -> term list -> term -> term
val eq : state -> term -> term -> term
val neq : state -> term -> term -> term
val and_a : state -> term IArray.t -> term
val and_l : state -> term list -> term
val or_a : state -> term IArray.t -> term
val or_l : state -> term list -> term
end = struct
module ID = Sidekick_smt.ID
module T = Sidekick_smt.Term
module Ty = Sidekick_smt.Ty
open Sidekick_smt.Solver_types
open Bool_intf
type term = T.t
type t = T.t
type state = T.state
type 'a view = 'a Bool_intf.view
exception Not_a_th_term
let id_and = ID.make "and"
let id_or = ID.make "or"
let id_imply = ID.make "=>"
let equal = T.equal
let hash = T.hash
let view_id cst_id args =
if ID.equal cst_id id_and then (
B_and args
) else if ID.equal cst_id id_or then (
B_or args
) else if ID.equal cst_id id_imply && IArray.length args >= 2 then (
(* conclusion is stored first *)
let len = IArray.length args in
B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
) else (
raise_notrace Not_a_th_term
)
let view_as_bool (t:T.t) : T.t view =
match T.view t with
| Not u -> B_not u
| App_cst ({cst_id; _}, args) ->
(try view_id cst_id args with Not_a_th_term -> B_atom t)
| _ -> B_atom t
module C = struct
let get_ty _ _ = Ty.prop
let abs ~self _a =
match T.view self with
| Not u -> u, false
| _ -> self, true
let eval id args =
let module Value = Sidekick_smt.Value in
match view_id id args with
| B_not (V_bool b) -> Value.bool (not b)
| B_and a when IArray.for_all Value.is_true a -> Value.true_
| B_and a when IArray.exists Value.is_false a -> Value.false_
| B_or a when IArray.exists Value.is_true a -> Value.true_
| B_or a when IArray.for_all Value.is_false a -> Value.false_
| B_imply (_, V_bool true) -> Value.true_
| B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_
| B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_
| B_atom v -> v
| B_not _ | B_and _ | B_or _ | B_imply _
-> Error.errorf "non boolean value in boolean connective"
(* no congruence closure for boolean terms *)
let relevant _id _ _ = false
let mk_cst ?(do_cc=false) id : cst =
{cst_id=id;
cst_view=Cst_def {
pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; }
let not = T.not_
let and_ = mk_cst id_and
let or_ = mk_cst id_or
let imply = mk_cst id_imply
end
let as_id id (t:T.t) : T.t IArray.t option =
match T.view t with
| App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args
| _ -> None
(* flatten terms of the given ID *)
let flatten_id op sign (l:T.t list) : T.t list =
CCList.flat_map
(fun t -> match as_id op t with
| Some args -> IArray.to_list args
| None when (sign && T.is_true t) || (not sign && T.is_false t) ->
[] (* idempotent *)
| None -> [t])
l
let and_l st l =
match flatten_id id_and true l with
| [] -> T.true_ st
| l when List.exists T.is_false l -> T.false_ st
| [x] -> x
| args -> T.app_cst st C.and_ (IArray.of_list args)
let or_l st l =
match flatten_id id_or false l with
| [] -> T.false_ st
| l when List.exists T.is_true l -> T.true_ st
| [x] -> x
| args -> T.app_cst st C.or_ (IArray.of_list args)
let and_ st a b = and_l st [a;b]
let or_ st a b = or_l st [a;b]
let and_a st a = and_l st (IArray.to_list a)
let or_a st a = or_l st (IArray.to_list a)
let eq = T.eq
let not_ = T.not_
let neq st a b = not_ st @@ eq st a b
let imply_a st xs y =
if IArray.is_empty xs then y
else T.app_cst st C.imply (IArray.append (IArray.singleton y) xs)
let imply_l st xs y = match xs with
| [] -> y
| _ -> T.app_cst st C.imply (IArray.of_list @@ y :: xs)
let imply st a b = imply_a st (IArray.singleton a) b
let make st = function
| B_atom t -> t
| B_and l -> and_a st l
| B_or l -> or_a st l
| B_imply (a,b) -> imply_a st a b
| B_not t -> not_ st t
end
module Term_distinct = struct
open Sidekick_base_term
let id_distinct = ID.make "distinct"
let relevant _id _ _ = true
let get_ty _ _ = Ty.prop
let abs ~self _a = self, true
module T = struct
include Term
let mk_eq = eq
let as_distinct t : _ option =
match view t with
| App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
Some (IArray.to_seq args)
| _ -> None
end
module Lit = Sidekick_smt.Lit
let eval args =
let module Value = Sidekick_smt.Value in
Log.debugf 5
(fun k->k "(@[distinct.eval@ %a@])" (Fmt.seq Value.pp) (IArray.to_seq args));
if
Iter.diagonal (IArray.to_seq args)
|> Iter.for_all (fun (x,y) -> not @@ Value.equal x y)
then Value.true_
else Value.false_
let c_distinct =
{cst_id=id_distinct;
cst_view=Cst_def {
pp=None; abs; ty=get_ty; relevant; do_cc=true; eval; }; }
let distinct st a =
if IArray.length a <= 1
then T.true_ st
else T.app_cst st c_distinct a
let distinct_l st = function
| [] | [_] -> T.true_ st
| xs -> distinct st (IArray.of_list xs)
end
module Term_ite = struct
open Sidekick_base_term
let[@inline] view_as_ite t = match Term.view t with
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
module Solver = Sidekick_msat_solver.Solver
module Theories = struct
module Th_cstor = Sidekick_th_cstor.Make(struct
module Solver = Solver
module T = Solver.A.Term
let[@inline] view_as_cstor t = match view t with
| App_cst (c, args) when Fun.do_cc
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
end)
end
let parse = Parse.parse
let parse_stdin = Parse.parse_stdin

2
src/smtlib/dune
View file

@ -4,7 +4,7 @@
(public_name sidekick.smtlib)
(libraries containers zarith msat sidekick.core sidekick.util
sidekick.msat-solver sidekick.base-term
sidekick.smt.th-bool sidekick.smt.th-distinct msat.backend)
sidekick.th-bool sidekick.th-distinct msat.backend)
(flags :standard -open Sidekick_util))
(menhir (modules Parser))