Module Solver.Make_cdcl_t

Parameters

Signature

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

type lit = Th.lit

literals

module Lit = Th.Lit
type clause
type clause_pool_id

Pool of clauses, with its own lifetime management

type theory = Th.t
type proof = Th.proof

A representation of a full proof

type proof_step = Th.proof_step
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end
module Proof = Th.Proof

A module to manipulate proofs.

type t = solver

Main solver type, containing all state for solving.

val create : ?on_conflict:(t -> Clause.t -> unit) -> ?on_decision:(t -> lit -> unit) -> ?on_learnt:(t -> Clause.t -> unit) -> ?on_gc:(t -> lit array -> unit) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter 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 -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit Solver_intf.sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> lit 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 list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter 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.

val add_lit : t -> ?default_pol:bool -> lit -> 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 -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> 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 -> Solver_intf.lbool

Evaluate atom in current state