simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-23 09:56:40 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: remove all traces of mcsat from src/sat

Browse source
This commit is contained in:
Simon Cruanes 2021-07-18 02:01:19 -04:00
parent 564dcec252
commit 4cb8887639
8 changed files with 1953 additions and 2551 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/backend/Dot.mli
View file

@ -57,13 +57,13 @@ module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) : S with type t := S.proof
and type assumption := S.clause) : S with type t := S.Proof.t
(** Functor for making a module to export proofs to the DOT format. *)
module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula
and type hyp = S.formula list
and type lemma := S.lemma
and type assumption = S.formula) : S with type t := S.proof
and type assumption = S.formula) : S with type t := S.Proof.t
(** Functor for making a module to export proofs to the DOT format.
The substitution of the hyp type is non-destructive due to a restriction
of destructive substitutions on earlier versions of ocaml. *)

22
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -74,7 +74,7 @@ module Make(A : ARG)
type lit = Lit_.t
(* actions from msat *)
type msat_acts = (Sidekick_sat.void, lit, Sidekick_sat.void, P.t) Sidekick_sat.acts
type msat_acts = (lit, P.t) Sidekick_sat.acts
(* the full argument to the congruence closure *)
module CC_actions = struct
@ -427,7 +427,7 @@ module Make(A : ARG)
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
Sidekick_sat.Log.debugf 2
Log.debugf 2
(fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])"
(if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
@ -455,17 +455,13 @@ module Make(A : ARG)
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f ->
acts.Sidekick_sat.acts_iter_assumptions
(function
| Sidekick_sat.Lit a -> f a
| Sidekick_sat.Assign _ -> assert false)
fun f -> acts.Sidekick_sat.acts_iter_assumptions f
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
let iter = iter_atoms_ acts in
Sidekick_sat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
self.on_progress();
assert_lits_ ~final self acts iter;
Profile.exit pb
@ -517,7 +513,7 @@ module Make(A : ARG)
module SC = Sat_solver.Clause
type t = {
msat: Sat_solver.proof;
msat: Sat_solver.Proof.t;
tdefs: (term*term) list; (* term definitions *)
p: P.t lazy_t;
}
@ -539,7 +535,7 @@ module Make(A : ARG)
clause [c] under given assumptions (each assm is a lit),
and return [-a1 \/ … \/ -an \/ c], discharging assumptions
*)
let conv_proof (msat:Sat_solver.proof) (t_defs:_ list) : P.t =
let conv_proof (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
let assms = ref [] in
let steps = ref [] in
@ -547,7 +543,7 @@ module Make(A : ARG)
let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *)
(* name of an already processed proof node *)
let find_proof_name (p:Sat_solver.proof) : string =
let find_proof_name (p:Sat_solver.Proof.t) : string =
try SC.Tbl.find n_tbl_ (SP.conclusion p)
with Not_found ->
Error.errorf
@ -631,7 +627,7 @@ module Make(A : ARG)
let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
let make (msat: Sat_solver.proof) (tdefs: _ list) : t =
let make (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
{ msat; tdefs; p=lazy (conv_proof msat tdefs) }
let check self = SP.check self.msat
@ -912,7 +908,7 @@ module Make(A : ARG)
match r with
| Sat_solver.Sat st ->
Log.debug 1 "sidekick.msat-solver: SAT";
let _lits f = st.iter_trail f (fun _ -> ()) in
let _lits f = st.iter_trail f in
(* TODO: theory combination *)
let m = mk_model self _lits in
do_on_exit ();

2275
src/sat/Internal.ml
View file

File diff suppressed because it is too large Load diff

31
src/sat/Sidekick_sat.ml
View file

@ -5,21 +5,15 @@ module Solver_intf = Solver_intf
module type S = Solver_intf.S
module type FORMULA = Solver_intf.FORMULA
module type EXPR = Solver_intf.EXPR
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT
module type PROOF = Solver_intf.PROOF
(** Empty type *)
type void = (unit,bool) Solver_intf.gadt_eq
type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = {
type 'form sat_state = 'form Solver_intf.sat_state = {
eval : 'form -> bool;
eval_level : 'form -> bool * int;
iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
model : unit -> ('term * 'value) list;
iter_trail : ('form -> unit) -> unit;
}
type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = {
@ -32,22 +26,16 @@ type 'clause export = 'clause Solver_intf.export = {
history : 'clause Vec.t;
}
type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption =
| Lit of 'formula (** The given formula is asserted true by the solver *)
| Assign of 'term * 'value (** The term is assigned to the value *)
type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
| Eval of 'term list
type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'formula list * 'proof)
type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = {
acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts = {
acts_iter_assumptions: ('formula -> unit) -> unit;
acts_eval_lit: 'formula -> lbool;
acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
acts_mk_term: 'term -> unit;
acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
acts_propagate : 'formula -> ('formula, 'proof) reason -> unit;
acts_add_decision_lit: 'formula -> bool -> unit;
}
@ -66,11 +54,4 @@ let pp_lbool out = function
exception No_proof = Solver_intf.No_proof
module Make_mcsat = Solver.Make_mcsat
module Make_cdcl_t = Solver.Make_cdcl_t
module Make_pure_sat = Solver.Make_pure_sat
(**/**)
module Vec = Vec
module Log = Log
(**/**)

1932
src/sat/Solver.ml
View file

File diff suppressed because it is too large Load diff

34
src/sat/Solver.mli
View file

@ -1,34 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** mSAT safe interface
This module defines a safe interface for the core solver.
It is the basis of the {!module:Solver} and {!module:Mcsolver} modules.
*)
module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
: S with type Term.t = Solver_intf.void
and module Formula = Th.Formula
and type lemma = Th.proof
and type theory = Th.t
module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT)
: S with module Term = Th.Term
and module Formula = Th.Formula
and type lemma = Th.proof
and type theory = Th.t
module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
: S with type Term.t = Solver_intf.void
and module Formula = Th.Formula
and type lemma = Th.proof
and type theory = unit

114
src/sat/Solver_intf.ml
View file

@ -13,7 +13,7 @@ Copyright 2016 Simon Cruanes
type 'a printer = Format.formatter -> 'a -> unit
type ('term, 'form, 'value) sat_state = {
type 'form sat_state = {
eval: 'form -> bool;
(** Returns the valuation of a formula in the current state
of the sat solver.
@ -24,11 +24,9 @@ type ('term, 'form, 'value) sat_state = {
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
(** Iter thorugh the formulas and terms in order of decision/propagation
iter_trail : ('form -> unit) -> unit;
(** Iter through the formulas in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
model: unit -> ('term * 'value) list;
(** Returns the model found if the formula is satisfiable. *)
}
(** The type of values returned when the solver reaches a SAT state. *)
@ -68,14 +66,7 @@ type 'term eval_res =
- [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
*)
type ('term, 'formula, 'value) assumption =
| Lit of 'formula (** The given formula is asserted true by the solver *)
| Assign of 'term * 'value (** The term is assigned to the value *)
(** Asusmptions made by the core SAT solver. *)
type ('term, 'formula, 'proof) reason =
| Eval of 'term list
(** The formula can be evalutaed using the terms in the list *)
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof)
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
@ -101,8 +92,8 @@ type lbool = L_true | L_false | L_undefined
(** Valuation of an atom *)
(* TODO: find a way to use atoms instead of formulas here *)
type ('term, 'formula, 'value, 'proof) acts = {
acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
type ('formula, 'proof) acts = {
acts_iter_assumptions: ('formula -> unit) -> unit;
(** Traverse the new assumptions on the boolean trail. *)
acts_eval_lit: 'formula -> lbool;
@ -112,10 +103,6 @@ type ('term, 'formula, 'value, 'proof) acts = {
(** Map the given formula to a literal, which will be decided by the
SAT solver. *)
acts_mk_term: 'term -> unit;
(** Map the given term (and its subterms) to decision variables,
for the MCSAT solver to decide. *)
acts_add_clause: ?keep:bool -> 'formula list -> 'proof -> unit;
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
@ -128,7 +115,7 @@ type ('term, 'formula, 'value, 'proof) acts = {
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
acts_propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit;
acts_propagate: 'formula -> ('formula, 'proof) reason -> unit;
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
(see the definition of {!type:eval_res} *)
@ -139,11 +126,6 @@ type ('term, 'formula, 'value, 'proof) acts = {
}
(** The type for a slice of assertions to assume/propagate in the theory. *)
type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq
type void = (unit,bool) gadt_eq
(** A provably empty type *)
exception No_proof
module type FORMULA = sig
@ -172,37 +154,6 @@ module type FORMULA = sig
but one returns [Negated] and the other [Same_sign]. *)
end
(** Formulas and Terms required for mcSAT *)
module type EXPR = sig
type proof
(** An abstract type for proofs *)
module Term : sig
type t
(** The type of terms *)
val equal : t -> t -> bool
(** Equality over terms. *)
val hash : t -> int
(** Hashing function for terms. Should be such that two terms equal according
to {!equal} have the same hash. *)
val pp : t printer
(** Printing function used among other for debugging. *)
end
module Value : sig
type t
(** The type of semantic values (domain elements) *)
val pp : t printer
(** Printing function used among other for debugging. *)
end
module Formula : FORMULA
end
(** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig
type t
@ -218,52 +169,18 @@ module type PLUGIN_CDCL_T = sig
val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *)
val partial_check : t -> (void, Formula.t, void, proof) acts -> unit
val partial_check : t -> (Formula.t, proof) acts -> unit
(** Assume the formulas in the slice, possibly using the [slice]
to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> (void, Formula.t, void, proof) acts -> unit
val final_check : t -> (Formula.t, proof) acts -> unit
(** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed;
if a conflict clause is added, search backtracks and then resumes. *)
end
(** Signature for theories to be given to the Model Constructing Solver. *)
module type PLUGIN_MCSAT = sig
type t
(** The plugin state itself *)
include EXPR
val push_level : t -> unit
(** Create a new backtrack level *)
val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *)
val partial_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit
(** Assume the formulas in the slice, possibly using the [slice]
to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit
(** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed;
if a conflict clause is added, search backtracks and then resumes. *)
val assign : t -> Term.t -> Value.t
(** Returns an assignment value for the given term. *)
val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit
(** An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts) *)
val eval : t -> Formula.t -> Term.t eval_res
(** Returns the evaluation of the Formula.t in the current assignment *)
end
(** Signature for pure SAT solvers *)
module type PLUGIN_SAT = sig
module Formula : FORMULA
@ -386,9 +303,7 @@ module type S = sig
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
include EXPR
type term = Term.t (** user terms *)
module Formula : FORMULA
type formula = Formula.t (** user formulas *)
@ -406,6 +321,7 @@ module type S = sig
type solver
(* TODO: keep this internal *)
module Atom : sig
type t = atom
@ -437,7 +353,6 @@ module type S = sig
and type atom = atom
and type formula = formula
and type lemma = lemma
and type t = proof
(** A module to manipulate proofs. *)
type t = solver
@ -465,7 +380,7 @@ module type S = sig
(** Result type for the solver *)
type res =
| Sat of (term,formula,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *)
| Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
@ -492,11 +407,6 @@ module type S = sig
The assumptions are just used for this call to [solve], they are
not saved in the solver's state. *)
val make_term : t -> term -> unit
(** Add a new term (i.e. decision variable) to the solver. This term will
be decided on at some point during solving, wether it appears
in clauses or not. *)
val make_atom : t -> formula -> atom
(** Add a new atom (i.e propositional formula) to the solver.
This formula will be decided on at some point during solving,

92
src/sat/msat.mld
View file

@ -1,92 +0,0 @@
{1 mSAT}
{2 License}
This code is free, under the {{:https://github.com/Gbury/mSAT/blob/master/LICENSE}Apache 2.0 license}.
{2 Contents}
mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely,
what mSAT provides are functors to easily create such solvers. Indeed, the core
of a sat solver does not need much information about either the exact representation
of terms or the inner workings of a theory.
Most modules in mSAT actually define functors. These functors usually take one
or two arguments, usually an implementation of Terms and formulas used, and an implementation
of the theory used during solving.
{4 Solver creation}
The following modules allow to easily create a SAT or SMT solver (remark: a SAT solver is
simply an SMT solver with an empty theory).
{!modules:
Msat
}
The following modules allow the creation of a McSat solver (Model Constructing solver):
{!modules:
Msat_mcsolver
}
{4 Useful tools}
An instanciation of a pure sat solver is also provided:
{!modules:
Msat_sat
}
Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:
{!modules:
Msat_tseitin
}
{4 Proof Management}
mSAT solvers are able to provide detailed proofs when an unsat state is reached. To do
so, it require the provided theory to give proofs of the tautologies it gives the solver.
These proofs will be called lemmas. The type of lemmas is defined by the theory and can
very well be [unit].
In this context a proof is a resolution tree, whose conclusion (i.e. root) is the
empty clause, effectively allowing to deduce [false] from the hypotheses.
A resolution tree is a binary tree whose nodes are clauses. Inner nodes' clauses are
obtained by performing resolution between the two clauses of the children nodes, while
leafs of the tree are either hypotheses, or tautologies (i.e. conflicts returned by
the theory).
{!modules:
Msat__Res
Msat__Res_intf
}
Backends for exporting proofs to different formats:
{!modules:
Dot
Coq
Dedukti
Backend_intf
}
{4 Internal modules}
WARNING: for advanced users only ! These modules expose a lot of unsafe functions
that must be used with care to not break the required invariants. Additionally, these
interfaces are not part of the main API and so are subject to a lot more breaking changes
than the safe modules above.
{!modules:
Dimacs
Internal
External
Solver_types
Solver_types_intf
}
{2 Index}
{!indexlist}