Module Sidekick_arith_lra__Simplex2.Make

Parameters

Signature

module V = Var
module V_map : CCMap.S with type V_map.key = V.t
type num = Q.t

Numbers

module Constraint : sig ... end
module Subst : sig ... end
type t
val create : ?⁠stat:Sidekick_util.Stat.t -> unit -> t

Create a new simplex.

val push_level : t -> unit
val pop_levels : t -> int -> unit
val define : t -> V.t -> (num * V.t) list -> unit

Define a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t

type unsat_cert
module Unsat_cert : sig ... end
exception E_unsat of Unsat_cert.t
type ev_on_propagate = V.lit -> reason:V.lit list -> unit
val add_var : t -> V.t -> unit

Make sure the variable exists in the simplex.

val add_constraint : on_propagate:ev_on_propagate -> t -> Constraint.t -> V.lit -> unit

Add a constraint to the simplex.

raises Unsat

if it's immediately obvious that this is not satisfiable.

val declare_bound : t -> Constraint.t -> V.lit -> unit

Declare that this constraint exists, so we can possibly propagate it. Unlike add_constraint this does NOT assert that the constraint is true

val check_exn : on_propagate:(V.lit -> reason:V.lit list -> unit) -> t -> unit

Check the whole simplex for satisfiability.

parameter on_propagate

is called with arguments lit, reason whenever reason => lit is found to be true by the simplex.

raises Unsat

if the constraints are not satisfiable.

type result =
| Sat of Subst.t
| Unsat of Unsat_cert.t
val check : on_propagate:(V.lit -> reason:V.lit list -> unit) -> t -> result

Call check_exn and return a model or a proof of unsat.