package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Satml.MakeSource

Parameters

module Th : Theory.S

Signature

Sourcetype th = Th.t
Sourcetype t
Sourceval solve : t -> unit
Sourceval set_new_proxies : t -> (Satml_types.Atom.atom * Satml_types.Atom.atom list * bool) Util.MI.t -> unit
Sourceval 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
Sourceval assume : t -> Satml_types.Atom.atom list list -> Satml_types.Atom.atom list list -> Expr.t -> cnumber:int -> Satml_types.Atom.atom option Satml_types.Flat_Formula.Map.t -> dec_lvl:int -> unit
Sourceval boolean_model : t -> Satml_types.Atom.atom list
Sourceval current_tbox : t -> th
Sourceval set_current_tbox : t -> th -> unit
Sourceval empty : unit -> t
Sourceval reset_steps : unit -> unit
Sourceval get_steps : unit -> int64
Sourceval assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
Sourceval decision_level : t -> int
Sourceval cancel_until : t -> int -> unit
Sourceval update_lazy_cnf : t -> do_bcp:bool -> Satml_types.Atom.atom option Satml_types.Flat_Formula.Map.t -> dec_lvl:int -> unit
Sourceval exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> bool
Sourceval known_lazy_formulas : t -> int Satml_types.Flat_Formula.Map.t
Sourceval assume_simple : t -> Satml_types.Atom.atom list list -> unit
Sourceval decide : t -> Satml_types.Atom.atom -> unit
Sourceval conflict_analyze_and_fix : t -> conflict_origin -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct