Module Satml.Make

Parameters

module Th : Theory.S

Signature

type th = Th.t
type t
val solve : t -> unit
val compute_concrete_model : declared_ids:Id.typed list -> t -> Models.t Stdlib.Lazy.t * Objective.Model.t
val assume : t -> (Satml_types.Atom.atom list * Expr.Labeled.Set.t) list -> (Satml_types.Atom.atom list * Expr.Labeled.Set.t) list -> Satml_types.Flat_Formula.Set.t -> dec_lvl:int -> unit
val boolean_model : t -> Satml_types.Atom.atom list
val instantiation_context : t -> Satml_types.Atom.Set.t
val current_tbox : t -> th
val set_current_tbox : t -> th -> unit
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
val decision_level : t -> int
val assertion_level : t -> int

Returns the number of active assertion levels, that is the number of levels introduced with push that have not yet been popped.

val cancel_until : t -> int -> unit
val exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> bool
val known_lazy_formulas : t -> int Satml_types.Flat_Formula.Map.t
val reason_of_deduction : Satml_types.Atom.atom -> Satml_types.Atom.Set.t
val conflict_analyze_and_fix : t -> Satml_intf.conflict_origin -> unit
val push : t -> Expr.t

push env adds a new assertion level and returns a guard g that must be used to guard all formulas asserted at this level.

val pop : t -> unit

pop env pops the latest assertion level.

val optimize : t -> Objective.Function.t -> unit

optimize env fn adds the objection fn to the environment env.

  • raises invalid_argurment

    if the decision level of env is not zero.