Data.Integer.SAT

This module implements a decision procedure for quantifier-free linear arithmetic. The algorithm is based on the following paper:

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic by Sergey Berezin, Vijay Ganesh, and David L. Dill

Documentation

data PropSet

A collection of propositions.

Instances

Show PropSet

noProps :: PropSet

An empty collection of propositions.

checkSat :: PropSet -> Maybe [(Int, Integer)]

Extract a model from a consistent set of propositions. Returns Nothing if the assertions have no model. If a variable does not appear in the assignment, then it is 0 (?).

assert :: Prop -> PropSet -> PropSet

Add a new proposition to an existing collection.

data Prop

The type of proposition.

Constructors

PTrue

PFalse

Prop :|| Prop

Prop :&& Prop

Not Prop

Expr :== Expr

Expr :/= Expr

Expr :< Expr

Expr :> Expr

Expr :<= Expr

Expr :>= Expr

Instances

Read Prop

Show Prop

data Expr

The type of integer expressions. Variable names must be non-negative.

Constructors

Expr :+ Expr

Addition

Expr :- Expr

Subtraction

Integer :* Expr

Multiplication by a constant

Negate Expr

Negation

Var Name

Variable

K Integer

Constant

If Prop Expr Expr

A conditional expression

Div Expr Integer

Division, rounds down

Mod Expr Integer

Non-negative remainder

Instances

Read Expr

Show Expr

data BoundType

Constructors

Lower

Upper

Instances

Show BoundType

getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer

Computes bounds on the expression that are compatible with the model. Returns Nothing if the bound is not known.

getExprRange :: Expr -> PropSet -> Maybe [Integer]

Compute the range of possible values for an expression. Returns Nothing if the bound is not known.

data Name

Instances

Eq Name

Ord Name

Read Name

Show Name

toName :: Int -> Name

fromName :: Name -> Maybe Int