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

cleanup msat, rename it sidekick.sat

Browse source
This commit is contained in:
Simon Cruanes 2021-07-18 01:40:55 -04:00
parent 4a337a85d3
commit 564dcec252
24 changed files with 66 additions and 474 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

193
src/backend/Coq.ml
View file

@ -1,193 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)
module type S = Backend_intf.S
module type Arg = sig
type hyp
type lemma
type assumption
val prove_hyp : Format.formatter -> string -> hyp -> unit
val prove_lemma : Format.formatter -> string -> lemma -> unit
val prove_assumption : Format.formatter -> string -> assumption -> unit
end
module Make(S : Msat.S)(A : Arg with type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) = struct
module Atom = S.Atom
module Clause = S.Clause
module M = Map.Make(S.Atom)
module C_tbl = S.Clause.Tbl
module P = S.Proof
let name = Clause.name
let clause_map c =
let rec aux acc a i =
if i >= Array.length a then acc
else begin
let name = Format.sprintf "A%d" i in
aux (M.add a.(i) name acc) a (i + 1)
end
in
aux M.empty (Clause.atoms c) 0
let clause_iter m format fmt clause =
let aux atom = Format.fprintf fmt format (M.find atom m) in
Array.iter aux (Clause.atoms clause)
let elim_duplicate fmt goal hyp _ =
(** Printing info comment in coq *)
Format.fprintf fmt
"(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n"
(name goal) (name hyp);
(** Prove the goal: intro the atoms, then use them with the hyp *)
let m = clause_map goal in
Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
(clause_iter m "%s@ ") goal (name hyp)
(clause_iter m "@ %s") hyp (name goal)
let resolution_aux m a h1 h2 fmt () =
Format.fprintf fmt "%s%a" (name h1)
(fun fmt -> Array.iter (fun b ->
if b == a then begin
Format.fprintf fmt "@ (fun p =>@ %s%a)"
(name h2) (fun fmt -> (Array.iter (fun c ->
if Atom.equal c (Atom.neg a) then
Format.fprintf fmt "@ (fun np => np p)"
else
Format.fprintf fmt "@ %s" (M.find c m)))
) (Clause.atoms h2)
end else
Format.fprintf fmt "@ %s" (M.find b m)
)) (Clause.atoms h1)
let resolution fmt goal hyp1 hyp2 atom =
let a = Atom.abs atom in
let h1, h2 =
if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2
else (
assert (Array.exists (Atom.equal a) (Clause.atoms hyp2));
hyp2, hyp1
)
in
(** Print some debug info *)
Format.fprintf fmt
"(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
(name goal) (name h1) (name h2);
(** Prove the goal: intro the axioms, then perform resolution *)
if Array.length (Clause.atoms goal) = 0 then (
let m = M.empty in
Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
false
) else (
let m = clause_map goal in
Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
(clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
true
)
(* Count uses of hypotheses *)
let incr_use h c =
let i = try C_tbl.find h c with Not_found -> 0 in
C_tbl.add h c (i + 1)
let decr_use h c =
let i = C_tbl.find h c - 1 in
assert (i >= 0);
let () = C_tbl.add h c i in
i <= 0
let clear fmt c =
Format.fprintf fmt "clear %s." (name c)
let rec clean_aux fmt = function
| [] -> ()
| [x] ->
Format.fprintf fmt "%a@\n" clear x
| x :: ((_ :: _) as r) ->
Format.fprintf fmt "%a@ %a" clear x clean_aux r
let clean h fmt l =
match List.filter (decr_use h) l with
| [] -> ()
| l' ->
Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l'
let prove_node t fmt node =
let clause = node.P.conclusion in
match node.P.step with
| P.Hypothesis _ ->
A.prove_hyp fmt (name clause) clause
| P.Assumption ->
A.prove_assumption fmt (name clause) clause
| P.Lemma _ ->
A.prove_lemma fmt (name clause) clause
| P.Duplicate (p, l) ->
let c = P.conclusion p in
let () = elim_duplicate fmt clause c l in
clean t fmt [c]
| P.Hyper_res hr ->
let (p1, p2, a) = P.res_of_hyper_res hr in
let c1 = P.conclusion p1 in
let c2 = P.conclusion p2 in
if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
let count_uses p =
let h = C_tbl.create 128 in
let aux () node =
List.iter (fun p' -> incr_use h P.(conclusion p')) (P.parents node.P.step)
in
let () = P.fold aux () p in
h
(* Here the main idea is to always try and have exactly
one goal to prove, i.e False. So each *)
let pp fmt p =
let h = count_uses p in
let aux () node =
Format.fprintf fmt "%a" (prove_node h) node
in
Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
P.fold aux () p
end
module Simple(S : Msat.S)
(A : Arg with type hyp = S.formula list
and type lemma := S.lemma
and type assumption := S.formula) =
Make(S)(struct
module P = S.Proof
(* Some helpers *)
let lit = S.Atom.formula
let get_assumption c =
match S.Clause.atoms_l c with
| [ x ] -> x
| _ -> assert false
let get_lemma c =
match P.expand (P.prove c) with
| {P.step=P.Lemma p; _} -> p
| _ -> assert false
let prove_hyp fmt name c =
A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c))
let prove_lemma fmt name c =
A.prove_lemma fmt name (get_lemma c)
let prove_assumption fmt name c =
A.prove_assumption fmt name (lit (get_assumption c))
end)

46
src/backend/Coq.mli
View file

@ -1,46 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)
(** Coq Backend
This module provides an easy way to produce coq scripts
corresponding to the resolution proofs output by the
sat solver. *)
module type S = Backend_intf.S
(** Interface for exporting proofs. *)
module type Arg = sig
(** Term printing for Coq *)
type hyp
type lemma
type assumption
(** The types of hypotheses, lemmas, and assumptions *)
val prove_hyp : Format.formatter -> string -> hyp -> unit
val prove_lemma : Format.formatter -> string -> lemma -> unit
val prove_assumption : Format.formatter -> string -> assumption -> unit
(** Proving function for hypotheses, lemmas and assumptions.
[prove_x fmt name x] should prove [x], and be such that after
executing it, [x] is among the coq hypotheses under the name [name].
The hypothesis should be the encoding of the given clause, i.e
for a clause [a \/ not b \/ c], the proved hypothesis should be:
[ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
one in the atoms array of the clause. *)
end
module Make(S : Msat.S)(A : Arg with type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) : S with type t := S.proof
(** Base functor to output Coq proofs *)
module Simple(S : Msat.S)(A : Arg with type hyp = S.formula list
and type lemma := S.lemma
and type assumption := S.formula) : S with type t := S.proof
(** Simple functor to output Coq proofs *)

62
src/backend/Dedukti.ml
View file

@ -1,62 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)
module type S = Backend_intf.S
module type Arg = sig
type proof
type lemma
type formula
val pp : Format.formatter -> formula -> unit
val prove : Format.formatter -> lemma -> unit
val context : Format.formatter -> proof -> unit
end
module Make(S : Msat.S)(A : Arg with type formula := S.formula
and type lemma := S.lemma
and type proof := S.proof) = struct
module P = S.Proof
let pp_nl fmt = Format.fprintf fmt "@\n"
let fprintf fmt format = Format.kfprintf pp_nl fmt format
let _clause_name = S.Clause.name
let _pp_clause fmt c =
let rec aux fmt = function
| [] -> ()
| a :: r ->
let f, pos =
if S.Atom.sign a then
S.Atom.formula a, true
else
S.Atom.formula (S.Atom.neg a), false
in
fprintf fmt "%s _b %a ->@ %a"
(if pos then "_pos" else "_neg") A.pp f aux r
in
fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
let context fmt p =
fprintf fmt "(; Embedding ;)";
fprintf fmt "Prop : Type.";
fprintf fmt "_proof : Prop -> Type.";
fprintf fmt "(; Notations for clauses ;)";
fprintf fmt "_pos : Prop -> Prop -> Type.";
fprintf fmt "_neg : Prop -> Prop -> Type.";
fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
A.context fmt p
let pp fmt p =
fprintf fmt "#NAME Proof.";
fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
context fmt p;
()
end

32
src/backend/Dedukti.mli
View file

@ -1,32 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Deduki backend for proofs
Work in progress...
*)
module type S = Backend_intf.S
module type Arg = sig
type lemma
type proof
type formula
val pp : Format.formatter -> formula -> unit
val prove : Format.formatter -> lemma -> unit
val context : Format.formatter -> proof -> unit
end
module Make :
functor(S : Msat.S) ->
functor(A : Arg
with type formula := S.formula
and type lemma := S.lemma
and type proof := S.proof) ->
S with type t := S.proof
(** Functor to generate a backend to output proofs for the dedukti type checker. *)

6
src/backend/Dot.ml
View file

@ -28,7 +28,7 @@ module type Arg = sig
end end
module Default(S : Msat.S) = struct module Default(S : Sidekick_sat.S) = struct
module Atom = S.Atom module Atom = S.Atom
module Clause = S.Clause module Clause = S.Clause
@ -49,7 +49,7 @@ module Default(S : Msat.S) = struct
end end
(** Functor to provide dot printing *) (** Functor to provide dot printing *)
module Make(S : Msat.S)(A : 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 hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause) = struct and type assumption := S.clause) = struct
@ -151,7 +151,7 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
end end
module Simple(S : Msat.S) module Simple(S : Sidekick_sat.S)
(A : Arg with type atom := S.formula (A : Arg with type atom := S.formula
and type hyp = S.formula list and type hyp = S.formula list
and type lemma := S.lemma and type lemma := S.lemma

6
src/backend/Dot.mli
View file

@ -47,20 +47,20 @@ module type Arg = sig
end end
module Default(S : Msat.S) : Arg with type atom := S.atom module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
and type hyp := S.clause and type hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause and type assumption := S.clause
(** Provides a reasonnable default to instantiate the [Make] functor, assuming (** Provides a reasonnable default to instantiate the [Make] functor, assuming
the original printing functions are compatible with DOT html labels. *) the original printing functions are compatible with DOT html labels. *)
module Make(S : Msat.S)(A : 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 hyp := S.clause
and type lemma := 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
(** Functor for making a module to export proofs to the DOT format. *) (** Functor for making a module to export proofs to the DOT format. *)
module Simple(S : Msat.S)(A : Arg with type atom := S.formula module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula
and type hyp = S.formula list and type hyp = S.formula list
and type lemma := S.lemma 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

12
src/backend/dune
View file

@ -1,10 +1,6 @@
(library (library
(name msat_backend) (name sidekick_backend)
(public_name msat.backend) (public_name sidekick.backend)
(synopsis "proof backends for msat") (synopsis "Proof backends for sidekick")
(libraries msat) (libraries sidekick.sat))
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -warn-error -27 -color always -safe-string)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

29
src/backtrack/Backtrackable_ref.ml
View file

@ -1,29 +0,0 @@
type 'a t = {
mutable cur: 'a;
stack: 'a Vec.t;
copy: ('a -> 'a) option;
}
let create ?copy x: _ t =
{cur=x; stack=Vec.create(); copy}
let[@inline] get self = self.cur
let[@inline] set self x = self.cur <- x
let[@inline] update self f = self.cur <- f self.cur
let[@inline] n_levels self = Vec.size self.stack
let[@inline] push_level self : unit =
let x = self.cur in
let x = match self.copy with None -> x | Some f -> f x in
Vec.push self.stack x
let pop_levels self n : unit =
assert (n>=0);
if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
let i = Vec.size self.stack-n in
let x = Vec.get self.stack i in
self.cur <- x;
Vec.shrink self.stack i;
()

30
src/backtrack/Backtrackable_ref.mli
View file

@ -1,30 +0,0 @@
(** {1 Backtrackable ref} *)
type 'a t
val create : ?copy:('a -> 'a) -> 'a -> 'a t
(** Create a backtrackable reference holding the given value initially.
@param copy if provided, will be used to copy the value when [push_level]
is called. *)
val set : 'a t -> 'a -> unit
(** Set the reference's current content *)
val get : 'a t -> 'a
(** Get the reference's current content *)
val update : 'a t -> ('a -> 'a) -> unit
(** Update the reference's current content *)
val push_level : _ t -> unit
(** Push a backtracking level, copying the current value on top of some
stack. The [copy] function will be used if it was provided in {!create}. *)
val n_levels : _ t -> int
(** Number of saved values *)
val pop_levels : _ t -> int -> unit
(** Pop [n] levels, restoring to the value the reference was storing [n] calls
to [push_level] earlier.
@raise Invalid_argument if [n] is bigger than [n_levels]. *)

2
src/backtrack/Msat_backtrack.ml
View file

@ -1,2 +0,0 @@
module Ref = Backtrackable_ref

11
src/backtrack/dune
View file

@ -1,11 +0,0 @@
(library
(name msat_backtrack)
(public_name msat.backtrack)
(libraries msat)
(synopsis "backtrackable data structures for msat")
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8
-color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

4
src/base/Base_types.ml
View file

@ -1,7 +1,7 @@
(** Basic type definitions for Sidekick_base *) (** Basic type definitions for Sidekick_base *)
module Vec = Msat.Vec module Vec = Sidekick_util.Vec
module Log = Msat.Log module Log = Sidekick_util.Log
module Fmt = CCFormat module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view module CC_view = Sidekick_core.CC_view

1
src/main/main.ml
View file

@ -11,7 +11,6 @@ module Fmt = CCFormat
module Term = Sidekick_base.Term module Term = Sidekick_base.Term
module Solver = Sidekick_smtlib.Solver module Solver = Sidekick_smtlib.Solver
module Process = Sidekick_smtlib.Process module Process = Sidekick_smtlib.Process
module Vec = Msat.Vec
type 'a or_error = ('a, string) E.t type 'a or_error = ('a, string) E.t

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

@ -1,12 +1,10 @@
(** {1 Implementation of a Solver using Msat} *) (** Core of the SMT solver using Sidekick_sat
(** {{: https://github.com/Gbury/mSAT/} Msat} is a modular SAT solver in Sidekick_sat (in src/sat/) is a modular SAT solver in
pure OCaml. pure OCaml.
This builds a {!Sidekick_core.SOLVER} on top of it. *) This builds a {!Sidekick_core.SOLVER} on top of it.
*)
module Log = Msat.Log
(** A logging module *)
(** Argument to pass to the functor {!Make} in order to create a (** Argument to pass to the functor {!Make} in order to create a
new Msat-based SMT solver. *) new Msat-based SMT solver. *)
@ -76,7 +74,7 @@ module Make(A : ARG)
type lit = Lit_.t type lit = Lit_.t
(* actions from msat *) (* actions from msat *)
type msat_acts = (Msat.void, lit, Msat.void, P.t) Msat.acts type msat_acts = (Sidekick_sat.void, lit, Sidekick_sat.void, P.t) Sidekick_sat.acts
(* the full argument to the congruence closure *) (* the full argument to the congruence closure *)
module CC_actions = struct module CC_actions = struct
@ -91,10 +89,10 @@ module Make(A : ARG)
module Lit = Lit module Lit = Lit
type t = msat_acts type t = msat_acts
let[@inline] raise_conflict a lits pr = let[@inline] raise_conflict a lits pr =
a.Msat.acts_raise_conflict lits pr a.Sidekick_sat.acts_raise_conflict lits pr
let[@inline] propagate a lit ~reason = let[@inline] propagate a lit ~reason =
let reason = Msat.Consequence reason in let reason = Sidekick_sat.Consequence reason in
a.Msat.acts_propagate lit reason a.Sidekick_sat.acts_propagate lit reason
end end
end end
@ -218,7 +216,7 @@ module Make(A : ARG)
include Lit include Lit
let norm lit = let norm lit =
let lit', sign = norm_sign lit in let lit', sign = norm_sign lit in
lit', if sign then Msat.Same_sign else Msat.Negated lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated
end end
module Eq_class = CC.N module Eq_class = CC.N
module Expl = CC.Expl module Expl = CC.Expl
@ -244,22 +242,22 @@ module Make(A : ARG)
let push_decision (_self:t) (acts:actions) (lit:lit) : unit = let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
let sign = Lit.sign lit in let sign = Lit.sign lit in
acts.Msat.acts_add_decision_lit (Lit.abs lit) sign acts.Sidekick_sat.acts_add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self acts c proof : 'a = let[@inline] raise_conflict self acts c proof : 'a =
Stat.incr self.count_conflict; Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c proof acts.Sidekick_sat.acts_raise_conflict c proof
let[@inline] propagate self acts p ~reason : unit = let[@inline] propagate self acts p ~reason : unit =
Stat.incr self.count_propagate; Stat.incr self.count_propagate;
acts.Msat.acts_propagate p (Msat.Consequence reason) acts.Sidekick_sat.acts_propagate p (Sidekick_sat.Consequence reason)
let[@inline] propagate_l self acts p cs proof : unit = let[@inline] propagate_l self acts p cs proof : unit =
propagate self acts p ~reason:(fun()->cs,proof) propagate self acts p ~reason:(fun()->cs,proof)
let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit = let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
Stat.incr self.count_axiom; Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep lits proof acts.Sidekick_sat.acts_add_clause ~keep lits proof
let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof = let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
let mk_lit t = Lit.atom self.tst t in (* no further simplification *) let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
@ -377,7 +375,7 @@ module Make(A : ARG)
let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit = let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:true lits proof add_sat_clause_ self acts ~keep:true lits proof
let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit let add_lit _self acts lit : unit = acts.Sidekick_sat.acts_mk_lit lit
let add_lit_t self acts ?sign t = let add_lit_t self acts ?sign t =
let lit = mk_lit self acts ?sign t in let lit = mk_lit self acts ?sign t in
@ -429,7 +427,7 @@ module Make(A : ARG)
(* handle a literal assumed by the SAT solver *) (* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit = let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
Msat.Log.debugf 2 Sidekick_sat.Log.debugf 2
(fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])" (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); (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
(* transmit to CC *) (* transmit to CC *)
@ -458,26 +456,26 @@ module Make(A : ARG)
let[@inline] iter_atoms_ acts : _ Iter.t = let[@inline] iter_atoms_ acts : _ Iter.t =
fun f -> fun f ->
acts.Msat.acts_iter_assumptions acts.Sidekick_sat.acts_iter_assumptions
(function (function
| Msat.Lit a -> f a | Sidekick_sat.Lit a -> f a
| Msat.Assign _ -> assert false) | Sidekick_sat.Assign _ -> assert false)
(* propagation from the bool solver *) (* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) = let check_ ~final (self:t) (acts: msat_acts) =
let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
let iter = iter_atoms_ acts in let iter = iter_atoms_ acts in
Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter)); Sidekick_sat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
self.on_progress(); self.on_progress();
assert_lits_ ~final self acts iter; assert_lits_ ~final self acts iter;
Profile.exit pb Profile.exit pb
(* propagation from the bool solver *) (* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit = let[@inline] partial_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
check_ ~final:false self acts check_ ~final:false self acts
(* perform final check of the model *) (* perform final check of the model *)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit = let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
check_ ~final:true self acts check_ ~final:true self acts
let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t = let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t =
@ -510,7 +508,7 @@ module Make(A : ARG)
module Lit = Solver_internal.Lit module Lit = Solver_internal.Lit
(** the parametrized SAT Solver *) (** the parametrized SAT Solver *)
module Sat_solver = Msat.Make_cdcl_t(Solver_internal) module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
module Atom = Sat_solver.Atom module Atom = Sat_solver.Atom
@ -528,7 +526,7 @@ module Make(A : ARG)
let pp_dot = let pp_dot =
let module Dot = let module Dot =
Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
let pp out self = Dot.pp out self.msat in let pp out self = Dot.pp out self.msat in
Some pp Some pp
@ -925,9 +923,9 @@ module Make(A : ARG)
let pr = us.get_proof () in let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr; if check then Sat_solver.Proof.check pr;
Some (Pre_proof.make pr (List.rev self.si.t_defs)) Some (Pre_proof.make pr (List.rev self.si.t_defs))
with Msat.Solver_intf.No_proof -> None with Sidekick_sat.Solver_intf.No_proof -> None
) in ) in
let unsat_core = lazy (us.Msat.unsat_assumptions ()) in let unsat_core = lazy (us.Sidekick_sat.unsat_assumptions ()) in
do_on_exit (); do_on_exit ();
Unsat {proof; unsat_core} Unsat {proof; unsat_core}

2
src/msat-solver/dune
View file

@ -2,5 +2,5 @@
(name Sidekick_msat_solver) (name Sidekick_msat_solver)
(public_name sidekick.msat-solver) (public_name sidekick.msat-solver)
(libraries containers iter sidekick.core sidekick.util (libraries containers iter sidekick.core sidekick.util
sidekick.cc sidekick.sat) sidekick.cc sidekick.sat sidekick.backend)
(flags :standard -open Sidekick_util)) (flags :standard -open Sidekick_util))

9
src/sat/Heap_intf.ml
View file

@ -1,8 +1,13 @@
module type RANKED = sig module type RANKED = sig
type t type t
val idx: t -> int (** Index in heap. return -1 if never set *)
val set_idx : t -> int -> unit (** Update index in heap *) val idx: t -> int
(** Index in heap. return -1 if never set *)
val set_idx : t -> int -> unit
(** Update index in heap *)
val cmp : t -> t -> bool val cmp : t -> t -> bool
end end

0
src/sat/Msat.ml → src/sat/Sidekick_sat.ml
View file

10
src/sat/dune
View file

@ -1,10 +1,10 @@
(library (library
(name msat) (name sidekick_sat)
(public_name msat) (public_name sidekick.sat)
(libraries iter) (libraries iter sidekick.util)
(synopsis "core data structures and algorithms for msat") (synopsis "Pure OCaml SAT solver implementation for sidekick")
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) (flags :standard -open Sidekick_util)
(ocamlopt_flags :standard -O3 -bin-annot (ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20) -unbox-closures -unbox-closures-factor 20)
) )

2
src/util/Backtrack_stack.ml
View file

@ -1,6 +1,4 @@
module Vec = Msat.Vec
type 'a t = { type 'a t = {
vec: 'a Vec.t; vec: 'a Vec.t;
lvls: int Vec.t; lvls: int Vec.t;

5
src/sat/Log.ml → src/util/Log.ml
View file

@ -1,8 +1,3 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** {1 Logging functions, real version} *) (** {1 Logging functions, real version} *)

14
src/sat/Log.mli → src/util/Log.mli
View file

@ -1,15 +1,13 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** {1 Logging function, for debugging} *) (** Logging function, for debugging *)
val enabled : bool val enabled : bool
val set_debug : int -> unit (** Set debug level *) val set_debug : int -> unit
val get_debug : unit -> int (** Current debug level *) (** Set debug level *)
val get_debug : unit -> int
(** Current debug level *)
val debugf : val debugf :
int -> int ->

5
src/util/Sidekick_util.ml
View file

@ -1,9 +1,10 @@
(* re-exports *) (* re-exports *)
module Fmt = CCFormat module Fmt = CCFormat
module Vec = Msat.Vec
module Log = Msat.Log
module Util = Util module Util = Util
module Vec = Vec
module Log = Log
module Backtrack_stack = Backtrack_stack module Backtrack_stack = Backtrack_stack
module Backtrackable_tbl = Backtrackable_tbl module Backtrackable_tbl = Backtrackable_tbl
module Error = Error module Error = Error

0
src/sat/Vec.ml → src/util/Vec.ml
View file

7
src/sat/Vec.mli → src/util/Vec.mli
View file

@ -1,4 +1,11 @@
(** Vectors
A resizable array, workhorse of imperative programming :-).
This implementation originated in alt-ergo-zero but has been basically rewritten
from scratch several times since.
*)
type 'a t type 'a t
(** Abstract type of vectors of 'a *) (** Abstract type of vectors of 'a *)