Module Internal.Make_pure_sat

Parameters

Signature

module Term : sig ... end
module Formula : sig ... end
module Value : sig ... end
type term = Term.t
type formula = Formula.t
type theory = unit
type lemma = Plugin.proof
type value = Value.t
type lit = {
lid : int;
term : term;
mutable l_level : int;
mutable l_idx : int;
mutable l_weight : float;
mutable assigned : value option;
}
type var = {
vid : int;
pa : atom;
na : atom;
mutable v_fields : int;
mutable v_level : int;
mutable v_idx : int;

position in heap

mutable v_weight : float;

Weight (for the heap), tracking activity

mutable v_assignable : lit list option;
mutable reason : reason option;
}
and atom = {
aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
watched : clause Msat.Vec.t;
}
and clause = {
cid : int;
atoms : atom array;
mutable cpremise : premise;
mutable activity : float;
mutable flags : int;
}
and reason =
| Decision
| Bcp of clause
| Bcp_lazy of clause lazy_t
| Semantic
and premise =
| Hyp of lemma
| Local
| Lemma of lemma
| History of clause list
| Empty_premise
type elt =
| E_lit of lit
| E_var of var
type trail_elt =
| Lit of lit
| Atom of atom
module MF : sig ... end
module MT : sig ... end
type st = {
t_map : lit MT.t;
f_map : var MF.t;
vars : elt Msat.Vec.t;
mutable cpt_mk_var : int;
mutable cpt_mk_clause : int;
}
val create_st : ?⁠size:[< `Big | `Small | `Tiny Big ] -> unit -> st
val nb_elt : st -> int
val get_elt : st -> int -> elt
val iter_elt : st -> (elt -> unit) -> unit
val name_of_clause : clause -> string
module Lit : sig ... end
val seen_var : int
val seen_pos : int
val seen_neg : int
module Var : sig ... end
module Atom : sig ... end
module Elt : sig ... end
module Trail_elt : sig ... end
module Clause : sig ... end
module Proof : sig ... end
type proof = Proof.t
module H : sig ... end
type unsat_cause =
| US_local of {
first : atom;
core : atom list;
}
| US_false of clause
exception E_sat
exception E_unsat of unsat_cause
exception UndecidedLit
exception Restart
exception Conflict of clause
val error : int
val warn : int
val info : int
val debug : int
val var_decay : float
val clause_decay : float
val restart_inc : float
val learntsize_inc : float
type t = {
st : st;
th : theory;
store_proof : bool;
clauses_hyps : clause Msat.Vec.t;
clauses_learnt : clause Msat.Vec.t;
clauses_to_add : clause Msat.Vec.t;
mutable unsat_at_0 : clause option;
mutable next_decision : atom option;
trail : trail_elt Msat.Vec.t;
elt_levels : int Msat.Vec.t;
mutable assumptions : atom Msat.Vec.t;
mutable th_head : int;
mutable elt_head : int;
order : H.t;
to_clear : var Msat.Vec.t;
mutable var_incr : float;
mutable clause_incr : float;
}
type solver = t
val restart_first : int
val learntsize_factor : float
val create_ : st:st -> store_proof:bool -> theory -> t
val create : ?⁠store_proof:bool -> ?⁠size:[< `Big | `Small | `Tiny Big ] -> theory -> t
val st : t -> st
val nb_clauses : t -> int
val decision_level : t -> int
val check_unsat_ : t -> unit
val iter_sub : (lit -> unit) -> var -> unit
val mk_atom_mcsat_ : t -> atom -> unit
val mk_atom : t -> formula -> atom
val insert_elt_order : t -> elt -> unit
val insert_var_order : t -> var -> unit
val insert_subterms_order : t -> var -> unit
val make_term : t -> term -> unit
val make_atom : t -> formula -> atom
val var_decay_activity : t -> unit
val clause_decay_activity : t -> unit
val var_bump_activity_aux : t -> var -> unit
val lit_bump_activity_aux : t -> lit -> unit
val var_bump_activity : t -> var -> unit
val clause_bump_activity : t -> clause -> unit
exception Trivial
val arr_to_list : 'a array -> int -> 'a list
val eliminate_duplicates : clause -> clause
val partition : atom array -> atom list * clause list
val new_decision_level : t -> unit
val attach_clause : clause -> unit
val cancel_until : t -> int -> unit
val pp_unsat_cause : Format.formatter -> unsat_cause -> unit
val report_unsat : t -> unsat_cause -> 'a
val simpl_reason : reason -> reason
val enqueue_bool : t -> atom -> level:int -> reason -> unit
val enqueue_semantic : t -> atom -> term list -> unit
val enqueue_assign : t -> lit -> value -> int -> unit
val swap_arr : 'a array -> int -> int -> unit
val put_high_level_atoms_first : atom array -> unit
val th_eval : t -> atom -> bool option
val backtrack_lvl : 'a -> atom array -> int * bool
type conflict_res = {
cr_backtrack_lvl : int;
cr_learnt : atom array;
cr_history : clause list;
cr_is_uip : bool;
}
val get_atom : t -> int -> atom
val analyze : t -> clause -> conflict_res
val record_learnt_clause : t -> clause -> conflict_res -> unit
val add_boolean_conflict : t -> clause -> unit
val add_clause_to_vec : t -> clause -> unit
val add_clause_ : t -> clause -> unit
val flush_clauses_ : t -> unit
val flush_clauses : t -> unit
type watch_res =
| Watch_kept
| Watch_removed
val propagate_in_clause : t -> atom -> clause -> int -> watch_res
val propagate_atom : t -> atom -> unit
val create_atom : t -> formula -> atom
exception Th_conflict of Clause.t
val slice_get : t -> int -> (term, formula, value) Msat.Solver_intf.assumption
val acts_add_clause : t -> ?⁠keep:bool -> formula list -> lemma -> unit
val acts_raise : t -> formula list -> lemma -> 'a
val check_consequence_lits_false_ : atom list -> unit
val acts_propagate : t -> formula -> (term, formula, lemma) Msat.Solver_intf.reason -> unit
val acts_iter : t -> full:bool -> int -> ((term, formula, value) Msat.Solver_intf.assumption -> unit) -> unit
val eval_atom_ : atom -> Msat.Solver_intf.lbool
val acts_eval_lit : t -> formula -> Msat.Solver_intf.lbool
val acts_mk_lit : t -> formula -> unit
val acts_mk_term : t -> term -> unit
val current_slice : t -> (term, formula, value, lemma) Msat.Solver_intf.acts
val full_slice : t -> (term, formula, value, lemma) Msat.Solver_intf.acts
val check_is_conflict_ : Clause.t -> unit
val theory_propagate : t -> clause option
val propagate : t -> clause option
val analyze_final : t -> atom -> atom list
val reduce_db : t -> int -> unit
val pick_branch_aux : t -> atom -> unit
val pick_branch_lit : t -> unit
val eval_level : t -> atom -> bool * int
val eval : t -> atom -> bool
val unsat_conflict : t -> clause option
val model : t -> (term * value) list
val solve_ : t -> unit
val assume : t -> formula list list -> lemma -> unit
val check_clause : clause -> bool
val check_vec : clause Msat.Vec.t -> bool
val check : t -> bool
val theory : t -> theory
val hyps : t -> clause Msat.Vec.t
val history : t -> clause Msat.Vec.t
val trail : t -> trail_elt Msat.Vec.t
type res =
| Sat of (term, Formula.t, value) Msat.Solver_intf.sat_state
| Unsat of (atom, clause, Proof.t) Msat.Solver_intf.unsat_state
val pp_all : t -> int -> string -> unit
val mk_sat : t -> (Term.t, Formula.t, value) Msat.Solver_intf.sat_state
val mk_unsat : t -> unsat_cause -> (atom, clause, clause) Msat.Solver_intf.unsat_state
val add_clause_a : t -> atom array -> lemma -> unit
val add_clause : t -> atom list -> lemma -> unit
val solve : ?⁠assumptions:atom list -> t -> res
val true_at_level0 : t -> atom -> bool
val eval_atom : 'a -> atom -> Msat.Solver_intf.lbool
val export : t -> clause Msat.Solver_intf.export