presburger-1.3.1: A decision procedure for quantifier-free linear arithmetic.

Data.Integer.SAT

Contents

Description

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

Synopsis

# Documentation

data PropSet Source

A collection of propositions.

Instances

 Show PropSet

An empty collection of propositions.

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

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 (?).

Add a new proposition to an existing collection.

data Prop Source

The type of proposition.

Constructors

 PTrue PFalse Prop :|| Prop infixr 2 Prop :&& Prop infixr 3 Not Prop Expr :== Expr infix 4 Expr :/= Expr infix 4 Expr :< Expr infix 4 Expr :> Expr infix 4 Expr :<= Expr infix 4 Expr :>= Expr infix 4

Instances

 Read Prop Show Prop

data Expr Source

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

Constructors

 Expr :+ Expr infixl 6 Addition Expr :- Expr infixl 6 Subtraction Integer :* Expr infixl 7 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 Source

Constructors

 Lower Upper

Instances

 Show BoundType

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

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

data Name Source

Instances

 Eq Name Ord Name Read Name Show Name

# Iterators

allSolutions :: PropSet -> [Solutions] Source

slnCurrent :: Solutions -> [(Int, Integer)] Source

slnNextVal :: Solutions -> Maybe Solutions Source

slnNextVar :: Solutions -> Maybe Solutions Source

slnEnumerate :: Solutions -> [Solutions] Source

# Debug

allInerts :: PropSet -> [Inerts] Source

ppInerts :: Inerts -> Doc Source

# For QuickCheck

data Bound Source

Constructors

 Bound Integer Term The integer is strictly positive

Instances

 Show Bound

tConst :: Integer -> Term Source

A constant term.