Index

.&&.	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
./=.	Data.ArithRel, Data.FOL.Arith
.<.	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
.<=.	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
.<=>.	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
.==.	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
.=>.	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
.>.	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
.>=.	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
.\|.	Algorithm.Cooper.Core, Algorithm.Cooper
.\|\|.	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
:*:	Data.FOL.Arith
:+:	Data.FOL.Arith
:/:	Data.FOL.Arith
AdaptiveSearch	SAT.PBO
addArtificialVariable	Algorithm.LPSolver
addAtLeast	SAT
addAtMost	SAT
addClause	SAT
addConstraint
1 (Function)	Algorithm.LPSolver
2 (Function)	SAT.Integer
addConstraint2	Algorithm.LPSolver
addConstraintSoft	SAT.Integer
addExactly	SAT
addFormula	SAT.TseitinEncoder
addPBAtLeast	SAT
addPBAtLeastSoft	SAT
addPBAtMost	SAT
addPBAtMostSoft	SAT
addPBExactly	SAT
addPBExactlySoft	SAT
allMCSAssumptions	SAT.CAMUS
allMUSAssumptions	SAT.CAMUS
And
1 (Data Constructor)	SAT.TseitinEncoder
2 (Data Constructor)	Algorithm.FOLModelFinder
3 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
And'	Algorithm.Cooper.Core, Algorithm.Cooper
andB	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
applySubst	Data.LA
applySubst1	Data.LA
approx
1 (Function)	Data.Polynomial.RootSeparation.Sturm
2 (Function)	Data.AlgebraicNumber.Real
approx'	Data.Polynomial.RootSeparation.Sturm
approxInterval	Data.AlgebraicNumber.Real
AReal	Data.AlgebraicNumber.Real
areCongruent	Algorithm.CongruenceClosure
ArminRestarts	SAT
asConst	Data.LA
assertAtom	Algorithm.Simplex2
assertAtomEx	Algorithm.Simplex2
assertLower	Algorithm.Simplex2
assertUpper	Algorithm.Simplex2
Atom
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Type/Class)	Algorithm.FOLModelFinder
3 (Type/Class)	Data.LA, Algorithm.Simplex2
4 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
5 (Type/Class)	Data.FOL.Arith
basis	Data.Polynomial.GroebnerBasis
basis'	Data.Polynomial.GroebnerBasis
basisOfBerlekampSubalgebra	Data.Polynomial.Factorization.FiniteField
berlekamp	Data.Polynomial.Factorization.FiniteField
BinarySearch	SAT.PBO
Block	Text.SDPFile
blockElem	Text.SDPFile
blockStruct	Text.SDPFile
Boolean	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
BoundExpr	Text.LPFile
Bounds	Text.LPFile
BoundsEnv	Data.LA, Algorithm.BoundsInference
BudgetExceeded
1 (Type/Class)	SAT
2 (Data Constructor)	SAT
cardinalityReduction	SAT.Types
ceiling'	Data.Delta
Cell	Algorithm.CAD
check	Algorithm.Simplex2
checkRealByCAD	Algorithm.OmegaTest.Misc
checkRealByFM	Algorithm.OmegaTest
checkRealBySimplex	Algorithm.OmegaTest.Misc
checkRealNoCheck	Algorithm.OmegaTest
Clause
1 (Type/Class)	SAT.Types, SAT
2 (Type/Class)	Algorithm.FOLModelFinder
clauses
1 (Function)	Text.GCNF
2 (Function)	Text.MaxSAT
clearArtificialVariables	Algorithm.LPSolver
clearLogger	Algorithm.Simplex2
cloneSolver	Algorithm.Simplex2
coeff
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
coeffMap
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
ColIndex	Algorithm.Simplex
collectNonnegVars	Algorithm.LPSolver
combineMaybe	Util
Complement	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
computeInterval	Data.LA, Algorithm.BoundsInference
Const	Data.FOL.Arith
constant
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
Constraint
1 (Type/Class)	Text.PBFile
2 (Type/Class)	Text.LPFile
3 (Data Constructor)	Text.LPFile
constraints	Text.LPFile
ConstraintType	Text.LPFile
constrBody	Text.LPFile
constrIndicator	Text.LPFile
constrLabel	Text.LPFile
constrType	Text.LPFile
cont	Data.Polynomial
ContinuousVariable	Text.LPFile
ContPP	Data.Polynomial
convert
1 (Function)	Converter.PB2LSP
2 (Function)	Converter.PB2WBO
3 (Function)	Converter.PB2SMP
4 (Function)	Converter.SAT2PB
5 (Function)	Converter.WBO2PB
6 (Function)	Converter.MaxSAT2WBO
7 (Function)	Converter.MaxSAT2NLPB
8 (Function)	Converter.LP2SMT
9 (Function)	Converter.PB2LP
10 (Function)	Converter.MaxSAT2LP
11 (Function)	Converter.SAT2LP
convertWBO	Converter.PB2LP
costs	Text.SDPFile
currentObjValue	Algorithm.Simplex
cutResolve	SAT.Types
defaultBounds	Text.LPFile
defaultCCMin	SAT
defaultLB	Text.LPFile
defaultLearningStrategy	SAT
defaultLearntSizeFirst	SAT
defaultLearntSizeInc	SAT
defaultOptions
1 (Function)	SAT.MUS
2 (Function)	SAT.CAMUS
3 (Function)	SAT.PBO.UnsatBased
4 (Function)	SAT.PBO.MSU4
5 (Function)	SAT.PBO
6 (Function)	Data.Polynomial.GroebnerBasis
7 (Function)	Converter.LP2SMT
8 (Function)	Algorithm.Simplex2
9 (Function)	Algorithm.OmegaTest
defaultPrintOptions	Data.Polynomial
defaultRandomFreq	SAT
defaultRestartFirst	SAT
defaultRestartInc	SAT
defaultRestartStrategy	SAT
defaultUB	Text.LPFile
define	Algorithm.LPSolver
deg	Data.Polynomial
Degree	Data.Polynomial
Delta
1 (Type/Class)	Data.Delta
2 (Data Constructor)	Data.Delta
delta	Data.Delta
deltaPart	Data.Delta
DenseBlock	Text.SDPFile
denseBlock	Text.SDPFile
DenseMatrix	Text.SDPFile
denseMatrix	Text.SDPFile
deriv	Data.Polynomial
diagBlock	Text.SDPFile
dir	Text.LPFile
div
1 (Function)	Data.Polynomial
2 (Function)	Data.Sign
divides	Data.Polynomial
Divisible	Algorithm.Cooper.Core, Algorithm.Cooper
divMod	Data.Polynomial
divModMP	Data.Polynomial
DNF
1 (Type/Class)	Data.DNF
2 (Data Constructor)	Data.DNF
dualSimplex
1 (Function)	Algorithm.Simplex
2 (Function)	Algorithm.LPSolver
3 (Function)	Algorithm.Simplex2
dump	Algorithm.Simplex2
eliminateQuantifiers
1 (Function)	Algorithm.FourierMotzkin.FOL, Algorithm.FourierMotzkin
2 (Function)	Algorithm.Cooper.FOL, Algorithm.Cooper
eliminateQuantifiers'	Algorithm.FourierMotzkin.FOL
emptySolver	Algorithm.LPSolver
emptyTheory	SAT.TheorySolver
encodeConj	SAT.TseitinEncoder
encodeDisj	SAT.TseitinEncoder
Encoder	SAT.TseitinEncoder
encSolver	SAT.TseitinEncoder
Entity	Algorithm.FOLModelFinder
enumMCSAssumptions	SAT.CAMUS
Eq	Text.PBFile
Eql
1 (Data Constructor)	Text.LPFile
2 (Data Constructor)	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
Equiv
1 (Data Constructor)	SAT.TseitinEncoder
2 (Data Constructor)	Algorithm.FOLModelFinder
3 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
eval
1 (Function)	Data.Polynomial
2 (Function)	SAT.Integer
evalAtom
1 (Function)	Data.LA
2 (Function)	Data.FOL.Arith
evalCell	Algorithm.CAD
evalExpr
1 (Function)	Data.LA
2 (Function)	Data.FOL.Arith
evalLinear	Data.LA
evalLit
1 (Function)	SAT.Types
2 (Function)	Algorithm.Cooper.Core
evalOp	Data.ArithRel, Data.FOL.Arith
evalPoint	Algorithm.CAD
evalQFFormula	Algorithm.Cooper.Core
exgcd	Data.Polynomial
Exists
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
expandDefs	Algorithm.LPSolver
expandDefs'	Algorithm.LPSolver
Expr
1 (Type/Class)	Text.LPFile
2 (Type/Class)	Data.LA
3 (Type/Class)	SAT.Integer
4 (Data Constructor)	SAT.Integer
5 (Type/Class)	Data.FOL.Arith
ExprZ
1 (Type/Class)	Algorithm.FourierMotzkin.Core
2 (Type/Class)	Algorithm.Cooper.Core, Algorithm.Cooper
extract	Data.LA
extractMaybe	Data.LA
F
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
F'	Algorithm.Cooper.Core, Algorithm.Cooper
Factor	Data.Polynomial
factor
1 (Function)	Data.Polynomial
2 (Function)	Data.Polynomial.Factorization.FiniteField
3 (Function)	Data.Polynomial.Factorization.Zassenhaus
4 (Function)	Data.Polynomial.Factorization.Kronecker
failedAssumptions	SAT
false	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
findModel	Algorithm.FOLModelFinder
findMUSAssumptions	SAT.MUS
findPoly	Data.AlgebraicNumber.Root
findSample	Algorithm.CAD
Finite	Text.LPFile
FlatTerm	Algorithm.CongruenceClosure
flipOp	Data.ArithRel, Data.FOL.Arith
floor'	Data.Delta
Forall
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
Formula
1 (Type/Class)	Text.PBFile
2 (Type/Class)	SAT.TseitinEncoder
3 (Type/Class)	Algorithm.FOLModelFinder
4 (Type/Class)	Data.FOL.Formula, Data.FOL.Arith
fracPart	Util
fromCoeffMap
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
fromFOLAtom	Data.LA.FOL
fromFOLExpr	Data.LA.FOL
fromLAAtom
1 (Function)	Algorithm.FourierMotzkin.Core
2 (Function)	Algorithm.Cooper.Core, Algorithm.Cooper
fromRat	Algorithm.FourierMotzkin.Core
fromReal	Data.Delta
fromTerm	Data.Polynomial
fromTerms
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
FSym	Algorithm.FOLModelFinder
FTApp	Algorithm.CongruenceClosure
FTConst	Algorithm.CongruenceClosure
gcd	Data.Polynomial
gcd'	Data.Polynomial
GClause	Text.GCNF
GCNF
1 (Type/Class)	Text.GCNF
2 (Data Constructor)	Text.GCNF
Ge
1 (Data Constructor)	Text.PBFile
2 (Data Constructor)	Text.LPFile
3 (Data Constructor)	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
GenericSolver	Algorithm.Simplex2
GenFormula	Algorithm.FOLModelFinder
GenLit	Algorithm.FOLModelFinder
gensym	Algorithm.LPSolver
getArtificialVariables	Algorithm.LPSolver
getBounds	Text.LPFile
getCoeff	Algorithm.Simplex2
getCol	Algorithm.Simplex2
getDefs	Algorithm.LPSolver
getLB	Algorithm.Simplex2
getModel	Algorithm.LPSolver
getObj	Algorithm.Simplex2
getObjValue
1 (Function)	Algorithm.Simplex2
2 (Function)	Algorithm.MIPSolver2
getOptDir	Algorithm.Simplex2
getRow	Algorithm.Simplex2
getTableau
1 (Function)	Algorithm.LPSolver
2 (Function)	Algorithm.Simplex2
getUB	Algorithm.Simplex2
getValue	Algorithm.Simplex2
getVarInfo	Text.LPFile
getVarType	Text.LPFile
goldenRatio	Data.AlgebraicNumber.Real
graeffesMethod	Data.Polynomial.RootSeparation.Graeffe
grevlex	Data.Polynomial
grlex	Data.Polynomial
GroupIndex	Text.GCNF
Gt	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
halve	Data.Polynomial.RootSeparation.Sturm
halve'	Data.Polynomial.RootSeparation.Sturm
height	Data.AlgebraicNumber.Real
hensel	Data.Polynomial.Factorization.Hensel
hittingSetDual	SAT.CAMUS
Imply
1 (Data Constructor)	SAT.TseitinEncoder
2 (Data Constructor)	Algorithm.FOLModelFinder
3 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
inferBounds	Algorithm.BoundsInference
IntegerVariable	Text.LPFile
integerVariables	Text.LPFile
integral	Data.Polynomial
interpolate	Data.Polynomial.Interpolation.Lagrange
Interval	Algorithm.CAD
isAlgebraicInteger	Data.AlgebraicNumber.Real
isBasicVariable	Algorithm.Simplex2
isFeasible	Algorithm.Simplex2
isInteger	Util
isInteger'	Data.Delta
isNegativeCoeff	Data.Polynomial
isNonBasicVariable	Algorithm.Simplex2
isOptimal	Algorithm.Simplex2
isPrimitive	Data.Polynomial
isRational	Data.AlgebraicNumber.Real
IsRel	Data.ArithRel, Data.FOL.Arith
isRootOf	Data.Polynomial
isSquareFree	Data.Polynomial
Label	Text.LPFile
Language	Converter.LP2SMT
lastGroupIndex	Text.GCNF
LazyConstraint	Text.LPFile
LBool	Data.LBool
lc	Data.Polynomial
lcm	Data.Polynomial
Le
1 (Data Constructor)	Text.LPFile
2 (Data Constructor)	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
LearningClause	SAT
LearningHybrid	SAT
LearningStrategy	SAT
lex	Data.Polynomial
lFalse	Data.LBool
lift1	Data.LA
lift2	Data.AlgebraicNumber.Root
liftBool	Data.LBool
linearize	SAT.Integer
LinearSearch	SAT.PBO
Lit
1 (Type/Class)	Text.PBFile
2 (Type/Class)	SAT.Types, SAT
3 (Type/Class)	Algorithm.FOLModelFinder
4 (Type/Class)	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
5 (Data Constructor)	Algorithm.Cooper.Core, Algorithm.Cooper
6 (Type/Class)	Algorithm.Cooper.Core, Algorithm.Cooper
literal	SAT.Types, SAT
LitMap	SAT.Types
litNot	SAT.Types, SAT
litPolarity	SAT.Types, SAT
LitSet	SAT.Types
litUndef	SAT.Types
litVar	SAT.Types, SAT
lm	Data.Polynomial
lnot	Data.LBool
lookupCoeff
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
lookupRow	Algorithm.Simplex
LP
1 (Type/Class)	Text.LPFile
2 (Data Constructor)	Text.LPFile
3 (Type/Class)	Algorithm.LPSolver
Lt	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
lt	Data.Polynomial
lTrue	Data.LBool
LubyRestarts	SAT
lUndef	Data.LBool
mapCoeff
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
mapCoeffWithVar	Data.LA
matrices	Text.SDPFile
Matrix	Text.SDPFile
maximize
1 (Function)	Algorithm.LPSolverHL
2 (Function)	Algorithm.MIPSolverHL
maxsatPrintModel	SAT.Printer
mcoprime	Data.Polynomial
MCS	SAT.CAMUS
mderiv	Data.Polynomial
mDim	Text.SDPFile
mdiv	Data.Polynomial
mdivides	Data.Polynomial
merge	Algorithm.CongruenceClosure
mfromIndices	Data.Polynomial
mfromIndicesMap	Data.Polynomial
mFunctions	Algorithm.FOLModelFinder
mgcd	Data.Polynomial
mindices	Data.Polynomial
mindicesMap	Data.Polynomial
minimalPolynomial	Data.AlgebraicNumber.Real
minimize
1 (Function)	SAT.PBO
2 (Function)	Algorithm.LPSolverHL
3 (Function)	Algorithm.MIPSolverHL
MiniSATRestarts	SAT
mintegral	Data.Polynomial
mlcm	Data.Polynomial
mmult	Data.Polynomial
mod	Data.Polynomial
Model
1 (Type/Class)	Text.GurobiSol
2 (Type/Class)	SAT.Types, SAT
3 (Type/Class)	Algorithm.FOLModelFinder
4 (Data Constructor)	Algorithm.FOLModelFinder
5 (Type/Class)	Data.Var, Algorithm.OmegaTest
6 (Type/Class)	Algorithm.Simplex2
7 (Type/Class)	Algorithm.CAD
model
1 (Function)	SAT
2 (Function)	Algorithm.Simplex2
3 (Function)	Algorithm.MIPSolver2
mone	Data.Polynomial
Monomial	Data.Polynomial
MonomialOrder	Data.Polynomial
mpow	Data.Polynomial
mRelations	Algorithm.FOLModelFinder
MSU4	SAT.PBO
mult	Data.Sign
mUniverse	Algorithm.FOLModelFinder
MUS	SAT.CAMUS
musPrintSol	SAT.Printer
narrow	Data.Polynomial.RootSeparation.Sturm
narrow'	Data.Polynomial.RootSeparation.Sturm
nAssigns	SAT
nBlock	Text.SDPFile
nClauses	SAT
Neg
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.Sign
negate	Data.Sign
negatePBAtLeast	SAT.Types
NegInf
1 (Data Constructor)	Text.LPFile
2 (Data Constructor)	Algorithm.CAD
negOp	Data.ArithRel, Data.FOL.Arith
NEq	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
newEncoder	SAT.TseitinEncoder
newSolver
1 (Function)	SAT
2 (Function)	Algorithm.CongruenceClosure
3 (Function)	Algorithm.Simplex2
4 (Function)	Algorithm.MIPSolver2
newVar
1 (Function)	SAT
2 (Function)	Algorithm.CongruenceClosure
3 (Function)	Algorithm.Simplex2
4 (Function)	SAT.Integer
newVars	SAT
newVars_	SAT
nLearnt	SAT
Nonneg	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
NormalConstraint	Text.LPFile
normalizeAtLeast	SAT.Types
normalizeClause	SAT.Types
normalizeConstraint	Algorithm.LPSolver
normalizePBAtLeast	SAT.Types
normalizePBExactly	SAT.Types
normalizePBSum	SAT.Types
normalizePoly	Data.AlgebraicNumber.Root
NormalStrategy	Data.Polynomial.GroebnerBasis
Not
1 (Data Constructor)	SAT.TseitinEncoder
2 (Data Constructor)	Algorithm.FOLModelFinder
3 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
notB	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
NthRoot
1 (Type/Class)	Data.Polynomial.RootSeparation.Graeffe
2 (Data Constructor)	Data.Polynomial.RootSeparation.Graeffe
nthRoot	Data.AlgebraicNumber.Real
numClauses
1 (Function)	Text.GCNF
2 (Function)	Text.MaxSAT
numRoots	Data.Polynomial.RootSeparation.Sturm
numRoots'	Data.Polynomial.RootSeparation.Sturm
numVars
1 (Function)	Text.GCNF
2 (Function)	Text.MaxSAT
nVars
1 (Function)	SAT
2 (Function)	Algorithm.Simplex2
ObjectiveFunction	Text.LPFile
objectiveFunction	Text.LPFile
ObjLimit	Algorithm.Simplex2
objLimit	Algorithm.Simplex2
ObjMaxOne	Converter.ObjType, Converter.PBSetObj
ObjMaxZero	Converter.ObjType, Converter.PBSetObj
ObjNone	Converter.ObjType, Converter.PBSetObj
objRow	Algorithm.Simplex
ObjType	Converter.ObjType, Converter.PBSetObj
Op	Text.PBFile
optCallback	SAT.CAMUS
optCheckReal	Algorithm.OmegaTest
optCheckSAT	Converter.LP2SMT
OptDir	Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL
optimize
1 (Function)	Algorithm.LPSolverHL
2 (Function)	Algorithm.Simplex2
3 (Function)	Algorithm.MIPSolver2
4 (Function)	Algorithm.MIPSolverHL
Optimum
1 (Data Constructor)	Algorithm.LPSolverHL, Algorithm.MIPSolverHL
2 (Data Constructor)	Algorithm.Simplex2
Options
1 (Type/Class)	SAT.MUS
2 (Data Constructor)	SAT.MUS
3 (Type/Class)	SAT.CAMUS
4 (Data Constructor)	SAT.CAMUS
5 (Type/Class)	SAT.PBO.UnsatBased
6 (Data Constructor)	SAT.PBO.UnsatBased
7 (Type/Class)	SAT.PBO.MSU4
8 (Data Constructor)	SAT.PBO.MSU4
9 (Type/Class)	SAT.PBO
10 (Data Constructor)	SAT.PBO
11 (Type/Class)	Data.Polynomial.GroebnerBasis
12 (Data Constructor)	Data.Polynomial.GroebnerBasis
13 (Type/Class)	Converter.LP2SMT
14 (Data Constructor)	Converter.LP2SMT
15 (Type/Class)	Algorithm.Simplex2
16 (Data Constructor)	Algorithm.Simplex2
17 (Type/Class)	Algorithm.OmegaTest
18 (Data Constructor)	Algorithm.OmegaTest
optLanguage	Converter.LP2SMT
optLitPrinter	SAT.MUS
optLogger
1 (Function)	SAT.MUS
2 (Function)	SAT.CAMUS
3 (Function)	SAT.PBO.UnsatBased
4 (Function)	SAT.PBO.MSU4
5 (Function)	SAT.PBO
OptMax	Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL
OptMin	Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL
optObjFunVarsHeuristics	SAT.PBO
optOptimize	Converter.LP2SMT
optProduceModel	Converter.LP2SMT
OptResult
1 (Type/Class)	Algorithm.LPSolverHL, Algorithm.MIPSolverHL
2 (Type/Class)	Algorithm.Simplex2
optSearchStrategy	SAT.PBO
optStrategy	Data.Polynomial.GroebnerBasis
optTrialLimitConf	SAT.PBO
OptUnsat	Algorithm.LPSolverHL, Algorithm.MIPSolverHL
optUpdateBest
1 (Function)	SAT.MUS
2 (Function)	SAT.PBO.UnsatBased
3 (Function)	SAT.PBO.MSU4
4 (Function)	SAT.PBO
optUpdateLB
1 (Function)	SAT.PBO.UnsatBased
2 (Function)	SAT.PBO.MSU4
3 (Function)	SAT.PBO
Or
1 (Data Constructor)	SAT.TseitinEncoder
2 (Data Constructor)	Algorithm.FOLModelFinder
3 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
Or'	Algorithm.Cooper.Core, Algorithm.Cooper
orB	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
packageVersions	Version
PApp	Algorithm.FOLModelFinder
parseDataFile	Text.SDPFile
parseDataString	Text.SDPFile
parseFile
1 (Function)	Text.GCNF
2 (Function)	Text.LPFile
3 (Function)	Text.MPSFile
parseOPBFile	Text.PBFile
parseOPBString	Text.PBFile
parseSparseDataFile	Text.SDPFile
parseSparseDataString	Text.SDPFile
parseString
1 (Function)	Text.GCNF
2 (Function)	Text.LPFile
3 (Function)	Text.MPSFile
parseWBOFile	Text.PBFile
parseWBOString	Text.PBFile
parseWCNFFile	Text.MaxSAT
parseWCNFString	Text.MaxSAT
pbEval	SAT.Types
pbLowerBound	SAT.Types
pbNumVars	Text.PBFile
pbPrintModel	SAT.Printer
pbUpperBound	SAT.Types
pdiv	Data.Polynomial
pdivMod	Data.Polynomial
phaseI
1 (Function)	Algorithm.Simplex
2 (Function)	Algorithm.LPSolver
pivot	Algorithm.Simplex
PivotResult	Algorithm.Simplex
PivotStrategy	Algorithm.Simplex2
PivotStrategyBlandRule	Algorithm.Simplex2
PivotStrategyLargestCoefficient	Algorithm.Simplex2
pmod	Data.Polynomial
Point
1 (Data Constructor)	Algorithm.CAD
2 (Type/Class)	Algorithm.CAD
Polynomial	Data.Polynomial
pOptIsNegativeCoeff	Data.Polynomial
pOptMonomialOrder	Data.Polynomial
pOptPrintCoeff	Data.Polynomial
pOptPrintVar	Data.Polynomial
Pos
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.Sign
3 (Data Constructor)	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
4 (Data Constructor)	Algorithm.Cooper.Core, Algorithm.Cooper
PosInf
1 (Data Constructor)	Text.LPFile
2 (Data Constructor)	Algorithm.CAD
pow	Data.Sign
pp	Data.Polynomial
pPrintCoeff	Data.Polynomial
pPrintVar	Data.Polynomial
PrettyCoeff	Data.Polynomial
prettyPrint	Data.Polynomial
PrettyVar	Data.Polynomial
PrintOptions
1 (Type/Class)	Data.Polynomial
2 (Data Constructor)	Data.Polynomial
Problem
1 (Type/Class)	Text.SDPFile
2 (Data Constructor)	Text.SDPFile
project
1 (Function)	Algorithm.CAD
2 (Function)	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
3 (Function)	Algorithm.Cooper.Core, Algorithm.Cooper
project'	Algorithm.FourierMotzkin.Core
projectCases	Algorithm.Cooper.Core, Algorithm.Cooper
projectCasesN	Algorithm.Cooper.Core, Algorithm.Cooper
projectN
1 (Function)	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
2 (Function)	Algorithm.Cooper.Core
projectN'	Algorithm.FourierMotzkin.Core
PSym	Algorithm.FOLModelFinder
pushNot	Data.FOL.Formula, Data.FOL.Arith
putTableau	Algorithm.LPSolver
QFFormula	Algorithm.Cooper.Core, Algorithm.Cooper
Rat	Algorithm.FourierMotzkin.Core
RawModel	Algorithm.Simplex2
rawModel	Algorithm.Simplex2
realPart	Data.Delta
realRoots	Data.AlgebraicNumber.Real
realRootsEx	Data.AlgebraicNumber.Real
recip	Data.Sign
reduce	Data.Polynomial
reduceGBasis	Data.Polynomial.GroebnerBasis
Rel
1 (Type/Class)	Data.ArithRel, Data.FOL.Arith
2 (Data Constructor)	Data.ArithRel, Data.FOL.Arith
rel	Data.ArithRel, Data.FOL.Arith
RelOp
1 (Type/Class)	Text.LPFile
2 (Type/Class)	Data.ArithRel, Algorithm.Simplex2, Data.FOL.Arith
render
1 (Function)	Text.SDPFile
2 (Function)	Text.GurobiSol
3 (Function)	Text.LPFile
renderSparse	Text.SDPFile
RestartStrategy	SAT
revForM	Util
revlex	Data.Polynomial
revMapM	Util
revSequence	Util
rootAdd	Data.AlgebraicNumber.Root
rootIndex	Data.AlgebraicNumber.Real
rootMul	Data.AlgebraicNumber.Root
rootNthRoot	Data.AlgebraicNumber.Root
RootOf	Algorithm.CAD
rootRecip	Data.AlgebraicNumber.Root
rootScale	Data.AlgebraicNumber.Root
rootShift	Data.AlgebraicNumber.Root
rootSimpPoly	Data.AlgebraicNumber.Root
Row	Algorithm.Simplex
RowIndex	Algorithm.Simplex
S1	Text.LPFile
S2	Text.LPFile
Sat	Data.FOL.Arith
satPrintModel	SAT.Printer
SatResult	Data.FOL.Arith
SearchStrategy	SAT.PBO
SemiContinuousVariable	Text.LPFile
semiContinuousVariables	Text.LPFile
separate	Data.Polynomial.RootSeparation.Sturm
separate'	Data.Polynomial.RootSeparation.Sturm
setCCMin	SAT
setCheckModel	SAT
setConfBudget	SAT
setLearningStrategy	SAT
setLearntSizeFirst	SAT
setLearntSizeInc	SAT
setLogger
1 (Function)	SAT
2 (Function)	Algorithm.Simplex2
3 (Function)	Algorithm.MIPSolver2
setNThread	Algorithm.MIPSolver2
setObj
1 (Function)	Converter.PBSetObj
2 (Function)	Algorithm.Simplex2
setObjFun	Algorithm.Simplex
setOptDir	Algorithm.Simplex2
setPivotStrategy	Algorithm.Simplex2
setRandomFreq	SAT
setRandomSeed	SAT
setRestartFirst	SAT
setRestartInc	SAT
setRestartStrategy	SAT
setRow	Algorithm.Simplex
setShowRational	Algorithm.MIPSolver2
setUsePB	SAT.TseitinEncoder
setVarPolarity	SAT
showAtom	Data.LA
showEntity	Algorithm.FOLModelFinder
showExpr	Data.LA
showModel	Algorithm.FOLModelFinder
showOp	Data.ArithRel, Data.FOL.Arith
showOPB	Text.PBFile
showRational	Util
showRationalAsFiniteDecimal	Util
showValue	Algorithm.Simplex2
showWBO	Text.PBFile
Sign	Data.Sign
signOf	Data.Sign
simpARealPoly	Data.AlgebraicNumber.Real
simplex
1 (Function)	Algorithm.Simplex
2 (Function)	Algorithm.LPSolver
SMTLIB2	Converter.LP2SMT
SoftConstraint	Text.PBFile
SoftFormula	Text.PBFile
solve
1 (Function)	SAT
2 (Function)	SAT.PBO.UnsatBased
3 (Function)	SAT.PBO.MSU4
4 (Function)	Algorithm.ContiTraverso
5 (Function)	Algorithm.LPSolverHL
6 (Function)	Algorithm.CAD
7 (Function)	Algorithm.FourierMotzkin.Core, Algorithm.FourierMotzkin
8 (Function)	Algorithm.Cooper.Core, Algorithm.Cooper
9 (Function)	Algorithm.OmegaTest
solve'
1 (Function)	Algorithm.ContiTraverso
2 (Function)	Algorithm.CAD
3 (Function)	Algorithm.FourierMotzkin.Core
solveFor	Data.LA
solveFormula
1 (Function)	Algorithm.FourierMotzkin.FOL, Algorithm.FourierMotzkin
2 (Function)	Algorithm.Cooper.FOL, Algorithm.Cooper
solveQFFormula	Algorithm.Cooper.Core, Algorithm.Cooper
solveQFLA
1 (Function)	Algorithm.Cooper.Core, Algorithm.Cooper
2 (Function)	Algorithm.OmegaTest
Solver
1 (Type/Class)	SAT
2 (Type/Class)	Algorithm.CongruenceClosure
3 (Type/Class)	Algorithm.LPSolver
4 (Type/Class)	Algorithm.Simplex2
5 (Type/Class)	Algorithm.MIPSolver2
SolverValue	Algorithm.Simplex2
solveWBO
1 (Function)	SAT.PBO.UnsatBased
2 (Function)	SAT.PBO.MSU4
solveWith	SAT
SOS	Text.LPFile
sos	Text.LPFile
SOSType	Text.LPFile
spolynomial	Data.Polynomial.GroebnerBasis
SQFree	Data.Polynomial
sqfree
1 (Function)	Data.Polynomial
2 (Function)	Data.Polynomial.Factorization.FiniteField
sqfreeChar0	Data.Polynomial.Factorization.SquareFree
Strategy	Data.Polynomial.GroebnerBasis
SturmChain	Data.Polynomial.RootSeparation.Sturm
sturmChain	Data.Polynomial.RootSeparation.Sturm
subst	Data.Polynomial
SugarStrategy	Data.Polynomial.GroebnerBasis
Sum	Text.PBFile
symbol	Data.Sign
T
1 (Data Constructor)	Algorithm.FOLModelFinder
2 (Data Constructor)	Data.FOL.Formula, Data.FOL.Arith
T'	Algorithm.Cooper.Core, Algorithm.Cooper
Tableau	Algorithm.Simplex
tableau	Algorithm.LPSolver
tdeg	Data.Polynomial
tderiv	Data.Polynomial
tdiv	Data.Polynomial
tdivides	Data.Polynomial
Term
1 (Type/Class)	Data.Polynomial
2 (Type/Class)	Text.PBFile
3 (Type/Class)	Algorithm.FOLModelFinder
4 (Type/Class)	Text.LPFile
5 (Data Constructor)	Text.LPFile
terms
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
thAssertLit	SAT.TheorySolver
thCheck	SAT.TheorySolver
TheorySolver
1 (Type/Class)	SAT.TheorySolver
2 (Data Constructor)	SAT.TheorySolver
thExplain	SAT.TheorySolver
thPopBacktrackPoint	SAT.TheorySolver
thPushBacktrackPoint	SAT.TheorySolver
tintegral	Data.Polynomial
TmApp	Algorithm.FOLModelFinder
tmult	Data.Polynomial
TmVar	Algorithm.FOLModelFinder
toCSV	Algorithm.Simplex
toFOLExpr	Data.LA.FOL
toFOLFormula	Data.LA.FOL
toLAAtom	Algorithm.FourierMotzkin.Core
toMonic	Data.Polynomial
topCost	Text.MaxSAT
toRat	Algorithm.FourierMotzkin.Core
toSkolemNF	Algorithm.FOLModelFinder
toStandardForm	Algorithm.LPUtil
toStandardForm'	Algorithm.LPUtil
toUPolynomialOf	Data.Polynomial
toValue	Algorithm.Simplex2
true	Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith
tweakParams	SAT.PBO
UMonomial	Data.Polynomial
Unbounded
1 (Data Constructor)	Algorithm.LPSolverHL, Algorithm.MIPSolverHL
2 (Data Constructor)	Algorithm.Simplex2
unDNF	Data.DNF
unitVar	Data.LA
Unknown	Data.FOL.Arith
unliftBool	Data.LBool
Unsat
1 (Data Constructor)	Algorithm.Simplex2
2 (Data Constructor)	Data.FOL.Arith
UnsatBased	SAT.PBO
UPolynomial	Data.Polynomial
UserDefinedCut	Text.LPFile
UTerm	Data.Polynomial
validLit	SAT.Types
validVar	SAT.Types
Var
1 (Type/Class)	Data.Polynomial
2 (Type/Class)	Text.PBFile
3 (Type/Class)	SAT.Types, SAT
4 (Data Constructor)	SAT.TseitinEncoder
5 (Type/Class)	Algorithm.FOLModelFinder
6 (Type/Class)	Algorithm.CongruenceClosure
7 (Type/Class)	Data.AlgebraicNumber.Root
8 (Type/Class)	Text.LPFile
9 (Type/Class)	Data.Var
10 (Type/Class)	Algorithm.Simplex2
11 (Data Constructor)	Data.FOL.Arith
var
1 (Function)	Data.Polynomial
2 (Function)	Data.LA
3 (Function)	Data.FOL.Arith
varBounds	Text.LPFile
varBumpActivity	SAT
varDecayActivity	SAT
Variables	Data.Var
variables	Text.LPFile
VarInfo
1 (Type/Class)	Text.LPFile
2 (Data Constructor)	Text.LPFile
varInfo	Text.LPFile
VarMap
1 (Type/Class)	SAT.Types
2 (Type/Class)	Data.Var
varName	Text.LPFile
Vars	Data.Polynomial
vars
1 (Function)	Data.Polynomial
2 (Function)	Data.Var
VarSet
1 (Type/Class)	SAT.Types
2 (Type/Class)	Data.Var
VarType	Text.LPFile
varType	Text.LPFile
version	Version
wboNumVars	Text.PBFile
WCNF
1 (Type/Class)	Text.MaxSAT
2 (Data Constructor)	Text.MaxSAT
Weight	Text.MaxSAT
WeightedClause	Text.MaxSAT
WeightedTerm	Text.PBFile
X
1 (Type/Class)	Data.Polynomial
2 (Data Constructor)	Data.Polynomial
YICES	Converter.LP2SMT
Zero	Data.Sign