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(sat): remove functor, split into modules

Browse source
This commit is contained in:
Simon Cruanes 2022-07-30 20:27:47 -04:00
parent b97582daa2
commit 085e37e063
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
15 changed files with 2967 additions and 3063 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

118
src/sat/CHANGELOG.md
View file

@ -1,118 +0,0 @@
# CHANGES
## 0.9.1
- add `on_conflit` callback
- fix termination issue when using `push_decision_lit` from plugin
## 0.9
- feat: allow the theory to ask for some literals to be decided on
- feat: allow to set the default polarity of variables at creation time
## 0.8.3
- support containers 3.0
## 0.8.2
- fix opam file
- fix: allow conflicts below decision level in `Make_cdcl_t`
## 0.8.1
- fixes in `Heap`
- package for `msat-bin`
- use `iter` instead of `sequence` in dune and opam files
- more docs
## 0.8
big refactoring, change of API with fewer functions, etc.
see `git log` for more details.
## 0.6.1
- add simple functor for DOT backend
- various bugfixes
## 0.6
### Feature
- An already instantiated sat solver in the Sat module
- A `full_slice` function for running possibly expensive satisfiability
tests (in SMT) when a propositional model has been found
- Forgetful propagations: propagations whose reason (i.e clause) is not watched
## 0.5.1
### Bug
- Removed some needless allocations
### Breaking
- Better interface for mcsat propagations
### Feature
- Allow level 0 semantic propagations
## 0.5
### Bug
- Grow heap when adding local hyps
- Avoid forgetting some one atom clauses
- Fixed a bug for propagations at level 0
- Late propagations need to be re-propagated
- Fixed conflict at level 0
- Avoid forgetting some theory conflict clauses
### Breaking
- Changed `if_sat` interface
## 0.4.1
### Bug
- fix bug in `add_clause`
## 0.4
- performance improvements
- many bugfixes
- more tests
### Breaking
- remove push/pop (source of many bugs)
- replaced by solve : assumptions:lit list -> unit -> result
### Features
- Accept late conflict clauses
- cleaner API, moving some types outside the client-required interface
## 0.3
### Features
- Proofs for atoms at level 0
- Compatibility with ocaml >= 4.00
- Released some restrictions on dummy sat theories
## 0.2
### Breaking
- Log argument has been removed from functors
- All the functors now take a dummy last argument to ensure the solver modules are unique
### Features
- push/pop operations
- access to decision level when evaluating literals

33
src/sat/Sidekick_sat.ml
View file

@ -1,35 +1,4 @@
(** Main API *)
open Sidekick_core
module Solver_intf = Solver_intf
module type S = Solver_intf.S
module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE
type sat_state = Solver_intf.sat_state
type reason = Solver_intf.reason =
| Consequence of (unit -> Lit.t list * Proof_step.id)
[@@unboxed]
module type ACTS = Solver_intf.ACTS
type acts = (module ACTS)
(** Print {!lbool} values *)
let pp_lbool out = function
| L_true -> Format.fprintf out "true"
| L_false -> Format.fprintf out "false"
| L_undefined -> Format.fprintf out "undefined"
exception No_proof = Solver_intf.No_proof
exception Resource_exhausted = Solver_intf.Resource_exhausted
include Sigs
module Solver = Solver
module Make_cdcl_t = Solver.Make_cdcl_t
module Pure_sat = Solver.Pure_sat

2565
src/sat/Solver.ml
View file

File diff suppressed because it is too large Load diff

5
src/sat/Solver.mli
View file

@ -1,5 +0,0 @@
module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Pure_sat : S with type theory = unit
module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : S with type theory = Th.t

342
src/sat/Solver_intf.ml
View file

@ -1,342 +0,0 @@
(** Interface for Solvers
This modules defines the safe external interface for solvers.
Solvers that implements this interface can be obtained using the [Make]
functor.
*)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
open Sidekick_core
type 'a printer = Format.formatter -> 'a -> unit
(** Solver in a "SATISFIABLE" state *)
module type SAT_STATE = sig
val eval : Lit.t -> bool
(** Returns the valuation of a lit in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
val eval_level : Lit.t -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the literal to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
val iter_trail : (Lit.t -> unit) -> unit
(** Iter through the lits in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
end
type sat_state = (module SAT_STATE)
(** The type of values returned when the solver reaches a SAT state. *)
(** Solver in an "UNSATISFIABLE" state *)
module type UNSAT_STATE = sig
type clause
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val unsat_assumptions : unit -> Lit.t Iter.t
(** Subset of assumptions responsible for "unsat" *)
val unsat_proof : unit -> Proof_term.step_id
end
type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *)
type same_sign = bool
(** This type is used during the normalisation of lits.
[true] means the literal stayed the same, [false] that its sign was flipped. *)
(** The type of reasons for propagations of a lit [f]. *)
type reason = Consequence of (unit -> Lit.t list * Proof_step.id) [@@unboxed]
(** [Consequence (l, p)] means that the lits in [l] imply the propagated
lit [f]. The proof should be a proof of the clause "[l] implies [f]".
invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
the current trail.
{b note} on lazyiness: the justification is suspended (using [unit -> …])
to avoid potentially costly computations that might never be used
if this literal is backtracked without participating in a conflict.
Therefore the function that produces [(l,p)] needs only be safe in
trails (partial models) that are conservative extensions of the current
trail.
If the theory isn't robust w.r.t. extensions of the trail (e.g. if
its internal state undergoes significant changes),
it can be easier to produce the explanation eagerly when
propagating, and then use [Consequence (fun () -> expl, proof)] with
the already produced [(expl,proof)] tuple.
*)
type lbool = L_true | L_false | L_undefined (** Valuation of an atom *)
(** Actions available to the Plugin
The plugin provides callbacks for the SAT solver to use. These callbacks
are provided with a [(module ACTS)] so they can modify the SAT solver
by adding new lemmas, raise conflicts, etc. *)
module type ACTS = sig
val proof : Proof_trace.t
val iter_assumptions : (Lit.t -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
val eval_lit : Lit.t -> lbool
(** Obtain current value of the given literal *)
val add_lit : ?default_pol:bool -> Lit.t -> unit
(** Map the given lit to an internal atom, which will be decided by the
SAT solver. *)
val add_clause : ?keep:bool -> Lit.t list -> Proof_step.id -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
- [C_use_allocator alloc] puts the clause in the given allocator.
*)
val raise_conflict : Lit.t list -> Proof_step.id -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
val propagate : Lit.t -> reason -> unit
(** Propagate a lit, i.e. the theory can evaluate the lit to be true
(see the definition of {!type:eval_res} *)
val add_decision_lit : Lit.t -> bool -> unit
(** Ask the SAT solver to decide on the given lit with given sign
before it can answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. This will be undone on backtracking. *)
end
type acts = (module ACTS)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
module type LIT = sig
(** lits *)
type t
(** The type of atomic lits over terms. *)
val equal : t -> t -> bool
(** Equality over lits. *)
val hash : t -> int
(** Hashing function for lits. Should be such that two lits equal according
to {!val:Expr_intf.S.equal} have the same hash. *)
val pp : t printer
(** Printing function used among other thing for debugging. *)
val neg : t -> t
(** Formula negation *)
val norm_sign : t -> t * same_sign
(** Returns a 'normalized' form of the lit, possibly same_sign
(in which case return [false]).
[norm] must be so that [a] and [neg a] normalise to the same lit,
but one returns [false] and the other [true]. *)
end
(** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig
type t
(** The plugin state itself *)
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 -> acts -> unit
(** Assume the lits in the slice, possibly using the [slice]
to push new lits to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> 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
exception Resource_exhausted
(** Can be raised in a progress handler *)
(** The external interface implemented by safe solvers, such as the one
created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
module type S = sig
(** literals *)
type clause
type theory
type solver
(** The main solver type. *)
type store
(** Stores atoms, clauses, etc. *)
module Clause : sig
type t = clause
val equal : t -> t -> bool
module Tbl : Hashtbl.S with type key = t
val pp : store -> t printer
(** Print the clause *)
val short_name : store -> t -> string
(** Short name for a clause. Unspecified *)
val n_atoms : store -> t -> int
val lits_iter : store -> t -> Lit.t Iter.t
(** Literals of a clause *)
val lits_a : store -> t -> Lit.t array
(** Atoms of a clause *)
val lits_l : store -> t -> Lit.t list
(** List of atoms of a clause *)
end
(** {2 Main Solver Type} *)
type t = solver
(** Main solver type, containing all state for solving. *)
val create :
?stat:Stat.t ->
?size:[ `Tiny | `Small | `Big ] ->
proof:Proof_trace.t ->
theory ->
t
(** Create new solver
@param theory the theory
@param the proof
@param size the initial size of internal data structures. The bigger,
the faster, but also the more RAM it uses. *)
val theory : t -> theory
(** Access the theory state *)
val store : t -> store
(** Store for the solver *)
val stat : t -> Stat.t
(** Statistics *)
val proof : t -> Proof_trace.t
(** Access the inner proof *)
val on_conflict : t -> (Clause.t, unit) Event.t
val on_decision : t -> (Lit.t, unit) Event.t
val on_learnt : t -> (Clause.t, unit) Event.t
val on_gc : t -> (Lit.t array, unit) Event.t
(** {2 Types} *)
(** Result type for the solver *)
type res =
| Sat of sat_state
(** Returned when the solver reaches SAT, with a model *)
| Unsat of clause unsat_state
(** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
has not yet been assigned a value. *)
(** {2 Base operations} *)
val assume : t -> Lit.t list list -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *)
val add_clause : t -> Lit.t list -> Proof_step.id -> unit
(** Lower level addition of clauses *)
val add_clause_a : t -> Lit.t array -> Proof_step.id -> unit
(** Lower level addition of clauses *)
val add_input_clause : t -> Lit.t list -> unit
(** Like {!add_clause} but with the justification of being an input clause *)
val add_input_clause_a : t -> Lit.t array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *)
(** {2 Solving} *)
val solve : ?on_progress:(unit -> unit) -> ?assumptions:Lit.t list -> t -> res
(** Try and solves the current set of clauses.
@param assumptions additional atomic assumptions to be temporarily added.
The assumptions are just used for this call to [solve], they are
not saved in the solver's state.
@param on_progress regularly called during solving.
Can raise {!Resource_exhausted}
to stop solving.
@raise Resource_exhausted if the on_progress handler raised it to stop
*)
(** {2 Evaluating and adding literals} *)
val add_lit : t -> ?default_pol:bool -> Lit.t -> unit
(** Ensure the SAT solver handles this particular literal, ie add
a boolean variable for it if it's not already there. *)
val set_default_pol : t -> Lit.t -> bool -> unit
(** Set default polarity for the given boolean variable.
Sign of the literal is ignored. *)
val true_at_level0 : t -> Lit.t -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *)
val eval_lit : t -> Lit.t -> lbool
(** Evaluate atom in current state *)
(** {2 Assumption stack} *)
val push_assumption : t -> Lit.t -> unit
(** Pushes an assumption onto the assumption stack. It will remain
there until it's pop'd by {!pop_assumptions}. *)
val pop_assumptions : t -> int -> unit
(** [pop_assumptions solver n] removes [n] assumptions from the stack.
It removes the assumptions that were the most
recently added via {!push_assumptions}. *)
(** Result returned by {!check_sat_propagations_only} *)
type propagation_result =
| PR_sat
| PR_conflict of { backtracked: int }
| PR_unsat of clause unsat_state
val check_sat_propagations_only :
?assumptions:Lit.t list -> t -> propagation_result
(** [check_sat_propagations_only solver] uses the added clauses
and local assumptions (using {!push_assumptions} and [assumptions])
to quickly assess whether the context is satisfiable.
It is not complete; calling {!solve} is required to get an accurate
result.
@returns either [Ok()] if propagation yielded no conflict, or [Error c]
if a conflict clause [c] was found. *)
end

63
src/sat/base_types_.ml Normal file
View file

@ -0,0 +1,63 @@
open Sidekick_core
open Sigs
(* a boolean variable (positive int) *)
module Var0 : sig
include Int_id.S
end = struct
include Int_id.Make ()
end
type var = Var0.t
(* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
module Atom0 : sig
include Int_id.S
val neg : t -> t
val sign : t -> bool
val of_var : var -> t
val var : t -> var
val pa : var -> t
val na : var -> t
module AVec : Vec_sig.S with type elt := t
module ATbl : CCHashtbl.S with type key = t
end = struct
include Int_id.Make ()
let[@inline] neg i = i lxor 1
let[@inline] sign i = i land 1 = 0
let[@inline] pa v = (v : var :> int) lsl 1
let of_var = pa
let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
let[@inline] na v = ((v : var :> int) lsl 1) lor 1
module AVec = Veci
module ATbl = CCHashtbl.Make (CCInt)
end
module Clause0 : sig
include Int_id.S
module Tbl : Hashtbl.S with type key = t
module CVec : Vec_sig.S with type elt := t
end = struct
include Int_id.Make ()
module Tbl = Util.Int_tbl
module CVec = Veci
end
module Step_vec = Proof_trace.Step_vec
type atom = Atom0.t
type clause = Clause0.t
type var_reason = Decision | Bcp of clause | Bcp_lazy of clause lazy_t
module AVec = Atom0.AVec
(** Vector of atoms *)
module ATbl = Atom0.ATbl
(** Hashtbl of atoms *)
module CVec = Clause0.CVec
(** Vector of clauses *)

2
src/sat/dune
View file

@ -2,6 +2,6 @@
(name sidekick_sat)
(public_name sidekick.sat)
(synopsis "Pure OCaml SAT solver implementation for sidekick")
(private_modules heap heap_intf)
(private_modules heap heap_intf base_types_)
(libraries iter sidekick.util sidekick.core)
(flags :standard -w +32 -open Sidekick_util))

0
src/sat/Heap.ml → src/sat/heap.ml
View file

0
src/sat/Heap.mli → src/sat/heap.mli
View file

0
src/sat/Heap_intf.ml → src/sat/heap_intf.ml
View file

153
src/sat/sigs.ml Normal file
View file

@ -0,0 +1,153 @@
(** Main types and signatures *)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
open Sidekick_core
(** Solver in a "SATISFIABLE" state *)
module type SAT_STATE = sig
val eval : Lit.t -> bool
(** Returns the valuation of a lit in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
val eval_level : Lit.t -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the literal to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
val iter_trail : (Lit.t -> unit) -> unit
(** Iter through the lits in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
end
type sat_state = (module SAT_STATE)
(** The type of values returned when the solver reaches a SAT state. *)
(** Solver in an "UNSATISFIABLE" state *)
module type UNSAT_STATE = sig
type clause
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val unsat_assumptions : unit -> Lit.t Iter.t
(** Subset of assumptions responsible for "unsat" *)
val unsat_proof : unit -> Proof_term.step_id
end
type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *)
type same_sign = bool
(** This type is used during the normalisation of lits.
[true] means the literal stayed the same, [false] that its sign was flipped. *)
(** The type of reasons for propagations of a lit [f]. *)
type reason = Consequence of (unit -> Lit.t list * Proof_step.id) [@@unboxed]
(** [Consequence (l, p)] means that the lits in [l] imply the propagated
lit [f]. The proof should be a proof of the clause "[l] implies [f]".
invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
the current trail.
{b note} on lazyiness: the justification is suspended (using [unit -> …])
to avoid potentially costly computations that might never be used
if this literal is backtracked without participating in a conflict.
Therefore the function that produces [(l,p)] needs only be safe in
trails (partial models) that are conservative extensions of the current
trail.
If the theory isn't robust w.r.t. extensions of the trail (e.g. if
its internal state undergoes significant changes),
it can be easier to produce the explanation eagerly when
propagating, and then use [Consequence (fun () -> expl, proof)] with
the already produced [(expl,proof)] tuple.
*)
type lbool = L_true | L_false | L_undefined (** Valuation of an atom *)
let pp_lbool out = function
| L_true -> Fmt.string out "true"
| L_false -> Fmt.string out "false"
| L_undefined -> Fmt.string out "undefined"
(** Actions available to the Plugin.
The plugin provides callbacks for the SAT solver to use. These callbacks
are provided with a [(module ACTS)] so they can modify the SAT solver
by adding new lemmas, raise conflicts, etc. *)
module type ACTS = sig
val proof : Proof_trace.t
val iter_assumptions : (Lit.t -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
val eval_lit : Lit.t -> lbool
(** Obtain current value of the given literal *)
val add_lit : ?default_pol:bool -> Lit.t -> unit
(** Map the given lit to an internal atom, which will be decided by the
SAT solver. *)
val add_clause : ?keep:bool -> Lit.t list -> Proof_step.id -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
- [C_use_allocator alloc] puts the clause in the given allocator.
*)
val raise_conflict : Lit.t list -> Proof_step.id -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
val propagate : Lit.t -> reason -> unit
(** Propagate a lit, i.e. the theory can evaluate the lit to be true
(see the definition of {!type:eval_res} *)
val add_decision_lit : Lit.t -> bool -> unit
(** Ask the SAT solver to decide on the given lit with given sign
before it can answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. This will be undone on backtracking. *)
end
type acts = (module ACTS)
(** The type for a slice of assertions to assume/propagate in the theory. *)
(** Signature for theories to be given to the CDCL(T) solver *)
module type THEORY_CDCL_T = sig
val push_level : unit -> unit
(** Create a new backtrack level *)
val pop_levels : int -> unit
(** Pop [n] levels of the theory *)
val partial_check : acts -> unit
(** Assume the lits in the slice, possibly using the [slice]
to push new lits to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : 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
module type PLUGIN = sig
include THEORY_CDCL_T
val has_theory : bool
(** [true] iff the solver is parametrized by a theory, not just
pure SAT. *)
end
type plugin = (module PLUGIN)

2036
src/sat/solver.ml Normal file
View file

File diff suppressed because it is too large Load diff

176
src/sat/solver.mli Normal file
View file

@ -0,0 +1,176 @@
(** The external interface implemented by SAT solvers. *)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
open Sidekick_core
open Sigs
type clause
type plugin = Sigs.plugin
type solver
(** The main solver type. *)
type store
(** Stores atoms, clauses, etc. *)
module Clause : sig
type t = clause
val equal : t -> t -> bool
module Tbl : Hashtbl.S with type key = t
val pp : store -> t Fmt.printer
(** Print the clause *)
val short_name : store -> t -> string
(** Short name for a clause. Unspecified *)
val n_atoms : store -> t -> int
val lits_iter : store -> t -> Lit.t Iter.t
(** Literals of a clause *)
val lits_a : store -> t -> Lit.t array
(** Atoms of a clause *)
val lits_l : store -> t -> Lit.t list
(** List of atoms of a clause *)
end
(** {2 Main Solver Type} *)
type t = solver
(** Main solver type, containing all state for solving. *)
val store : t -> store
(** Store for the solver *)
val stat : t -> Stat.t
(** Statistics *)
val proof : t -> Proof_trace.t
(** Access the inner proof *)
val on_conflict : t -> (Clause.t, unit) Event.t
val on_decision : t -> (Lit.t, unit) Event.t
val on_learnt : t -> (Clause.t, unit) Event.t
val on_gc : t -> (Lit.t array, unit) Event.t
(** {2 Types} *)
(** Result type for the solver *)
type res =
| Sat of sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of clause unsat_state
(** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
has not yet been assigned a value. *)
(** {2 Base operations} *)
val assume : t -> Lit.t list list -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *)
val add_clause : t -> Lit.t list -> Proof_step.id -> unit
(** Lower level addition of clauses *)
val add_clause_a : t -> Lit.t array -> Proof_step.id -> unit
(** Lower level addition of clauses *)
val add_input_clause : t -> Lit.t list -> unit
(** Like {!add_clause} but with the justification of being an input clause *)
val add_input_clause_a : t -> Lit.t array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *)
(** {2 Solving} *)
val solve : ?on_progress:(unit -> unit) -> ?assumptions:Lit.t list -> t -> res
(** Try and solves the current set of clauses.
@param assumptions additional atomic assumptions to be temporarily added.
The assumptions are just used for this call to [solve], they are
not saved in the solver's state.
@param on_progress regularly called during solving.
Can raise {!Resource_exhausted}
to stop solving.
@raise Resource_exhausted if the on_progress handler raised it to stop
*)
(** {2 Evaluating and adding literals} *)
val add_lit : t -> ?default_pol:bool -> Lit.t -> unit
(** Ensure the SAT solver handles this particular literal, ie add
a boolean variable for it if it's not already there. *)
val set_default_pol : t -> Lit.t -> bool -> unit
(** Set default polarity for the given boolean variable.
Sign of the literal is ignored. *)
val true_at_level0 : t -> Lit.t -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *)
val eval_lit : t -> Lit.t -> lbool
(** Evaluate atom in current state *)
(** {2 Assumption stack} *)
val push_assumption : t -> Lit.t -> unit
(** Pushes an assumption onto the assumption stack. It will remain
there until it's pop'd by {!pop_assumptions}. *)
val pop_assumptions : t -> int -> unit
(** [pop_assumptions solver n] removes [n] assumptions from the stack.
It removes the assumptions that were the most
recently added via {!push_assumptions}. *)
(** Result returned by {!check_sat_propagations_only} *)
type propagation_result =
| PR_sat
| PR_conflict of { backtracked: int }
| PR_unsat of clause unsat_state
val check_sat_propagations_only :
?assumptions:Lit.t list -> t -> propagation_result
(** [check_sat_propagations_only solver] uses the added clauses
and local assumptions (using {!push_assumptions} and [assumptions])
to quickly assess whether the context is satisfiable.
It is not complete; calling {!solve} is required to get an accurate
result.
@returns either [Ok()] if propagation yielded no conflict, or [Error c]
if a conflict clause [c] was found. *)
(** {2 Initialization} *)
val plugin_cdcl_t : (module THEORY_CDCL_T) -> (module PLUGIN)
val create :
?stat:Stat.t ->
?size:[ `Tiny | `Small | `Big ] ->
proof:Proof_trace.t ->
plugin ->
t
(** Create new solver
@param theory the theory
@param the proof
@param size the initial size of internal data structures. The bigger,
the faster, but also the more RAM it uses. *)
val plugin_pure_sat : plugin
val create_pure_sat :
?stat:Stat.t ->
?size:[ `Tiny | `Small | `Big ] ->
proof:Proof_trace.t ->
unit ->
t

408
src/sat/store.ml Normal file
View file

@ -0,0 +1,408 @@
open Sidekick_core
open Sigs
include Base_types_
module Lit_tbl = Hashtbl.Make (Lit)
type cstore = {
c_lits: atom array Vec.t; (* storage for clause content *)
c_activity: Vec_float.t;
c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *)
c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
c_attached: Bitvec.t;
c_marked: Bitvec.t;
c_removable: Bitvec.t;
c_dead: Bitvec.t;
}
type t = {
(* variables *)
v_of_lit: var Lit_tbl.t; (* lit -> var *)
v_level: int Vec.t; (* decision/assignment level, or -1 *)
v_heap_idx: int Vec.t; (* index in priority heap *)
v_weight: Vec_float.t; (* heuristic activity *)
v_reason: var_reason option Vec.t; (* reason for assignment *)
v_seen: Bitvec.t; (* generic temporary marker *)
v_default_polarity: Bitvec.t; (* default polarity in decisions *)
mutable v_count: int;
(* atoms *)
a_is_true: Bitvec.t;
a_seen: Bitvec.t;
a_form: Lit.t Vec.t;
(* TODO: store watches in clauses instead *)
a_watched: Clause0.CVec.t Vec.t;
a_proof_lvl0: Proof_step.id ATbl.t;
(* atom -> proof for it to be true at level 0 *)
stat_n_atoms: int Stat.counter;
(* clauses *)
c_store: cstore;
}
type store = t
let create ?(size = `Big) ~stat () : t =
let size_map =
match size with
| `Tiny -> 8
| `Small -> 16
| `Big -> 4096
in
let stat_n_atoms = Stat.mk_int stat "sat.n-atoms" in
{
v_of_lit = Lit_tbl.create size_map;
v_level = Vec.create ();
v_heap_idx = Vec.create ();
v_weight = Vec_float.create ();
v_reason = Vec.create ();
v_seen = Bitvec.create ();
v_default_polarity = Bitvec.create ();
v_count = 0;
a_is_true = Bitvec.create ();
a_form = Vec.create ();
a_watched = Vec.create ();
a_seen = Bitvec.create ();
a_proof_lvl0 = ATbl.create 16;
stat_n_atoms;
c_store =
{
c_lits = Vec.create ();
c_activity = Vec_float.create ();
c_recycle_idx = Veci.create ~cap:0 ();
c_proof = Step_vec.create ~cap:0 ();
c_dead = Bitvec.create ();
c_attached = Bitvec.create ();
c_removable = Bitvec.create ();
c_marked = Bitvec.create ();
};
}
(** iterate on variables *)
let iter_vars self f =
Vec.iteri self.v_level ~f:(fun i _ -> f (Var0.of_int_unsafe i))
module Var = struct
include Var0
let[@inline] level self v = Vec.get self.v_level (v : var :> int)
let[@inline] set_level self v l = Vec.set self.v_level (v : var :> int) l
let[@inline] reason self v = Vec.get self.v_reason (v : var :> int)
let[@inline] set_reason self v r = Vec.set self.v_reason (v : var :> int) r
let[@inline] weight self v = Vec_float.get self.v_weight (v : var :> int)
let[@inline] set_weight self v w =
Vec_float.set self.v_weight (v : var :> int) w
let[@inline] mark self v = Bitvec.set self.v_seen (v : var :> int) true
let[@inline] unmark self v = Bitvec.set self.v_seen (v : var :> int) false
let[@inline] marked self v = Bitvec.get self.v_seen (v : var :> int)
let[@inline] set_default_pol self v b =
Bitvec.set self.v_default_polarity (v : var :> int) b
let[@inline] default_pol self v =
Bitvec.get self.v_default_polarity (v : var :> int)
let[@inline] heap_idx self v = Vec.get self.v_heap_idx (v : var :> int)
let[@inline] set_heap_idx self v i =
Vec.set self.v_heap_idx (v : var :> int) i
end
module Atom = struct
include Atom0
let[@inline] lit self a = Vec.get self.a_form (a : atom :> int)
let lit = lit
let[@inline] mark self a = Bitvec.set self.a_seen (a : atom :> int) true
let[@inline] unmark self a = Bitvec.set self.a_seen (a : atom :> int) false
let[@inline] marked self a = Bitvec.get self.a_seen (a : atom :> int)
let[@inline] watched self a = Vec.get self.a_watched (a : atom :> int)
let[@inline] is_true self a = Bitvec.get self.a_is_true (a : atom :> int)
let[@inline] set_is_true self a b =
Bitvec.set self.a_is_true (a : atom :> int) b
let[@inline] is_false self a = is_true self (neg a)
let[@inline] has_value self a = is_true self a || is_false self a
let[@inline] reason self a = Var.reason self (var a)
let[@inline] level self a = Var.level self (var a)
let[@inline] marked_both self a = marked self a && marked self (neg a)
let proof_lvl0 self a = ATbl.get self.a_proof_lvl0 a
let set_proof_lvl0 self a p = ATbl.replace self.a_proof_lvl0 a p
let pp self fmt a = Lit.pp fmt (lit self a)
let pp_a self fmt v =
if Array.length v = 0 then
Format.fprintf fmt "@<1>∅"
else (
pp self fmt v.(0);
if Array.length v > 1 then
for i = 1 to Array.length v - 1 do
Format.fprintf fmt " @<1>∨ %a" (pp self) v.(i)
done
)
(* Complete debug printing *)
let[@inline] pp_sign a =
if sign a then
"+"
else
"-"
(* print level+reason of assignment *)
let debug_reason _self out = function
| n, _ when n < 0 -> Format.fprintf out "%%"
| n, None -> Format.fprintf out "%d" n
| n, Some Decision -> Format.fprintf out "@@%d" n
| n, Some (Bcp c) -> Format.fprintf out "->%d/%d" n (c :> int)
| n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/<lazy>" n
let pp_level self out a =
let v = var a in
debug_reason self out (Var.level self v, Var.reason self v)
let debug_value self out (a : atom) =
if is_true self a then
Format.fprintf out "T%a" (pp_level self) a
else if is_false self a then
Format.fprintf out "F%a" (pp_level self) a
else
()
let debug self out a =
Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]" (pp_sign a)
(var a : var :> int)
(debug_value self) a Lit.pp (lit self a)
let debug_a self out vec =
Array.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) vec
end
module Clause = struct
include Clause0
(* TODO: store watch lists inside clauses *)
let make_a (store : store) ~removable (atoms : atom array) proof_step : t =
let {
c_recycle_idx;
c_lits;
c_activity;
c_attached;
c_dead;
c_removable;
c_marked;
c_proof;
} =
store.c_store
in
(* allocate new ID *)
let cid =
if Veci.is_empty c_recycle_idx then
Vec.size c_lits
else
Veci.pop c_recycle_idx
in
(* allocate space *)
(let new_len = cid + 1 in
Vec.ensure_size c_lits ~elt:[||] new_len;
Vec_float.ensure_size c_activity new_len;
Step_vec.ensure_size c_proof new_len;
Bitvec.ensure_size c_attached new_len;
Bitvec.ensure_size c_dead new_len;
Bitvec.ensure_size c_removable new_len;
Bitvec.ensure_size c_marked new_len;
Bitvec.set c_removable cid removable);
Vec.set c_lits cid atoms;
Step_vec.set c_proof cid proof_step;
let c = of_int_unsafe cid in
c
let make_l store ~removable atoms proof_rule : t =
make_a store ~removable (Array.of_list atoms) proof_rule
let[@inline] n_atoms (store : store) (c : t) : int =
Array.length (Vec.get store.c_store.c_lits (c : t :> int))
let[@inline] iter (store : store) ~f c =
let { c_lits; _ } = store.c_store in
Array.iter f (Vec.get c_lits (c : t :> int))
exception Early_exit
let for_all store ~f c =
try
iter store c ~f:(fun x -> if not (f x) then raise_notrace Early_exit);
true
with Early_exit -> false
let fold (store : store) ~f acc c =
let { c_lits; _ } = store.c_store in
Array.fold_left f acc (Vec.get c_lits (c : t :> int))
let[@inline] marked store c = Bitvec.get store.c_store.c_marked (c : t :> int)
let[@inline] set_marked store c b =
Bitvec.set store.c_store.c_marked (c : t :> int) b
let[@inline] attached store c =
Bitvec.get store.c_store.c_attached (c : t :> int)
let[@inline] set_attached store c b =
Bitvec.set store.c_store.c_attached (c : t :> int) b
let[@inline] dead store c = Bitvec.get store.c_store.c_dead (c : t :> int)
let[@inline] set_dead store c b =
Bitvec.set store.c_store.c_dead (c : t :> int) b
let[@inline] removable store c =
Bitvec.get store.c_store.c_removable (c : t :> int)
let[@inline] proof_step store c =
Step_vec.get store.c_store.c_proof (c : t :> int)
let dealloc store c : unit =
assert (dead store c);
let {
c_lits;
c_recycle_idx;
c_activity;
c_proof = _;
c_dead;
c_removable;
c_attached;
c_marked;
} =
store.c_store
in
(* clear data *)
let cid = (c : t :> int) in
Bitvec.set c_attached cid false;
Bitvec.set c_dead cid false;
Bitvec.set c_removable cid false;
Bitvec.set c_marked cid false;
Vec.set c_lits cid [||];
Vec_float.set c_activity cid 0.;
Veci.push c_recycle_idx cid;
(* recycle idx *)
()
let[@inline] activity store c =
Vec_float.get store.c_store.c_activity (c : t :> int)
let[@inline] set_activity store c f =
Vec_float.set store.c_store.c_activity (c : t :> int) f
let[@inline] atoms_a store c : atom array =
Vec.get store.c_store.c_lits (c : t :> int)
let lits_l store c : Lit.t list =
let arr = atoms_a store c in
Util.array_to_list_map (Atom.lit store) arr
let lits_a store c : Lit.t array =
let arr = atoms_a store c in
Array.map (Atom.lit store) arr
let lits_iter store c : Lit.t Iter.t =
let arr = atoms_a store c in
Iter.of_array arr |> Iter.map (Atom.lit store)
let short_name _store c = Printf.sprintf "cl[%d]" (c : t :> int)
let pp store fmt c =
Format.fprintf fmt "(cl[%d] : %a"
(c : t :> int)
(Atom.pp_a store) (atoms_a store c)
let debug store out c =
let atoms = atoms_a store c in
Format.fprintf out "(@[cl[%d]@ {@[<hov>%a@]}@])"
(c : t :> int)
(Atom.debug_a store) atoms
end
(* allocate new variable *)
let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var =
let {
v_count;
v_of_lit;
v_level;
v_heap_idx;
v_weight;
v_reason;
v_seen;
v_default_polarity;
stat_n_atoms;
a_is_true;
a_seen;
a_watched;
a_form;
c_store = _;
a_proof_lvl0 = _;
} =
self
in
let v_idx = v_count in
let v = Var.of_int_unsafe v_idx in
Stat.incr stat_n_atoms;
self.v_count <- 1 + v_idx;
Lit_tbl.add v_of_lit form v;
Vec.push v_level (-1);
Vec.push v_heap_idx (-1);
Vec.push v_reason None;
Vec_float.push v_weight 0.;
Bitvec.ensure_size v_seen v_idx;
Bitvec.ensure_size v_default_polarity v_idx;
Bitvec.set v_default_polarity v_idx pol;
assert (Vec.size a_form = 2 * (v : var :> int));
Bitvec.ensure_size a_is_true (2 * (v : var :> int));
Bitvec.ensure_size a_seen (2 * (v : var :> int));
Vec.push a_form form;
Vec.push a_watched (CVec.create ~cap:0 ());
Vec.push a_form (Lit.neg form);
Vec.push a_watched (CVec.create ~cap:0 ());
assert (Vec.get a_form (Atom.of_var v : atom :> int) == form);
v
(* create new variable *)
let alloc_var (self : t) ?default_pol (lit : Lit.t) : var * same_sign =
let lit, same_sign = Lit.norm_sign lit in
try Lit_tbl.find self.v_of_lit lit, same_sign
with Not_found ->
let v = alloc_var_uncached_ ?default_pol self lit in
v, same_sign
let clear_var (self : t) (v : var) : unit =
Var.unmark self v;
Atom.unmark self (Atom.pa v);
Atom.unmark self (Atom.na v);
()
let atom_of_var_ v same_sign : atom =
if same_sign then
Atom.pa v
else
Atom.na v
let alloc_atom (self : t) ?default_pol lit : atom =
let var, same_sign = alloc_var self ?default_pol lit in
atom_of_var_ var same_sign
let find_atom (self : t) lit : atom option =
let lit, same_sign = Lit.norm_sign lit in
match Lit_tbl.find self.v_of_lit lit with
| v -> Some (atom_of_var_ v same_sign)
| exception Not_found -> None

129
src/sat/store.mli Normal file
View file

@ -0,0 +1,129 @@
open Sidekick_core
open Sigs
type var = Base_types_.var
type atom = Base_types_.atom
type clause = Base_types_.clause
module CVec = Base_types_.CVec
type var_reason = Base_types_.var_reason =
| Decision
| Bcp of clause
| Bcp_lazy of clause lazy_t
type t
type store = t
val create : ?size:[< `Big | `Small | `Tiny > `Big ] -> stat:Stat.t -> unit -> t
val iter_vars : t -> (var -> unit) -> unit
module Var : sig
type t = var
val equal : t -> t -> same_sign
val compare : t -> t -> int
val hash : t -> int
val to_int : t -> int
val of_int_unsafe : int -> t
val level : store -> var -> int
val set_level : store -> var -> int -> unit
val reason : store -> var -> var_reason option
val set_reason : store -> var -> var_reason option -> unit
val weight : store -> var -> float
val set_weight : store -> var -> float -> unit
val mark : store -> var -> unit
val unmark : store -> var -> unit
val marked : store -> var -> same_sign
val set_default_pol : store -> var -> same_sign -> unit
val default_pol : store -> var -> same_sign
val heap_idx : store -> var -> int
val set_heap_idx : store -> var -> int -> unit
end
module Atom : sig
type t = atom
val equal : t -> t -> same_sign
val compare : t -> t -> int
val hash : t -> int
val to_int : t -> int
val of_int_unsafe : int -> t
val neg : t -> t
val sign : t -> same_sign
val of_var : var -> t
val var : t -> var
val pa : var -> t
val na : var -> t
module AVec = Sidekick_sat__Base_types_.Atom0.AVec
module ATbl = Sidekick_sat__Base_types_.Atom0.ATbl
val lit : store -> atom -> Lit.t
val mark : store -> atom -> unit
val unmark : store -> atom -> unit
val marked : store -> atom -> same_sign
val watched : store -> atom -> CVec.t
val is_true : store -> atom -> same_sign
val set_is_true : store -> atom -> same_sign -> unit
val is_false : store -> t -> same_sign
val has_value : store -> atom -> same_sign
val reason : store -> t -> var_reason option
val level : store -> t -> int
val marked_both : store -> atom -> same_sign
val proof_lvl0 : store -> ATbl.key -> int32 option
val set_proof_lvl0 : store -> ATbl.key -> int32 -> unit
val pp : store -> Format.formatter -> atom -> unit
val pp_a : store -> Format.formatter -> atom array -> unit
val pp_sign : t -> string
val debug_reason : 'a -> Format.formatter -> int * var_reason option -> unit
val pp_level : store -> Format.formatter -> t -> unit
val debug_value : store -> Format.formatter -> atom -> unit
val debug : store -> Format.formatter -> t -> unit
val debug_a : store -> Format.formatter -> t array -> unit
end
module Clause : sig
type t = clause
val equal : t -> t -> same_sign
val compare : t -> t -> int
val hash : t -> int
val to_int : t -> int
val of_int_unsafe : int -> t
module Tbl : Hashtbl.S with type key = t
module CVec = Base_types_.CVec
val make_a : store -> removable:same_sign -> atom array -> int32 -> t
val make_l : store -> removable:same_sign -> atom list -> int32 -> t
val n_atoms : store -> t -> int
val marked : store -> t -> same_sign
val set_marked : store -> t -> same_sign -> unit
val attached : store -> t -> same_sign
val set_attached : store -> t -> same_sign -> unit
val removable : store -> t -> same_sign
val dead : store -> t -> same_sign
val set_dead : store -> t -> same_sign -> unit
val dealloc : store -> t -> unit
val proof_step : store -> t -> int32
val activity : store -> t -> float
val set_activity : store -> t -> float -> unit
val iter : store -> f:(atom -> unit) -> t -> unit
val fold : store -> f:('a -> atom -> 'a) -> 'a -> t -> 'a
val for_all : store -> f:(atom -> same_sign) -> t -> same_sign
val atoms_a : store -> t -> atom array
val lits_l : store -> t -> Lit.t list
val lits_a : store -> t -> Lit.t array
val lits_iter : store -> t -> Lit.t Iter.t
val short_name : store -> t -> string
val pp : store -> Format.formatter -> t -> unit
val debug : store -> Format.formatter -> t -> unit
end
val alloc_var_uncached_ : ?default_pol:same_sign -> t -> Lit.t -> var
val alloc_var : t -> ?default_pol:same_sign -> Lit.t -> var * same_sign
val clear_var : t -> var -> unit
val atom_of_var_ : var -> same_sign -> atom
val alloc_atom : t -> ?default_pol:same_sign -> Lit.t -> atom
val find_atom : t -> Lit.t -> atom option