msat 0.9.1 (latest) · OCaml Package

Main API

module Solver_intf : sig ... end

Interface for Solvers

module type S = Solver_intf.S

module type FORMULA = Solver_intf.FORMULA

module type EXPR = Solver_intf.EXPR

module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T

module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT

module type PROOF = Solver_intf.PROOF

type void = (unit, bool) Solver_intf.gadt_eq

Empty type

type lbool = Solver_intf.lbool =

type ('term, 'form, 'value) sat_state =
  ('term, 'form, 'value) Solver_intf.sat_state =
  {

}

type ('atom, 'clause, 'proof) unsat_state =
  ('atom, 'clause, 'proof) Solver_intf.unsat_state =
  {

}

type 'clause export = 'clause Solver_intf.export = {

}

type ('term, 'formula, 'value) assumption =
  ('term, 'formula, 'value) Solver_intf.assumption =

type ('term, 'formula, 'proof) reason =
  ('term, 'formula, 'proof) Solver_intf.reason =

type ('term, 'formula, 'value, 'proof) acts =
  ('term, 'formula, 'value, 'proof) Solver_intf.acts =
  {

acts_iter_assumptions : (('term, 'formula, 'value) assumption -> unit) -> unit;
acts_eval_lit : 'formula -> lbool;
acts_mk_lit : ?default_pol:bool -> 'formula -> unit;
acts_mk_term : 'term -> unit;
acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
acts_raise_conflict : 'b. 'formula list -> 'proof -> 'b;
acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
acts_add_decision_lit : 'formula -> bool -> unit;

}

type negated = Solver_intf.negated =

val pp_negated : Format.formatter -> negated -> unit

Print negated values

val pp_lbool : Format.formatter -> lbool -> unit

Print lbool values

exception No_proof

module Make_mcsat (Th : Solver_intf.PLUGIN_MCSAT) : sig ... end

module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : sig ... end

module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : sig ... end

package msat