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 Source

A collection of propositions.

Instances

Show PropSet

noProps :: PropSet Source

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

assert :: Prop -> PropSet -> PropSet Source

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