Up  

Module type Solver_types.S

module type S = Solver_types_intf.S
Interface for the internal types.

The signatures of clauses used in the Solver.
val mcsat : bool
TODO:deprecate.

Type definitions


type term 
type formula 
type proof
The types of terms, formulas and proofs. All of these are user-provided.
type lit = {
   lid : int; (*
Unique identifier
*)
   term : term; (*
Wrapped term
*)
   mutable l_level : int; (*
Decision level of the assignment
*)
   mutable l_weight : float; (*
Weight (for the heap)
*)
   mutable assigned : term option; (*
Assignment
*)
}
Wrapper type for literals, i.e. theory terms (for mcsat only).
type var = {
   vid : int; (*
Unique identifier
*)
   pa : atom; (*
Link for the positive atom
*)
   na : atom; (*
Link for the negative atom
*)
   mutable used : int; (*
Number of attached clause that contain the var
*)
   mutable seen : bool; (*
Boolean used during propagation
*)
   mutable v_level : int; (*
Level of decision/propagation
*)
   mutable v_weight : float; (*
Variable weight (for the heap)
*)
   mutable v_assignable : lit list option; (*
In mcsat, the list of lits that wraps subterms of the formula wrapped.
*)
   mutable reason : reason option; (*
The reason for propagation/decision of the literal
*)
} 
type atom = {
   aid : int; (*
Unique identifier
*)
   var : var; (*
Link for the parent variable
*)
   neg : atom; (*
Link for the negation of the atom
*)
   lit : formula; (*
Wrapped formula
*)
   mutable is_true : bool; (*
Is the atom true ? Conversely, the atom is false iff a.neg.is_true
*)
   mutable watched : clause Vec.t; (*
The vector of clauses that watch this atom
*)
}
Atoms and variables wrap theory formulas. They exist in the form of triplet: a variable and two atoms. For a formula f in normal form, the variable v points to the positive atom a which wraps f, while a.neg wraps the theory negation of f.
type clause = {
   name : string; (*
Clause name, mainly for printing, unique.
*)
   tag : int option; (*
User-provided tag for clauses.
*)
   atoms : atom array; (*
The atoms that constitute the clause.
*)
   mutable cpremise : premise; (*
The premise of the clause, i.e. the justification of why the clause must be satisfied.
*)
   mutable activity : float; (*
Clause activity, used for the heap heuristics.
*)
   mutable attached : bool; (*
Is the clause attached, i.e. does it watch literals.
*)
   mutable visited : bool; (*
Boolean used during propagation and proof generation.
*)
}
The type of clauses. Each clause generated should be true, i.e. enforced by the current problem (for more information, see the cpremise field).
type reason =
| Decision (*
The atom has been decided by the sat solver
*)
| Bcp of clause (*
The atom has been propagated by the given clause
*)
| Semantic (*
The atom has been propagated by the theory at the given level.
*)
Reasons of propagation/decision of atoms.
type premise =
| Hyp (*
The clause is a hypothesis, provided by the user.
*)
| Local (*
The clause is a 1-atom clause, where the atom is a local assumption
*)
| Lemma of proof (*
The clause is a theory-provided tautology, with the given proof.
*)
| History of clause list (*
The clause can be obtained by resolution of the clauses in the list. For a premise History [a_1 :: ... :: a_n] the clause is obtained by performing resolution of a_1 with a_2, and then performing a resolution step between the result and a_3, etc... Of course, each of the clause a_i also has its own premise.
*)
Premises for clauses. Indeed each clause generated during a run of the solver should be satisfied, the premise is the justification of why it should be satisfied by the solver.
type t =
| Lit of lit
| Atom of atom (*
Either a lit of an atom
*)

Decisions and propagations


val of_lit : lit -> t
val of_atom : atom -> t
Constructors and destructors

Elements


type elt =
| E_lit of lit
| E_var of var (*
Either a lit of a var
*) 
val nb_elt : unit -> int
val get_elt : int -> elt
val iter_elt : (elt -> unit) -> unit
Read access to the vector of variables created
val elt_of_lit : lit -> elt
val elt_of_var : var -> elt
Constructors & destructor for elements
val get_elt_id : elt -> int
val get_elt_level : elt -> int
val get_elt_weight : elt -> float
val set_elt_level : elt -> int -> unit
val set_elt_weight : elt -> float -> unit
Accessors for elements

Variables, Litterals & Clauses 


val dummy_var : var
val dummy_atom : atom
val dummy_clause : clause
Dummy values for use in vector dummys
val add_term : term -> lit
Returns the variable associated with the term
val add_atom : formula -> atom
Returns the atom associated with the given formula
val make_boolean_var : formula -> var * Formula_intf.negated
Returns the variable linked with the given formula, and whether the atom associated with the formula is var.pa or var.na
val empty_clause : clause
The empty clause
val make_clause : ?tag:int ->
       string ->
       atom list ->
       premise -> clause
make_clause name atoms size premise creates a clause with the given attributes.

Clause names


val fresh_name : unit -> string
val fresh_lname : unit -> string
val fresh_tname : unit -> string
val fresh_hname : unit -> string
Fresh names for clauses

Printing


val print_lit : Format.formatter -> lit -> unit
val print_atom : Format.formatter -> atom -> unit
val print_clause : Format.formatter -> clause -> unit
Pretty printing functions for atoms and clauses
val pp : Format.formatter -> t -> unit
val pp_lit : Format.formatter -> lit -> unit
val pp_atom : Format.formatter -> atom -> unit
val pp_clause : Format.formatter -> clause -> unit
val pp_dimacs : Format.formatter -> clause -> unit
val pp_reason : Format.formatter -> int * reason option -> unit
Debug function for atoms and clauses (very verbose)