Index

.&&.	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
./=.	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
.<.	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
.<=.
1 (Function)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Function)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
.<=>.	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
.==.
1 (Function)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Function)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
.=>.	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
.>.	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
.>=.
1 (Function)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Function)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
.\|.	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
.\|\|.	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
:*:	ToySolver.Data.FOL.Arith
:+	ToySolver.Data.AlgebraicNumber.Complex
:+:	ToySolver.Data.FOL.Arith
:/:	ToySolver.Data.FOL.Arith
AComplex	ToySolver.Data.AlgebraicNumber.Complex
AdaptiveSearch	ToySolver.SAT.PBO
addAtLeast	ToySolver.SAT
addAtMost	ToySolver.SAT
addClause	ToySolver.SAT
addConstraint
1 (Function)	ToySolver.SAT.Integer
2 (Function)	ToySolver.Arith.LPSolver
addConstraintSoft	ToySolver.SAT.Integer
addConstraintWithArtificialVariable	ToySolver.Arith.LPSolver
addExactly	ToySolver.SAT
addFormula	ToySolver.SAT.TseitinEncoder
addLowerBound	ToySolver.SAT.PBO.Context
addPBAtLeast
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addPBAtLeastSoft
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addPBAtMost
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addPBAtMostSoft
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addPBExactly
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addPBExactlySoft
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBNLC
addRow	ToySolver.Arith.Simplex
addSolution
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
addXORClause	ToySolver.SAT
addXORClauseSoft	ToySolver.SAT
allMCSAssumptions
1 (Function)	ToySolver.SAT.MUS.CAMUS
2 (Function)	ToySolver.SAT.MUS.DAA
allMUSAssumptions
1 (Function)	ToySolver.SAT.MUS.CAMUS
2 (Function)	ToySolver.SAT.MUS.DAA
And
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Data.BoolExpr
3 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
andB	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
applySubst	ToySolver.Data.LA
applySubst1	ToySolver.Data.LA
applySubst1Atom	ToySolver.Data.LA
applySubstAtom	ToySolver.Data.LA
approx
1 (Function)	ToySolver.Data.AlgebraicNumber.Sturm
2 (Function)	ToySolver.Data.AlgebraicNumber.Real
approx'	ToySolver.Data.AlgebraicNumber.Sturm
approxInterval	ToySolver.Data.AlgebraicNumber.Real
AReal	ToySolver.Data.AlgebraicNumber.Real
areCongruent	ToySolver.EUF.CongruenceClosure
areCongruentFlatTerm	ToySolver.EUF.CongruenceClosure
areDualDNFs	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
areEqual	ToySolver.EUF.EUFSolver
ArminRestarts	ToySolver.SAT
asConst	ToySolver.Data.LA
assert	ToySolver.SMT
assertAtom	ToySolver.Arith.Simplex2
assertAtom'	ToySolver.Arith.Simplex2
assertAtomEx	ToySolver.Arith.Simplex2
assertAtomEx'	ToySolver.Arith.Simplex2
assertEqual	ToySolver.EUF.EUFSolver
assertEqual'	ToySolver.EUF.EUFSolver
assertLower	ToySolver.Arith.Simplex2
assertLower'	ToySolver.Arith.Simplex2
assertNamed	ToySolver.SMT
assertNotEqual	ToySolver.EUF.EUFSolver
assertNotEqual'	ToySolver.EUF.EUFSolver
assertUpper	ToySolver.Arith.Simplex2
assertUpper'	ToySolver.Arith.Simplex2
AtLeast	ToySolver.SAT.Types, ToySolver.SAT
Atom
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Type/Class)	ToySolver.Data.FOL.Arith
3 (Type/Class)	ToySolver.Data.LA, ToySolver.Arith.Simplex2
4 (Data Constructor)	ToySolver.Data.BoolExpr
5 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
6 (Type/Class)	ToySolver.EUF.FiniteModelFinder
basis	ToySolver.Data.Polynomial.GroebnerBasis
basis'	ToySolver.Data.Polynomial.GroebnerBasis
basisOfBerlekampSubalgebra	ToySolver.Data.Polynomial.Factorization.FiniteField
BC	ToySolver.SAT.PBO
BCD	ToySolver.SAT.PBO
BCD2	ToySolver.SAT.PBO
berlekamp	ToySolver.Data.Polynomial.Factorization.FiniteField
BinarySearch	ToySolver.SAT.PBO
Block	ToySolver.Text.SDPFile
blockElem	ToySolver.Text.SDPFile
blockStruct	ToySolver.Text.SDPFile
Boolean	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
BoolExpr	ToySolver.Data.BoolExpr
Bound	ToySolver.Arith.Simplex2
boundExplanation	ToySolver.Arith.Simplex2
BoundExpr	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Bounds
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Type/Class)	ToySolver.Arith.FourierMotzkin.Base
BoundsEnv	ToySolver.Data.LA, ToySolver.Arith.BoundsInference
boundsToConstrs	ToySolver.Arith.FourierMotzkin.Base
boundValue	ToySolver.Arith.Simplex2
BudgetExceeded
1 (Type/Class)	ToySolver.SAT
2 (Data Constructor)	ToySolver.SAT
cabook_proposition_5_10	ToySolver.Data.Polynomial.Factorization.Hensel.Internal
cabook_proposition_5_11	ToySolver.Data.Polynomial.Factorization.Hensel.Internal
camus	ToySolver.SAT.MUS.CAMUS
cardinalityReduction	ToySolver.SAT.Types
ceiling'	ToySolver.Data.Delta
Cell	ToySolver.Arith.CAD
check
1 (Function)	ToySolver.EUF.EUFSolver
2 (Function)	ToySolver.Arith.Simplex2
checkDuality	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
checkDualityA	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
checkDualityB	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
checkRealByCAD	ToySolver.Arith.OmegaTest
checkRealByFM	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
checkRealBySimplex	ToySolver.Arith.OmegaTest
checkRealByVS	ToySolver.Arith.OmegaTest
checkRealNoCheck	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
checkSAT	ToySolver.SMT
checkSATAssuming	ToySolver.SMT
Clause
1 (Type/Class)	ToySolver.SAT.Types, ToySolver.SAT
2 (Type/Class)	ToySolver.EUF.FiniteModelFinder
clauses
1 (Function)	ToySolver.Text.GCNF
2 (Function)	ToySolver.Text.MaxSAT
clauseSubsume	ToySolver.SAT.Types
clauseToPBLinAtLeast	ToySolver.SAT.Types
clear
1 (Function)	ToySolver.Internal.Data.SeqQueue
2 (Function)	ToySolver.Internal.Data.Vec
3 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
4 (Function)	ToySolver.Internal.Data.PriorityQueue
clearLogger	ToySolver.Arith.Simplex2
clone
1 (Function)	ToySolver.Internal.Data.Vec
2 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
3 (Function)	ToySolver.Internal.Data.PriorityQueue
cloneSolver	ToySolver.Arith.Simplex2
coeff
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
coeffMap
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
ColIndex	ToySolver.Arith.Simplex
collectBounds	ToySolver.Arith.FourierMotzkin.Base
collectNonnegVars	ToySolver.Arith.LPSolver
combineMaybe	ToySolver.Internal.Util
compilationTime	ToySolver.Version
Complement	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
computeInterval	ToySolver.Data.LA, ToySolver.Arith.BoundsInference
condition_1_1	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_1_1_solve	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_1_2	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_1_2_solve	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_1_3	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_1_3_solve	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_2_1	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
condition_2_1_solve	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
Config
1 (Type/Class)	ToySolver.SAT
2 (Data Constructor)	ToySolver.SAT
configCCMin	ToySolver.SAT
configCheckModel	ToySolver.SAT
configConstrDecay	ToySolver.SAT
configEnableBackwardSubsumptionRemoval	ToySolver.SAT
configEnableForwardSubsumptionRemoval	ToySolver.SAT
configEnablePBSplitClausePart	ToySolver.SAT
configEnablePhaseSaving	ToySolver.SAT
configLearningStrategy	ToySolver.SAT
configLearntSizeFirst	ToySolver.SAT
configLearntSizeInc	ToySolver.SAT
configPBHandlerType	ToySolver.SAT
configRandomFreq	ToySolver.SAT
configRestartFirst	ToySolver.SAT
configRestartInc	ToySolver.SAT
configRestartStrategy	ToySolver.SAT
configVarDecay	ToySolver.SAT
conjugate	ToySolver.Data.AlgebraicNumber.Complex
Const	ToySolver.Data.FOL.Arith
constant
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
constExpr	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Constr	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
Constraint
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constraints	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constraintsToDNF	ToySolver.Arith.FourierMotzkin.Base
constrExpr	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
ConstrID
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.Arith.Simplex2
ConstrIDSet	ToySolver.Arith.Simplex2
constrIndicator	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constrIsLazy	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constrLabel	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constrLB	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
constrUB	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
cont	ToySolver.Data.Polynomial
Context	ToySolver.SAT.PBO.Context
ContinuousVariable	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
ContPP	ToySolver.Data.Polynomial
convert
1 (Function)	ToySolver.Converter.SAT2PB
2 (Function)	ToySolver.Converter.PB2WBO
3 (Function)	ToySolver.Converter.PB2SMP
4 (Function)	ToySolver.Converter.PB2LSP
5 (Function)	ToySolver.Converter.MIP2SMT
6 (Function)	ToySolver.Converter.PB2IP
7 (Function)	ToySolver.Converter.SAT2IP
8 (Function)	ToySolver.Converter.WBO2PB
9 (Function)	ToySolver.Converter.MaxSAT2NLPB
10 (Function)	ToySolver.Converter.MaxSAT2WBO
11 (Function)	ToySolver.Converter.MaxSAT2IP
convertWBO
1 (Function)	ToySolver.Converter.PB2LSP
2 (Function)	ToySolver.Converter.PB2IP
costs	ToySolver.Text.SDPFile
CS	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
currentObjValue	ToySolver.Arith.Simplex
currentValue	ToySolver.Arith.Simplex
cutResolve	ToySolver.SAT.Types
daa	ToySolver.SAT.MUS.DAA
declareConst	ToySolver.SMT
declareFSym	ToySolver.SMT
declareFun	ToySolver.SMT
declareSort	ToySolver.SMT
declareSSym	ToySolver.SMT
defaultBounds	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
defaultCCMin	ToySolver.SAT
defaultEnableBackwardSubsumptionRemoval	ToySolver.SAT
defaultEnableForwardSubsumptionRemoval	ToySolver.SAT
defaultEnableObjFunVarsHeuristics	ToySolver.SAT.PBO
defaultEnablePhaseSaving	ToySolver.SAT
defaultLB	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
defaultLearntSizeFirst	ToySolver.SAT
defaultLearntSizeInc	ToySolver.SAT
defaultPBSplitClausePart	ToySolver.SAT
defaultRandomFreq	ToySolver.SAT
defaultRestartFirst	ToySolver.SAT
defaultRestartInc	ToySolver.SAT
defaultTrialLimitConf	ToySolver.SAT.PBO
defaultUB	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
define	ToySolver.Arith.LPSolver
deg	ToySolver.Data.Polynomial
Degree	ToySolver.Data.Polynomial
deleteRedundancy	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
Delta
1 (Type/Class)	ToySolver.Data.Delta
2 (Data Constructor)	ToySolver.Data.Delta
delta	ToySolver.Data.Delta
deltaPart	ToySolver.Data.Delta
DenseBlock	ToySolver.Text.SDPFile
denseBlock	ToySolver.Text.SDPFile
DenseMatrix	ToySolver.Text.SDPFile
denseMatrix	ToySolver.Text.SDPFile
Dequeue	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
dequeue	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
dequeueBatch	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
deriv	ToySolver.Data.Polynomial
diagBlock	ToySolver.Text.SDPFile
div	ToySolver.Data.Polynomial
divides	ToySolver.Data.Polynomial
Divisible	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
divMod	ToySolver.Data.Polynomial
divModMP	ToySolver.Data.Polynomial
DNF
1 (Type/Class)	ToySolver.Data.DNF
2 (Data Constructor)	ToySolver.Data.DNF
dualSimplex
1 (Function)	ToySolver.Arith.Simplex2
2 (Function)	ToySolver.Arith.Simplex
3 (Function)	ToySolver.Arith.LPSolver
dump	ToySolver.Arith.Simplex2
EAp	ToySolver.SMT
EFrac	ToySolver.SMT
eliminateQuantifiers
1 (Function)	ToySolver.Arith.FourierMotzkin.FOL, ToySolver.Arith.FourierMotzkin
2 (Function)	ToySolver.Arith.Cooper.FOL, ToySolver.Arith.Cooper
eliminateQuantifiers'	ToySolver.Arith.FourierMotzkin.FOL
emptySolver	ToySolver.Arith.LPSolver
emptyTableau	ToySolver.Arith.Simplex
emptyTheory	ToySolver.SAT.TheorySolver
encodeConj	ToySolver.SAT.TseitinEncoder
encodeConjWithPolarity	ToySolver.SAT.TseitinEncoder
encodeDisj	ToySolver.SAT.TseitinEncoder
encodeDisjWithPolarity	ToySolver.SAT.TseitinEncoder
encodeFormula	ToySolver.SAT.TseitinEncoder
encodeFormulaWithPolarity	ToySolver.SAT.TseitinEncoder
encodeITE	ToySolver.SAT.TseitinEncoder
encodeITEWithPolarity	ToySolver.SAT.TseitinEncoder
Encoder	ToySolver.SAT.TseitinEncoder
encSolver	ToySolver.SAT.TseitinEncoder
Enqueue	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
enqueue	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
enqueueBatch	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
Entity
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.EUF.FiniteModelFinder
EntityTuple
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.EUF.FiniteModelFinder
enumMCSAssumptions	ToySolver.SAT.MUS.CAMUS
enumMinimalHittingSets
1 (Function)	ToySolver.Combinatorial.HittingSet.Simple
2 (Function)	ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
Eql
1 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
eqR	ToySolver.Arith.FourierMotzkin.Base
Equiv
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Data.BoolExpr
3 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
Error	ToySolver.SMT
eval
1 (Function)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Function)	ToySolver.Data.Polynomial
3 (Function)	ToySolver.SAT.Integer
4 (Function)	ToySolver.SMT
evalAp	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
evalAtLeast	ToySolver.SAT.Types, ToySolver.SAT
evalAtom
1 (Function)	ToySolver.Data.FOL.Arith
2 (Function)	ToySolver.Data.LA
3 (Function)	ToySolver.EUF.FiniteModelFinder
evalBounds	ToySolver.Arith.FourierMotzkin.Base
evalCell	ToySolver.Arith.CAD
evalClause
1 (Function)	ToySolver.SAT.Types, ToySolver.SAT
2 (Function)	ToySolver.EUF.FiniteModelFinder
evalClauses	ToySolver.EUF.FiniteModelFinder
evalClausesU	ToySolver.EUF.FiniteModelFinder
evalExactly	ToySolver.SAT.Types, ToySolver.SAT
evalExpr
1 (Function)	ToySolver.Data.FOL.Arith
2 (Function)	ToySolver.Data.LA
evalFormula
1 (Function)	ToySolver.EUF.FiniteModelFinder
2 (Function)	ToySolver.SAT.TseitinEncoder
evalFSym	ToySolver.SMT
evalLinear	ToySolver.Data.LA
evalLit
1 (Function)	ToySolver.SAT.Types, ToySolver.SAT
2 (Function)	ToySolver.EUF.FiniteModelFinder
3 (Function)	ToySolver.Arith.Cooper.Base
evalObjectiveFunction	ToySolver.SAT.PBO.Context
evalOp	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
evalPBLinAtLeast	ToySolver.SAT.Types, ToySolver.SAT
evalPBLinExactly	ToySolver.SAT.Types, ToySolver.SAT
evalPBLinSum	ToySolver.SAT.Types, ToySolver.SAT
evalPBSum	ToySolver.SAT.PBNLC
evalPoint	ToySolver.Arith.CAD
evalQFFormula
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
evalTerm	ToySolver.EUF.FiniteModelFinder
evalVar	ToySolver.SAT.Types, ToySolver.SAT
evalXORClause	ToySolver.SAT.Types, ToySolver.SAT
Exactly	ToySolver.SAT.Types, ToySolver.SAT
Exception	ToySolver.SMT
exgcd	ToySolver.Data.Polynomial
Exists
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
explain
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
3 (Function)	ToySolver.Arith.Simplex2
explainConst	ToySolver.EUF.CongruenceClosure
explainFlatTerm	ToySolver.EUF.CongruenceClosure
Expr
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
3 (Type/Class)	ToySolver.Data.FOL.Arith
4 (Type/Class)	ToySolver.Data.LA
5 (Type/Class)	ToySolver.SAT.Integer
6 (Data Constructor)	ToySolver.SAT.Integer
7 (Type/Class)	ToySolver.SMT
exprSort	ToySolver.SMT
ExprZ
1 (Type/Class)	ToySolver.Arith.FourierMotzkin.Base
2 (Type/Class)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
Extended	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
extract	ToySolver.Data.LA
extractMaybe	ToySolver.Data.LA
F
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
Factor	ToySolver.Data.Polynomial
factor
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.Polynomial.Factorization.FiniteField
3 (Function)	ToySolver.Data.Polynomial.Factorization.Zassenhaus
4 (Function)	ToySolver.Data.Polynomial.Factorization.Kronecker
Failure
1 (Type/Class)	ToySolver.Combinatorial.HittingSet.SHD
2 (Data Constructor)	ToySolver.Combinatorial.HittingSet.SHD
3 (Type/Class)	ToySolver.Combinatorial.HittingSet.HTCBDD
4 (Data Constructor)	ToySolver.Combinatorial.HittingSet.HTCBDD
false	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
findModel	ToySolver.EUF.FiniteModelFinder
findMUSAssumptions
1 (Function)	ToySolver.SAT.MUS
2 (Function)	ToySolver.SAT.MUS.QuickXplain
findPoly	ToySolver.Data.AlgebraicNumber.Root
findPrimeImplicateOrPrimeImplicant	ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
findSample	ToySolver.Arith.CAD
Finite	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
FlatTerm	ToySolver.EUF.CongruenceClosure
flatTermToFSym
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
flipOp	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
floor'	ToySolver.Data.Delta
fold	ToySolver.Data.BoolExpr
Forall
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
Formula
1 (Type/Class)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Type/Class)	ToySolver.Wang
3 (Type/Class)	ToySolver.EUF.FiniteModelFinder
4 (Type/Class)	ToySolver.SAT.TseitinEncoder
fracPart	ToySolver.Internal.Util
fromCoeffMap
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
fromFOLAtom	ToySolver.Data.LA.FOL
fromFOLExpr	ToySolver.Data.LA.FOL
fromLAAtom
1 (Function)	ToySolver.Arith.FourierMotzkin.Base
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
fromOrdRel	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
fromReal	ToySolver.Data.Delta
fromTerm	ToySolver.Data.Polynomial
fromTerms
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
fromVar	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
FSym
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.EUF.FiniteModelFinder
3 (Type/Class)	ToySolver.SMT
fsymToFlatTerm
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
fsymToTerm
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
FTApp	ToySolver.EUF.CongruenceClosure
FTConst	ToySolver.EUF.CongruenceClosure
FunDef
1 (Type/Class)	ToySolver.SMT
2 (Data Constructor)	ToySolver.SMT
FunType	ToySolver.SMT
gcd	ToySolver.Data.Polynomial
gcd'	ToySolver.Data.Polynomial
GClause	ToySolver.Text.GCNF
GCNF
1 (Type/Class)	ToySolver.Text.GCNF
2 (Data Constructor)	ToySolver.Text.GCNF
Ge
1 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
generateCNFAndDNF	ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
GenericSolver	ToySolver.Arith.Simplex2
GenericVec	ToySolver.Internal.Data.Vec
GenFormula	ToySolver.EUF.FiniteModelFinder
GenLit	ToySolver.EUF.FiniteModelFinder
getArray	ToySolver.Internal.Data.Vec
getAssumptionsImplications	ToySolver.SAT
getBestModel
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
3 (Function)	ToySolver.Arith.MIPSolver2
getBestSolution
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
3 (Function)	ToySolver.Arith.MIPSolver2
getBestValue
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
3 (Function)	ToySolver.Arith.MIPSolver2
getBounds	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
getCapacity	ToySolver.Internal.Data.Vec
getCoeff	ToySolver.Arith.Simplex2
getCol	ToySolver.Arith.Simplex2
getConfig	ToySolver.SAT
getDefinitions	ToySolver.SAT.TseitinEncoder
getElems
1 (Function)	ToySolver.Internal.Data.Vec
2 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
3 (Function)	ToySolver.Internal.Data.PriorityQueue
getEnableBackwardSubsumptionRemoval	ToySolver.SAT
getEnableForwardSubsumptionRemoval	ToySolver.SAT
getEnableObjFunVarsHeuristics	ToySolver.SAT.PBO
getEnablePhaseSaving	ToySolver.SAT
getFailedAssumptions	ToySolver.SAT
getFixedLiterals	ToySolver.SAT
getGlobalDeclarations	ToySolver.SMT
getHeapArray
1 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Function)	ToySolver.Internal.Data.PriorityQueue
getHeapVec
1 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Function)	ToySolver.Internal.Data.PriorityQueue
getLB	ToySolver.Arith.Simplex2
getLitFixed	ToySolver.SAT
getLowerBound	ToySolver.SAT.PBO.Context
getModel
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
3 (Function)	ToySolver.SAT
4 (Function)	ToySolver.Arith.Simplex2
5 (Function)	ToySolver.SMT
6 (Function)	ToySolver.Arith.LPSolver
getNConstraints	ToySolver.SAT
getNLearntConstraints	ToySolver.SAT
getNVars	ToySolver.SAT
getObj	ToySolver.Arith.Simplex2
getObjectiveFunction	ToySolver.SAT.PBO.Context
getObjValue	ToySolver.Arith.Simplex2
getOptDir	ToySolver.Arith.Simplex2
getPBSplitClausePart	ToySolver.SAT
getRandomGen	ToySolver.SAT
getRawModel	ToySolver.Arith.Simplex2
getRow	ToySolver.Arith.Simplex2
getSearchStrategy	ToySolver.SAT.PBO
getSearchUpperBound	ToySolver.SAT.PBO.Context
getSize	ToySolver.Internal.Data.Vec
getTableau
1 (Function)	ToySolver.Arith.Simplex2
2 (Function)	ToySolver.Arith.LPSolver
getTrialLimitConf	ToySolver.SAT.PBO
getUB	ToySolver.Arith.Simplex2
getUnsatAssumptions	ToySolver.SMT
getUnsatCore	ToySolver.SMT
getValue	ToySolver.Arith.Simplex2
getVarFixed	ToySolver.SAT
getVarType	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
gitHash	ToySolver.Version
goldenRatio	ToySolver.Data.AlgebraicNumber.Real
grevlex	ToySolver.Data.Polynomial
grlex	ToySolver.Data.Polynomial
GroupIndex	ToySolver.Text.GCNF
growTo	ToySolver.Internal.Data.Vec
Gt	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
halve	ToySolver.Data.AlgebraicNumber.Sturm
halve'	ToySolver.Data.AlgebraicNumber.Sturm
height	ToySolver.Data.AlgebraicNumber.Real
hensel	ToySolver.Data.Polynomial.Factorization.Hensel.Internal, ToySolver.Data.Polynomial.Factorization.Hensel
IfThenElse	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
imagPart	ToySolver.Data.AlgebraicNumber.Complex
IModel	ToySolver.SAT.Types, ToySolver.SAT
Imply
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Data.BoolExpr
3 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
Index
1 (Type/Class)	ToySolver.Internal.Data.Vec
2 (Type/Class)	ToySolver.Internal.Data.IndexedPriorityQueue
3 (Type/Class)	ToySolver.Internal.Data.PriorityQueue
inferBounds	ToySolver.Arith.BoundsInference
instantiateAtLeast	ToySolver.SAT.Types
instantiateClause	ToySolver.SAT.Types
instantiatePBLinAtLeast	ToySolver.SAT.Types
instantiatePBLinExactly	ToySolver.SAT.Types
instantiateXORClause	ToySolver.SAT.Types
IntegerVariable	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
integerVariables	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
integral	ToySolver.Data.Polynomial
interpolate	ToySolver.Data.Polynomial.Interpolation.Lagrange
intersectBounds	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Interval	ToySolver.Arith.CAD
IOURef	ToySolver.Internal.Data.IOURef
isAlgebraicInteger	ToySolver.Data.AlgebraicNumber.Real
isBasicVariable	ToySolver.Arith.Simplex2
isCounterExampleOf	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
IsEqRel	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
isFeasible
1 (Function)	ToySolver.Arith.Simplex2
2 (Function)	ToySolver.Arith.Simplex
isFinished
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
isInteger	ToySolver.Internal.Util
isInteger'	ToySolver.Data.Delta
isNegativeCoeff	ToySolver.Data.Polynomial
isNonBasicVariable	ToySolver.Arith.Simplex2
IsNonneg	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
isolatingInterval	ToySolver.Data.AlgebraicNumber.Real
isOptimal
1 (Function)	ToySolver.Arith.Simplex2
2 (Function)	ToySolver.Arith.Simplex
isOptimum
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
IsOrdRel	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
IsPos
1 (Data Constructor)	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
2 (Data Constructor)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
isPrimitive	ToySolver.Data.Polynomial
isRational	ToySolver.Data.AlgebraicNumber.Real
isRedundant	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
isRootOf	ToySolver.Data.Polynomial
isSquareFree	ToySolver.Data.Polynomial
isUnsat
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
isValid	ToySolver.Wang
isValidTableau	ToySolver.Arith.Simplex
IsZero	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
ITE	ToySolver.Data.BoolExpr
ite	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
iteBoolean	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
Label	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Language	ToySolver.Converter.MIP2SMT
lastGroupIndex	ToySolver.Text.GCNF
LBool	ToySolver.Data.LBool
lc	ToySolver.Data.Polynomial
lcm	ToySolver.Data.Polynomial
Le
1 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
LearningClause	ToySolver.SAT
LearningHybrid	ToySolver.SAT
LearningStrategy	ToySolver.SAT
lex	ToySolver.Data.Polynomial
lFalse	ToySolver.Data.LBool
lift1	ToySolver.Data.LA
lift2	ToySolver.Data.AlgebraicNumber.Root
liftBool	ToySolver.Data.LBool
linearize	ToySolver.SAT.Integer
linearizePBSum	ToySolver.SAT.PBNLC
linearizePBSumWithPolarity	ToySolver.SAT.PBNLC
LinearSearch	ToySolver.SAT.PBO
Lit
1 (Type/Class)	ToySolver.SAT.Types, ToySolver.SAT
2 (Type/Class)	ToySolver.EUF.FiniteModelFinder
3 (Type/Class)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
literal	ToySolver.SAT.Types, ToySolver.SAT
LitMap	ToySolver.SAT.Types
litNot	ToySolver.SAT.Types, ToySolver.SAT
litPolarity	ToySolver.SAT.Types, ToySolver.SAT
LitSet	ToySolver.SAT.Types
litUndef	ToySolver.SAT.Types
litVar	ToySolver.SAT.Types, ToySolver.SAT
lm	ToySolver.Data.Polynomial
lnot	ToySolver.Data.LBool
logMessage	ToySolver.SAT.PBO.Context
lookupCoeff
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
lookupRow	ToySolver.Arith.Simplex
LP	ToySolver.Arith.LPSolver
Lt	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
lt	ToySolver.Data.Polynomial
lTrue	ToySolver.Data.LBool
LubyRestarts	ToySolver.SAT
lUndef	ToySolver.Data.LBool
magnitude	ToySolver.Data.AlgebraicNumber.Complex
mapCoeff
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.LA
mapCoeffWithVar	ToySolver.Data.LA
matrices	ToySolver.Text.SDPFile
Matrix	ToySolver.Text.SDPFile
maximize
1 (Function)	ToySolver.Arith.LPSolverHL
2 (Function)	ToySolver.Arith.MIPSolverHL
maxsatPrintModel	ToySolver.SAT.Printer
maxSubsetSum	ToySolver.Combinatorial.SubsetSum
mcoprime	ToySolver.Data.Polynomial
MCS	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
mderiv	ToySolver.Data.Polynomial
mDim	ToySolver.Text.SDPFile
mdiv	ToySolver.Data.Polynomial
mdivides	ToySolver.Data.Polynomial
member	ToySolver.Internal.Data.IndexedPriorityQueue
mEquivClasses	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
merge	ToySolver.EUF.CongruenceClosure
merge'	ToySolver.EUF.CongruenceClosure
mergeFlatTerm	ToySolver.EUF.CongruenceClosure
mergeFlatTerm'	ToySolver.EUF.CongruenceClosure
Method	ToySolver.Combinatorial.HittingSet.HTCBDD
MethodKnuth	ToySolver.Combinatorial.HittingSet.HTCBDD
MethodToda	ToySolver.Combinatorial.HittingSet.HTCBDD
mfromIndices	ToySolver.Data.Polynomial
mfromIndicesMap	ToySolver.Data.Polynomial
mFunctions
1 (Function)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Function)	ToySolver.EUF.FiniteModelFinder
mgcd	ToySolver.Data.Polynomial
mindices	ToySolver.Data.Polynomial
mindicesMap	ToySolver.Data.Polynomial
minimalHittingSets
1 (Function)	ToySolver.Combinatorial.HittingSet.Simple
2 (Function)	ToySolver.Combinatorial.HittingSet.SHD
3 (Function)	ToySolver.Combinatorial.HittingSet.HTCBDD
4 (Function)	ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
minimalPolynomial
1 (Function)	ToySolver.Data.AlgebraicNumber.Real
2 (Function)	ToySolver.Data.AlgebraicNumber.Complex
minimize
1 (Function)	ToySolver.Arith.LPSolverHL
2 (Function)	ToySolver.Arith.MIPSolverHL
MiniSATRestarts	ToySolver.SAT
minSubsetSum	ToySolver.Combinatorial.SubsetSum
mintegral	ToySolver.Data.Polynomial
mlcm	ToySolver.Data.Polynomial
mmult	ToySolver.Data.Polynomial
mod	ToySolver.Data.Polynomial
Model
1 (Type/Class)	ToySolver.Text.GurobiSol
2 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
3 (Data Constructor)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
4 (Type/Class)	ToySolver.Data.Var, ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper, ToySolver.Arith.OmegaTest
5 (Type/Class)	ToySolver.SAT.Types, ToySolver.SAT
6 (Type/Class)	ToySolver.EUF.FiniteModelFinder
7 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
8 (Type/Class)	ToySolver.Arith.Simplex2
9 (Type/Class)	ToySolver.SMT
10 (Type/Class)	ToySolver.Arith.CAD
modify	ToySolver.Internal.Data.Vec
modify'	ToySolver.Internal.Data.Vec
modifyConfig	ToySolver.SAT
modifyIOURef	ToySolver.Internal.Data.IOURef
mone	ToySolver.Data.Polynomial
Monomial	ToySolver.Data.Polynomial
MonomialOrder	ToySolver.Data.Polynomial
MonotoneBoolean	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
mpow	ToySolver.Data.Polynomial
mRelations	ToySolver.EUF.FiniteModelFinder
MSS	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
MSU4	ToySolver.SAT.PBO
mUniverse
1 (Function)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Function)	ToySolver.EUF.FiniteModelFinder
mUnspecified	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
MUS	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
musPrintSol	ToySolver.SAT.Printer
name	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
narrow	ToySolver.Data.AlgebraicNumber.Sturm
narrow'	ToySolver.Data.AlgebraicNumber.Sturm
nAssigns	ToySolver.SAT
nat	ToySolver.Data.Polynomial
nBlock	ToySolver.Text.SDPFile
nConstraints	ToySolver.SAT
Neg	ToySolver.EUF.FiniteModelFinder
negatePBLinAtLeast	ToySolver.SAT.Types
negatePolarity	ToySolver.SAT.TseitinEncoder
NegInf
1 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Arith.CAD
negOp	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
NEq	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
new	ToySolver.Internal.Data.Vec
newConst
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
newEncoder	ToySolver.SAT.TseitinEncoder
NewFifo	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
newFifo	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
newFSym
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
newFun
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
newIOURef	ToySolver.Internal.Data.IOURef
newOptimizer	ToySolver.SAT.PBO
newOptimizer2	ToySolver.SAT.PBO
newPriorityQueue
1 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Function)	ToySolver.Internal.Data.PriorityQueue
newPriorityQueueBy
1 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Function)	ToySolver.Internal.Data.PriorityQueue
newSimpleContext	ToySolver.SAT.PBO.Context
newSimpleContext2	ToySolver.SAT.PBO.Context
newSolver
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
3 (Function)	ToySolver.SAT
4 (Function)	ToySolver.Arith.Simplex2
5 (Function)	ToySolver.SMT
6 (Function)	ToySolver.Arith.MIPSolver2
newSolverWithConfig	ToySolver.SAT
newVar
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.Integer
3 (Function)	ToySolver.Arith.Simplex2
4 (Function)	ToySolver.Arith.LPSolver
newVars	ToySolver.SAT
newVars_	ToySolver.SAT
nLearnt	ToySolver.SAT
normalize	ToySolver.SAT.PBO.Context
normalizeAtLeast	ToySolver.SAT.Types
normalizeClause	ToySolver.SAT.Types
Normalized	ToySolver.SAT.PBO.Context
normalizePBLinAtLeast	ToySolver.SAT.Types
normalizePBLinExactly	ToySolver.SAT.Types
normalizePBLinSum	ToySolver.SAT.Types
normalizePoly	ToySolver.Data.AlgebraicNumber.Root
normalizeXORClause	ToySolver.SAT.Types
NormalStrategy	ToySolver.Data.Polynomial.GroebnerBasis
Not
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Data.BoolExpr
3 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
notB	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
nthRoot	ToySolver.Data.AlgebraicNumber.Real
numClauses
1 (Function)	ToySolver.Text.GCNF
2 (Function)	ToySolver.Text.MaxSAT
numRoots	ToySolver.Data.AlgebraicNumber.Sturm
numRoots'	ToySolver.Data.AlgebraicNumber.Sturm
numVars
1 (Function)	ToySolver.Text.GCNF
2 (Function)	ToySolver.Text.MaxSAT
nVars
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.Arith.Simplex2
objDir	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
ObjectiveFunction
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
objectiveFunction	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
objExpr	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
objLabel	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
ObjLimit	ToySolver.Arith.Simplex2
objLimit	ToySolver.Arith.Simplex2
ObjMaxOne	ToySolver.Converter.ObjType, ToySolver.Converter.PBSetObj
ObjMaxZero	ToySolver.Converter.ObjType, ToySolver.Converter.PBSetObj
ObjNone	ToySolver.Converter.ObjType, ToySolver.Converter.PBSetObj
objRowIndex	ToySolver.Arith.Simplex
ObjType	ToySolver.Converter.ObjType, ToySolver.Converter.PBSetObj
occurFreq	ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
optCheckReal	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
optCheckSAT	ToySolver.Converter.MIP2SMT
OptDir	ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex2, ToySolver.Arith.Simplex, ToySolver.Arith.MIPSolverHL
optEnableBiasedSearch	ToySolver.SAT.PBO.BCD2
optEnableHardening	ToySolver.SAT.PBO.BCD2
optHTCBDDCommand	ToySolver.Combinatorial.HittingSet.HTCBDD
optimize
1 (Function)	ToySolver.SAT.PBO
2 (Function)	ToySolver.Arith.Simplex2
3 (Function)	ToySolver.Arith.MIPSolver2
4 (Function)	ToySolver.Arith.FourierMotzkin.Optimization
5 (Function)	ToySolver.Arith.LPSolverHL
6 (Function)	ToySolver.Arith.MIPSolverHL
Optimizer	ToySolver.SAT.PBO
Optimum
1 (Data Constructor)	ToySolver.Arith.Simplex2
2 (Data Constructor)	ToySolver.Arith.LPSolver
3 (Data Constructor)	ToySolver.Arith.LPSolverHL, ToySolver.Arith.MIPSolverHL
Options
1 (Type/Class)	ToySolver.Data.Polynomial.GroebnerBasis
2 (Data Constructor)	ToySolver.Data.Polynomial.GroebnerBasis
3 (Type/Class)	ToySolver.Converter.MIP2SMT
4 (Data Constructor)	ToySolver.Converter.MIP2SMT
5 (Type/Class)	ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain
6 (Data Constructor)	ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain
7 (Type/Class)	ToySolver.SAT.PBO.BCD2
8 (Data Constructor)	ToySolver.SAT.PBO.BCD2
9 (Type/Class)	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
10 (Data Constructor)	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
11 (Type/Class)	ToySolver.Combinatorial.HittingSet.SHD
12 (Data Constructor)	ToySolver.Combinatorial.HittingSet.SHD
13 (Type/Class)	ToySolver.Combinatorial.HittingSet.HTCBDD
14 (Data Constructor)	ToySolver.Combinatorial.HittingSet.HTCBDD
15 (Type/Class)	ToySolver.Arith.Simplex2
16 (Data Constructor)	ToySolver.Arith.Simplex2
17 (Type/Class)	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
18 (Data Constructor)	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
optKnownCSes	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
optKnownMCSes	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
optKnownMUSes	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
optLanguage	ToySolver.Converter.MIP2SMT
optLitPrinter	ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain
optLogger
1 (Function)	ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain
2 (Function)	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
OptMax	ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex2, ToySolver.Arith.Simplex, ToySolver.Arith.MIPSolverHL
optMethod	ToySolver.Combinatorial.HittingSet.HTCBDD
OptMin	ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex2, ToySolver.Arith.Simplex, ToySolver.Arith.MIPSolverHL
optOnGetErrorLine
1 (Function)	ToySolver.Combinatorial.HittingSet.SHD
2 (Function)	ToySolver.Combinatorial.HittingSet.HTCBDD
optOnGetLine
1 (Function)	ToySolver.Combinatorial.HittingSet.SHD
2 (Function)	ToySolver.Combinatorial.HittingSet.HTCBDD
optOnMCSFound	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
optOnMUSFound	ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
optOptimize	ToySolver.Converter.MIP2SMT
optProduceModel	ToySolver.Converter.MIP2SMT
OptResult
1 (Type/Class)	ToySolver.Arith.Simplex2
2 (Type/Class)	ToySolver.Arith.LPSolver
3 (Type/Class)	ToySolver.Arith.LPSolverHL, ToySolver.Arith.MIPSolverHL
optSetLogic	ToySolver.Converter.MIP2SMT
optSHDArgs	ToySolver.Combinatorial.HittingSet.SHD
optSHDCommand	ToySolver.Combinatorial.HittingSet.SHD
optSolvingNormalFirst	ToySolver.SAT.PBO.BCD2
optStrategy	ToySolver.Data.Polynomial.GroebnerBasis
OptUnsat	ToySolver.Arith.LPSolverHL, ToySolver.Arith.MIPSolverHL
optUpdateBest	ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain
Or
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Data.BoolExpr
3 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
orB	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
OrdRel
1 (Type/Class)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
2 (Data Constructor)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
ordRel	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
packageVersions	ToySolver.Version
PApp	ToySolver.EUF.FiniteModelFinder
parseByteString	ToySolver.Text.MaxSAT
parseDataFile	ToySolver.Text.SDPFile
parseDataString	ToySolver.Text.SDPFile
parseFile
1 (Function)	ToySolver.Data.MIP.LPFile
2 (Function)	ToySolver.Data.MIP.MPSFile
3 (Function)	ToySolver.Text.GCNF
4 (Function)	ToySolver.Text.MaxSAT
parseLPString	ToySolver.Data.MIP
parseMPSString	ToySolver.Data.MIP
parser
1 (Function)	ToySolver.Data.MIP.LPFile
2 (Function)	ToySolver.Data.MIP.MPSFile
parseSparseDataFile	ToySolver.Text.SDPFile
parseSparseDataString	ToySolver.Text.SDPFile
parseString
1 (Function)	ToySolver.Data.MIP.LPFile
2 (Function)	ToySolver.Data.MIP.MPSFile
3 (Function)	ToySolver.Text.GCNF
4 (Function)	ToySolver.Text.MaxSAT
PBHandlerType	ToySolver.SAT
PBHandlerTypeCounter	ToySolver.SAT
PBHandlerTypePueblo	ToySolver.SAT
PBLinAtLeast	ToySolver.SAT.Types, ToySolver.SAT
PBLinExactly	ToySolver.SAT.Types, ToySolver.SAT
PBLinSum	ToySolver.SAT.Types, ToySolver.SAT
PBLinTerm	ToySolver.SAT.Types, ToySolver.SAT
pbLowerBound	ToySolver.SAT.Types
pbPrintModel	ToySolver.SAT.Printer
pbSubsume	ToySolver.SAT.Types
PBSum	ToySolver.SAT.PBNLC
PBTerm	ToySolver.SAT.PBNLC
pbUpperBound	ToySolver.SAT.Types
pdiv	ToySolver.Data.Polynomial
pdivMod	ToySolver.Data.Polynomial
peek	ToySolver.Internal.Data.Vec
phaseI
1 (Function)	ToySolver.Arith.Simplex
2 (Function)	ToySolver.Arith.LPSolver
pivot	ToySolver.Arith.Simplex
PivotStrategy	ToySolver.Arith.Simplex2
PivotStrategyBlandRule	ToySolver.Arith.Simplex2
PivotStrategyLargestCoefficient	ToySolver.Arith.Simplex2
pmod	ToySolver.Data.Polynomial
Point
1 (Data Constructor)	ToySolver.Arith.CAD
2 (Type/Class)	ToySolver.Arith.CAD
Polarity
1 (Type/Class)	ToySolver.SAT.TseitinEncoder
2 (Data Constructor)	ToySolver.SAT.TseitinEncoder
polarityBoth	ToySolver.SAT.TseitinEncoder
polarityNeg	ToySolver.SAT.TseitinEncoder
polarityNegOccurs	ToySolver.SAT.TseitinEncoder
polarityNone	ToySolver.SAT.TseitinEncoder
polarityPos	ToySolver.SAT.TseitinEncoder
polarityPosOccurs	ToySolver.SAT.TseitinEncoder
Polynomial	ToySolver.Data.Polynomial
pop
1 (Function)	ToySolver.Internal.Data.Vec
2 (Function)	ToySolver.SMT
popBacktrackPoint
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
3 (Function)	ToySolver.Arith.Simplex2
popMaybe	ToySolver.Internal.Data.Vec
pOptIsNegativeCoeff	ToySolver.Data.Polynomial
pOptMonomialOrder	ToySolver.Data.Polynomial
pOptPrintCoeff	ToySolver.Data.Polynomial
pOptPrintVar	ToySolver.Data.Polynomial
Pos	ToySolver.EUF.FiniteModelFinder
PosInf
1 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Arith.CAD
pp	ToySolver.Data.Polynomial
pPrintCoeff	ToySolver.Data.Polynomial
pPrintVar	ToySolver.Data.Polynomial
PrettyCoeff	ToySolver.Data.Polynomial
prettyPrint	ToySolver.Data.Polynomial
PrettyVar	ToySolver.Data.Polynomial
primalDualSimplex
1 (Function)	ToySolver.Arith.Simplex
2 (Function)	ToySolver.Arith.LPSolver
PrintOptions
1 (Type/Class)	ToySolver.Data.Polynomial
2 (Data Constructor)	ToySolver.Data.Polynomial
PriorityQueue
1 (Type/Class)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Type/Class)	ToySolver.Internal.Data.PriorityQueue
Problem
1 (Type/Class)	ToySolver.Text.SDPFile
2 (Data Constructor)	ToySolver.Text.SDPFile
3 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
4 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
project
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
3 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
4 (Function)	ToySolver.Arith.CAD
project'
1 (Function)	ToySolver.Arith.FourierMotzkin.Base
2 (Function)	ToySolver.Arith.CAD
projectCases
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
projectCasesN
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
projectN
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
3 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
4 (Function)	ToySolver.Arith.CAD
projectN'
1 (Function)	ToySolver.Arith.FourierMotzkin.Base
2 (Function)	ToySolver.Arith.CAD
PSym	ToySolver.EUF.FiniteModelFinder
push
1 (Function)	ToySolver.Internal.Data.Vec
2 (Function)	ToySolver.SMT
pushBacktrackPoint
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
3 (Function)	ToySolver.Arith.Simplex2
pushNot	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
putTableau	ToySolver.Arith.LPSolver
QFFormula
1 (Type/Class)	ToySolver.Arith.VirtualSubstitution
2 (Type/Class)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
QueueSize	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
queueSize	ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.IndexedPriorityQueue, ToySolver.Internal.Data.PriorityQueue
Rat	ToySolver.Arith.FourierMotzkin.Base
RawModel	ToySolver.Arith.Simplex2
read	ToySolver.Internal.Data.Vec
readFile	ToySolver.Data.MIP
readInt	ToySolver.Internal.TextUtil
readIOURef	ToySolver.Internal.Data.IOURef
readLPFile	ToySolver.Data.MIP
readMPSFile	ToySolver.Data.MIP
readUnsignedInteger	ToySolver.Internal.TextUtil
realPart
1 (Function)	ToySolver.Data.Delta
2 (Function)	ToySolver.Data.AlgebraicNumber.Complex
realRoots	ToySolver.Data.AlgebraicNumber.Real
realRootsEx	ToySolver.Data.AlgebraicNumber.Real
reduce	ToySolver.Data.Polynomial
reduceGBasis	ToySolver.Data.Polynomial.GroebnerBasis
refineIsolatingInterval	ToySolver.Data.AlgebraicNumber.Real
RelOp
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Type/Class)	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.Arith.Simplex2
render
1 (Function)	ToySolver.Text.SDPFile
2 (Function)	ToySolver.Text.GurobiSol
3 (Function)	ToySolver.Data.MIP.LPFile
4 (Function)	ToySolver.Data.MIP.MPSFile
renderSparse	ToySolver.Text.SDPFile
resize	ToySolver.Internal.Data.Vec
resizeCapacity	ToySolver.Internal.Data.Vec
resizeHeapCapacity
1 (Function)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Function)	ToySolver.Internal.Data.PriorityQueue
resizeTableCapacity	ToySolver.Internal.Data.IndexedPriorityQueue
resizeVarCapacity	ToySolver.SAT
RestartStrategy	ToySolver.SAT
revForM	ToySolver.Internal.Util
revlex	ToySolver.Data.Polynomial
revMapM	ToySolver.Internal.Util
revSequence	ToySolver.Internal.Util
rootAdd	ToySolver.Data.AlgebraicNumber.Root
rootIndex	ToySolver.Data.AlgebraicNumber.Real
rootMul	ToySolver.Data.AlgebraicNumber.Root
rootNthRoot	ToySolver.Data.AlgebraicNumber.Root
RootOf	ToySolver.Arith.CAD
rootRecip	ToySolver.Data.AlgebraicNumber.Root
rootScale	ToySolver.Data.AlgebraicNumber.Root
rootShift	ToySolver.Data.AlgebraicNumber.Root
rootSimpPoly	ToySolver.Data.AlgebraicNumber.Root
Row	ToySolver.Arith.Simplex
RowIndex	ToySolver.Arith.Simplex
runProcessWithOutputCallback	ToySolver.Internal.ProcessUtil
S1	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
S2	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Sat	ToySolver.Data.FOL.Arith
satPrintModel	ToySolver.SAT.Printer
SatResult	ToySolver.Data.FOL.Arith
sBool	ToySolver.SMT
SearchStrategy	ToySolver.SAT.PBO
SemiContinuousVariable	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
semiContinuousVariables	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
SemiIntegerVariable	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
semiIntegerVariables	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
separate	ToySolver.Data.AlgebraicNumber.Sturm
separate'	ToySolver.Data.AlgebraicNumber.Sturm
SeqQueue	ToySolver.Internal.Data.SeqQueue
Sequent	ToySolver.Wang
setCCMin	ToySolver.SAT
setCheckModel	ToySolver.SAT
setConfBudget	ToySolver.SAT
setConfig	ToySolver.SAT
setEnableBackwardSubsumptionRemoval	ToySolver.SAT
setEnableForwardSubsumptionRemoval	ToySolver.SAT
setEnableObjFunVarsHeuristics	ToySolver.SAT.PBO
setEnablePhaseSaving	ToySolver.SAT
setFinished	ToySolver.SAT.PBO.Context
setGlobalDeclarations	ToySolver.SMT
setLearningStrategy	ToySolver.SAT
setLearntSizeFirst	ToySolver.SAT
setLearntSizeInc	ToySolver.SAT
setLogger
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT
3 (Function)	ToySolver.SAT.PBO
4 (Function)	ToySolver.Arith.Simplex2
5 (Function)	ToySolver.Arith.MIPSolver2
setNThread	ToySolver.Arith.MIPSolver2
setObj
1 (Function)	ToySolver.Converter.PBSetObj
2 (Function)	ToySolver.Arith.Simplex2
setObjFun	ToySolver.Arith.Simplex
setOnUpdateBestSolution
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
3 (Function)	ToySolver.Arith.MIPSolver2
setOnUpdateLowerBound
1 (Function)	ToySolver.SAT.PBO.Context
2 (Function)	ToySolver.SAT.PBO
setOptDir	ToySolver.Arith.Simplex2
setPBHandlerType	ToySolver.SAT
setPBSplitClausePart	ToySolver.SAT
setPivotStrategy	ToySolver.Arith.Simplex2
setRandomFreq	ToySolver.SAT
setRandomGen	ToySolver.SAT
setRestartFirst	ToySolver.SAT
setRestartInc	ToySolver.SAT
setRestartStrategy	ToySolver.SAT
setSearchStrategy	ToySolver.SAT.PBO
setShowRational	ToySolver.Arith.MIPSolver2
setTheory	ToySolver.SAT
setTrialLimitConf	ToySolver.SAT.PBO
setUnsat	ToySolver.SAT.PBO.Context
setUsePB	ToySolver.SAT.TseitinEncoder
setVarPolarity	ToySolver.SAT
showAtom	ToySolver.Data.LA
showEntity	ToySolver.EUF.FiniteModelFinder
showExpr	ToySolver.Data.LA
showModel	ToySolver.EUF.FiniteModelFinder
showOp	ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA
showRational	ToySolver.Internal.Util
showRationalAsFiniteDecimal	ToySolver.Internal.Util
showValue	ToySolver.Arith.Simplex2
simpARealPoly	ToySolver.Data.AlgebraicNumber.Real
SimpleContext	ToySolver.SAT.PBO.Context
simplex
1 (Function)	ToySolver.Arith.Simplex
2 (Function)	ToySolver.Arith.LPSolver
simplify
1 (Function)	ToySolver.Data.BoolExpr
2 (Function)	ToySolver.Arith.FourierMotzkin.Base
simplifyAtom	ToySolver.Arith.Simplex2
SMTLIB2	ToySolver.Converter.MIP2SMT
solve
1 (Function)	ToySolver.SAT
2 (Function)	ToySolver.SAT.PBO.BC
3 (Function)	ToySolver.SAT.PBO.BCD
4 (Function)	ToySolver.SAT.PBO.BCD2
5 (Function)	ToySolver.SAT.PBO.MSU4
6 (Function)	ToySolver.SAT.PBO.UnsatBased
7 (Function)	ToySolver.Combinatorial.Knapsack.DPSparse
8 (Function)	ToySolver.Combinatorial.Knapsack.DPDense
9 (Function)	ToySolver.Combinatorial.Knapsack.BB
10 (Function)	ToySolver.Arith.VirtualSubstitution
11 (Function)	ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
12 (Function)	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
13 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
14 (Function)	ToySolver.Arith.CAD
15 (Function)	ToySolver.Arith.LPSolverHL
16 (Function)	ToySolver.Arith.ContiTraverso
solve'
1 (Function)	ToySolver.Arith.FourierMotzkin.Base
2 (Function)	ToySolver.Arith.CAD
3 (Function)	ToySolver.Arith.ContiTraverso
solveFor	ToySolver.Data.LA
solveFormula
1 (Function)	ToySolver.Arith.FourierMotzkin.FOL, ToySolver.Arith.FourierMotzkin
2 (Function)	ToySolver.Arith.Cooper.FOL, ToySolver.Arith.Cooper
solveGeneric	ToySolver.Combinatorial.Knapsack.DPSparse
solveInt	ToySolver.Combinatorial.Knapsack.DPSparse
solveInteger	ToySolver.Combinatorial.Knapsack.DPSparse
solveQFFormula
1 (Function)	ToySolver.Arith.VirtualSubstitution
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
solveQFLIRAConj
1 (Function)	ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
2 (Function)	ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
Solver
1 (Type/Class)	ToySolver.EUF.CongruenceClosure
2 (Type/Class)	ToySolver.EUF.EUFSolver
3 (Type/Class)	ToySolver.SAT
4 (Type/Class)	ToySolver.Arith.Simplex2
5 (Type/Class)	ToySolver.SMT
6 (Type/Class)	ToySolver.Arith.MIPSolver2
7 (Type/Class)	ToySolver.Arith.LPSolver
SolverValue	ToySolver.Arith.Simplex2
solveWith	ToySolver.SAT
Sort
1 (Type/Class)	ToySolver.SMT
2 (Data Constructor)	ToySolver.SMT
sosBody	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
SOSConstraint
1 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
2 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
sosConstraints	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
sosLabel	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
SOSType	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
sosType	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
spolynomial	ToySolver.Data.Polynomial.GroebnerBasis
SQFree	ToySolver.Data.Polynomial
sqfree
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.Polynomial.Factorization.FiniteField
sqfreeChar0	ToySolver.Data.Polynomial.Factorization.SquareFree
sReal	ToySolver.SMT
SS	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
SSym	ToySolver.SMT
ssymArity	ToySolver.SMT
SSymBool	ToySolver.SMT
SSymReal	ToySolver.SMT
SSymUserDeclared	ToySolver.SMT
Strategy	ToySolver.Data.Polynomial.GroebnerBasis
SturmChain	ToySolver.Data.AlgebraicNumber.Sturm
sturmChain	ToySolver.Data.AlgebraicNumber.Sturm
subsetSum	ToySolver.Combinatorial.SubsetSum
subst	ToySolver.Data.Polynomial
SugarStrategy	ToySolver.Data.Polynomial.GroebnerBasis
T
1 (Data Constructor)	ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.EUF.FiniteModelFinder
Tableau	ToySolver.Arith.Simplex
tableau	ToySolver.Arith.LPSolver
TApp	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
tdeg	ToySolver.Data.Polynomial
tderiv	ToySolver.Data.Polynomial
tdiv	ToySolver.Data.Polynomial
tdivides	ToySolver.Data.Polynomial
Term
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.Data.Polynomial
3 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
4 (Data Constructor)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
5 (Type/Class)	ToySolver.EUF.FiniteModelFinder
terms
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
3 (Function)	ToySolver.Data.LA
termToFlatTerm
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
termToFSym
1 (Function)	ToySolver.EUF.CongruenceClosure
2 (Function)	ToySolver.EUF.EUFSolver
thAssertLit	ToySolver.SAT.TheorySolver
thCheck	ToySolver.SAT.TheorySolver
thConstructModel	ToySolver.SAT.TheorySolver
TheorySolver
1 (Type/Class)	ToySolver.SAT.TheorySolver
2 (Data Constructor)	ToySolver.SAT.TheorySolver
thExplain	ToySolver.SAT.TheorySolver
thPopBacktrackPoint	ToySolver.SAT.TheorySolver
thPushBacktrackPoint	ToySolver.SAT.TheorySolver
tintegral	ToySolver.Data.Polynomial
TmApp	ToySolver.EUF.FiniteModelFinder
tmult	ToySolver.Data.Polynomial
TmVar	ToySolver.EUF.FiniteModelFinder
toCSV	ToySolver.Arith.Simplex
toFOLExpr	ToySolver.Data.LA.FOL
toFOLFormula	ToySolver.Data.LA.FOL
toLAAtom	ToySolver.Arith.FourierMotzkin.Base
toLPString	ToySolver.Data.MIP
toMonic	ToySolver.Data.Polynomial
toMPSString	ToySolver.Data.MIP
topCost	ToySolver.Text.MaxSAT
toRat	ToySolver.Arith.FourierMotzkin.Base
toSkolemNF	ToySolver.EUF.FiniteModelFinder
toStandardForm	ToySolver.Arith.LPUtil
toStandardForm'	ToySolver.Arith.LPUtil
toUPolynomialOf	ToySolver.Data.Polynomial
toValue	ToySolver.Arith.Simplex2
toVar	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
true	ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith
tscale	ToySolver.Data.Polynomial
twoPhaseSimplex	ToySolver.Arith.LPSolver
UMonomial	ToySolver.Data.Polynomial
Unbounded
1 (Data Constructor)	ToySolver.Arith.Simplex2
2 (Data Constructor)	ToySolver.Arith.LPSolver
3 (Data Constructor)	ToySolver.Arith.LPSolverHL, ToySolver.Arith.MIPSolverHL
unDNF	ToySolver.Data.DNF
unitVar	ToySolver.Data.LA
Unknown	ToySolver.Data.FOL.Arith
unliftBool	ToySolver.Data.LBool
unsafeModify	ToySolver.Internal.Data.Vec
unsafeModify'	ToySolver.Internal.Data.Vec
unsafePeek	ToySolver.Internal.Data.Vec
unsafePop	ToySolver.Internal.Data.Vec
unsafeRead	ToySolver.Internal.Data.Vec
unsafeWrite	ToySolver.Internal.Data.Vec
Unsat
1 (Data Constructor)	ToySolver.Data.FOL.Arith
2 (Data Constructor)	ToySolver.Arith.Simplex2
3 (Data Constructor)	ToySolver.Arith.LPSolver
UnsatBased	ToySolver.SAT.PBO
Unsupported	ToySolver.SMT
update	ToySolver.Internal.Data.IndexedPriorityQueue
UPolynomial	ToySolver.Data.Polynomial
US	ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.QuickXplain, ToySolver.SAT.MUS.CAMUS, ToySolver.SAT.MUS.DAA
userCuts	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
UTerm	ToySolver.Data.Polynomial
UVec	ToySolver.Internal.Data.Vec
VAFun
1 (Type/Class)	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
2 (Type/Class)	ToySolver.SMT
ValBool	ToySolver.SMT
validLit	ToySolver.SAT.Types
validVar	ToySolver.SAT.Types
ValRational	ToySolver.SMT
valSort	ToySolver.SMT
Value
1 (Type/Class)	ToySolver.Internal.Data.IndexedPriorityQueue
2 (Type/Class)	ToySolver.Combinatorial.Knapsack.DPDense
3 (Type/Class)	ToySolver.Combinatorial.Knapsack.BB
4 (Type/Class)	ToySolver.SMT
ValUninterpreted	ToySolver.SMT
Var
1 (Type/Class)	ToySolver.Data.Var, ToySolver.Data.LA
2 (Type/Class)	ToySolver.Data.Polynomial
3 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
4 (Data Constructor)	ToySolver.Data.FOL.Arith
5 (Type/Class)	ToySolver.Data.AlgebraicNumber.Root
6 (Type/Class)	ToySolver.SAT.Types, ToySolver.SAT
7 (Type/Class)	ToySolver.EUF.FiniteModelFinder
8 (Type/Class)	ToySolver.Arith.Simplex2
var
1 (Function)	ToySolver.Data.Polynomial
2 (Function)	ToySolver.Data.FOL.Arith
3 (Function)	ToySolver.Data.LA
varBounds	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
varBumpActivity	ToySolver.SAT
varDecayActivity	ToySolver.SAT
varExpr	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
Variables
1 (Type/Class)	ToySolver.Data.Var
2 (Type/Class)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
variables	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
VarMap
1 (Type/Class)	ToySolver.Data.Var
2 (Type/Class)	ToySolver.SAT.Types
Vars	ToySolver.Data.Polynomial
vars
1 (Function)	ToySolver.Data.Var
2 (Function)	ToySolver.Data.Polynomial
3 (Function)	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
VarSet
1 (Type/Class)	ToySolver.Data.Var
2 (Type/Class)	ToySolver.SAT.Types
VarType	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
varType	ToySolver.Data.MIP.Base, ToySolver.Data.MIP
VASortFun	ToySolver.SMT
Vec	ToySolver.Internal.Data.Vec
version	ToySolver.Version
WCNF
1 (Type/Class)	ToySolver.Text.MaxSAT
2 (Data Constructor)	ToySolver.Text.MaxSAT
Weight
1 (Type/Class)	ToySolver.Combinatorial.SubsetSum
2 (Type/Class)	ToySolver.Text.MaxSAT
3 (Type/Class)	ToySolver.Combinatorial.Knapsack.DPDense
4 (Type/Class)	ToySolver.Combinatorial.Knapsack.BB
WeightedClause	ToySolver.Text.MaxSAT
withVArgs	ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver
write	ToySolver.Internal.Data.Vec
writeFile	ToySolver.Data.MIP
writeIOURef	ToySolver.Internal.Data.IOURef
writeLPFile	ToySolver.Data.MIP
writeMPSFile	ToySolver.Data.MIP
X
1 (Type/Class)	ToySolver.Data.Polynomial
2 (Data Constructor)	ToySolver.Data.Polynomial
XORClause	ToySolver.SAT.Types, ToySolver.SAT
YICES	ToySolver.Converter.MIP2SMT
Yices1	ToySolver.Converter.MIP2SMT
Yices2	ToySolver.Converter.MIP2SMT
YicesVersion	ToySolver.Converter.MIP2SMT
zassenhaus	ToySolver.Data.Polynomial.Factorization.Zassenhaus
zmod	ToySolver.Arith.OmegaTest.Base