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 set_new_proxies : t -> Satml_types.Flat_Formula.proxies -> unit
val new_vars : t -> nbv:int -> Satml_types.Atom.var list -> Satml_types.Atom.atom list list -> Satml_types.Atom.atom list list -> Satml_types.Atom.atom list list * Satml_types.Atom.atom list list
val assume : t -> Satml_types.Atom.atom list list -> Satml_types.Atom.atom list list -> Expr.t -> cnumber:int -> AltErgoLib.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.Flat_Formula.hcons_env -> AltErgoLib.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 AltErgoLib.Satml_types.Flat_Formula.Map.t
val reason_of_deduction : Satml_types.Atom.atom -> AltErgoLib.Satml_types.Atom.Set.t
val do_case_split : t -> Util.case_split_policy -> conflict_origin
val conflict_analyze_and_fix : t -> 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.