Module La
module La: sig end
Linear arithmetic decision procedure
Author(s): Harald Ruess, N. Shankar
This module provides the building blocks for a decision procedure
for real and integer linear arithmetic based on the Simplex algorithm.
module S: sig end
States
s consist of two solution sets
(r, t) with
r the
regular solution set with equalities of the
form
x = a with
x a nonslack variable (see
Term.Var.is_slack)
and
a a linear arithmetic term.,
t a
tableau with equalities
k = b with
k a slack variable,
and all variables in the linear arithmetic term
b are slack variables, too.
A state
s represents the conjunction of equalities in
r and
t.
type tag =
val pp : tag -> S.t Pretty.printer
Print a partitioned version of s.
| Parameters: |
|
tag |
: |
tag
|
|
fmt |
: |
Format.formatter
|
|
s |
: |
S.t
|
|
val can : Partition.t * S.t -> Jst.Eqtrans.t
replace s a substitutes dependent variables
x
in
a with their right hand side
b if
x = b in
s.
The result is canonized using
Arith.map.
val nl_merge : (Fact.Equal.t -> unit) Pervasives.ref
module Infsys: sig end
Inference system for linear arithmetic.
exception Unbounded
Indicates unboundedness of a term in a state.
val upper : Partition.t * S.t -> Jst.Eqtrans.t
upper s a returns either
(b, rho) such that b+ is empty and rho |- a = b, or- raises
Unbounded if a is unbounded in s.
val lower : Partition.t * S.t -> Jst.Eqtrans.t
val is_equal : Partition.t * S.t -> Jst.Pred2.t
val model : S.t -> Term.t list -> Term.t Term.Map.t
model (p, s) xs returns an assignment rho
for the variables in xs with bindings x |-> q.
q is either a rational number or a rational
number added to the multiple of a "small" constant eps.
The assignment rho can be extended to a model of s.