type th = Th.tval solve : t -> unitval compute_concrete_model :
declared_ids:Id.typed list ->
t ->
Models.t Lazy.t * Objective.Model.tval set_new_proxies : t -> Satml_types.Flat_Formula.proxies -> unitval 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 listval assume :
t ->
Satml_types.Atom.atom list list ->
Satml_types.Atom.atom list list ->
Expr.t ->
cnumber:int ->
Satml_types.Flat_Formula.Set.t ->
dec_lvl:int ->
unitval boolean_model : t -> Satml_types.Atom.atom listval instantiation_context :
t ->
Satml_types.Flat_Formula.hcons_env ->
Satml_types.Atom.Set.tval create : Satml_types.Atom.hcons_env -> tval assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unitval decision_level : t -> intval cancel_until : t -> int -> unitval exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> boolval known_lazy_formulas : t -> int Satml_types.Flat_Formula.Map.tval reason_of_deduction : Satml_types.Atom.atom -> Satml_types.Atom.Set.tval assume_simple : t -> Satml_types.Atom.atom list list -> unitval do_case_split : t -> Util.case_split_policy -> conflict_originval decide : t -> Satml_types.Atom.atom -> unitval conflict_analyze_and_fix : t -> conflict_origin -> unitval push : t -> Satml_types.Atom.atom -> unitval pop : t -> unitval optimize : t -> Objective.Function.t -> unitoptimize env fn adds the objection fn to the environment env.
invalid_argurment if the decision level of env is not zero.