Safe Haskell	Trustworthy
Language	Haskell98

Data.Integer.SAT

Contents

Iterators
Debug
For QuickCheck

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 #

A collection of propositions.

Instances

Show PropSet #
Methods showsPrec :: Int -> PropSet -> ShowS # show :: PropSet -> String # showList :: [PropSet] -> ShowS #

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 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 #
Methods readsPrec :: Int -> ReadS Prop # readList :: ReadS [Prop] # readPrec :: ReadPrec Prop # readListPrec :: ReadPrec [Prop] #
Show Prop #
Methods showsPrec :: Int -> Prop -> ShowS # show :: Prop -> String # showList :: [Prop] -> ShowS #

data Expr #

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 #
Methods readsPrec :: Int -> ReadS Expr # readList :: ReadS [Expr] # readPrec :: ReadPrec Expr # readListPrec :: ReadPrec [Expr] #
Show Expr #
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #

data BoundType #

Constructors

Lower
Upper

Instances

Show BoundType #
Methods showsPrec :: Int -> BoundType -> ShowS # show :: BoundType -> String # showList :: [BoundType] -> ShowS #

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 #
Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name #
Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Read Name #
Methods readsPrec :: Int -> ReadS Name # readList :: ReadS [Name] # readPrec :: ReadPrec Name # readListPrec :: ReadPrec [Name] #
Show Name #
Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #