.&&. | ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
./=. | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector |
.<. | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
.<=. | |
1 (Function) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
2 (Function) | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
.<=>. | 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.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
.=>. | ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
.>. | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
.>=. | |
1 (Function) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
2 (Function) | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
.|. | 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.Arith.DifferenceLogic |
:/: | ToySolver.Data.FOL.Arith |
:<= | ToySolver.Arith.DifferenceLogic |
A | ToySolver.Text.QDimacs, ToySolver.QBF |
AComplex | ToySolver.Data.AlgebraicNumber.Complex |
AdaptiveSearch | ToySolver.SAT.PBO |
addAtLeast | ToySolver.SAT.Types, ToySolver.SAT |
addAtMost | ToySolver.SAT.Types, ToySolver.SAT |
AddCardinality | ToySolver.SAT.Types, ToySolver.SAT |
AddClause | ToySolver.SAT.Types, ToySolver.SAT |
addClause | ToySolver.SAT.Types, ToySolver.SAT |
addConstraint | |
1 (Function) | ToySolver.SAT.Encoder.Integer |
2 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
addConstraintSoft | ToySolver.SAT.Encoder.Integer |
addConstraintWithArtificialVariable | ToySolver.Arith.Simplex.Textbook.LPSolver |
Adder | ToySolver.SAT.Encoder.PB |
addExactly | ToySolver.SAT.Types, ToySolver.SAT |
addFormula | ToySolver.SAT.Encoder.Tseitin |
addLowerBound | ToySolver.SAT.PBO.Context |
addMIP | ToySolver.Converter.MIP2PB |
addPBAtLeast | ToySolver.SAT.Types, ToySolver.SAT |
addPBAtLeastSoft | ToySolver.SAT.Types, ToySolver.SAT |
addPBAtMost | ToySolver.SAT.Types, ToySolver.SAT |
addPBAtMostSoft | ToySolver.SAT.Types, ToySolver.SAT |
addPBExactly | ToySolver.SAT.Types, ToySolver.SAT |
addPBExactlySoft | ToySolver.SAT.Types, ToySolver.SAT |
AddPBLin | ToySolver.SAT.Types, ToySolver.SAT |
addPBLinAtLeastAdder | ToySolver.SAT.Encoder.PB.Internal.Adder |
addPBLinAtLeastBDD | ToySolver.SAT.Encoder.PB.Internal.BDD |
addPBLinAtLeastSorter | ToySolver.SAT.Encoder.PB.Internal.Sorter |
AddPBNL | ToySolver.SAT.Types |
addPBNLAtLeast | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addPBNLAtLeastSoft | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addPBNLAtMost | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addPBNLAtMostSoft | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addPBNLExactly | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addPBNLExactlySoft | ToySolver.SAT.Types, ToySolver.SAT.Encoder.PBNLC |
addRow | ToySolver.Arith.Simplex.Textbook |
addSolution | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
addWBO | ToySolver.Converter.WBO2PB |
AddXORClause | ToySolver.SAT.Types, ToySolver.SAT |
addXORClause | ToySolver.SAT.Types, ToySolver.SAT |
addXORClauseSoft | ToySolver.SAT.Types, ToySolver.SAT |
allMUSAssumptions | ToySolver.SAT.MUS.Enum |
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 |
Append | ToySolver.Graph.ShortestPath |
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.Config, ToySolver.SAT |
asConst | ToySolver.Data.LA |
assert | ToySolver.SMT |
assertAtom | |
1 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
2 (Function) | ToySolver.Arith.Simplex |
assertAtom' | ToySolver.Arith.Simplex |
assertAtomEx | ToySolver.Arith.Simplex |
assertAtomEx' | ToySolver.Arith.Simplex |
assertEqual | ToySolver.EUF.EUFSolver |
assertEqual' | ToySolver.EUF.EUFSolver |
assertLower | ToySolver.Arith.Simplex |
assertLower' | ToySolver.Arith.Simplex |
assertNamed | ToySolver.SMT |
assertNotEqual | ToySolver.EUF.EUFSolver |
assertNotEqual' | ToySolver.EUF.EUFSolver |
assertUpper | ToySolver.Arith.Simplex |
assertUpper' | ToySolver.Arith.Simplex |
AtLeast | ToySolver.SAT.Types, ToySolver.SAT |
Atom | |
1 (Type/Class) | ToySolver.Text.QDimacs |
2 (Data Constructor) | ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
3 (Type/Class) | ToySolver.Data.FOL.Arith |
4 (Type/Class) | ToySolver.Data.LA, ToySolver.Arith.Simplex |
5 (Data Constructor) | ToySolver.Data.BoolExpr |
6 (Data Constructor) | ToySolver.EUF.FiniteModelFinder |
7 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
8 (Type/Class) | ToySolver.BitVector.Base, ToySolver.BitVector |
Base | ToySolver.SAT.Encoder.PB.Internal.Sorter |
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 |
BDD | ToySolver.SAT.Encoder.PB |
bellmanFord | ToySolver.Graph.ShortestPath |
bellmanFordDetectNegativeCycle | ToySolver.Graph.ShortestPath |
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.Simplex |
boundExplanation | ToySolver.Arith.Simplex |
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.Simplex |
BranchingERWA | ToySolver.SAT.Config, ToySolver.SAT |
BranchingLRB | ToySolver.SAT.Config, ToySolver.SAT |
BranchingStrategy | ToySolver.SAT.Config, ToySolver.SAT |
BranchingVSIDS | ToySolver.SAT.Config, ToySolver.SAT |
BudgetExceeded | |
1 (Type/Class) | ToySolver.SAT |
2 (Data Constructor) | ToySolver.SAT |
BV | ToySolver.BitVector.Base, ToySolver.BitVector |
bv2nat | ToySolver.BitVector.Base, ToySolver.BitVector |
bvadd | ToySolver.BitVector.Base, ToySolver.BitVector |
bvand | ToySolver.BitVector.Base, ToySolver.BitVector |
bvashr | ToySolver.BitVector.Base, ToySolver.BitVector |
bvcomp | ToySolver.BitVector.Base, ToySolver.BitVector |
BVComparison | ToySolver.BitVector.Base, ToySolver.BitVector |
bvlshr | ToySolver.BitVector.Base, ToySolver.BitVector |
bvmul | ToySolver.BitVector.Base, ToySolver.BitVector |
bvnand | ToySolver.BitVector.Base, ToySolver.BitVector |
bvneg | ToySolver.BitVector.Base, ToySolver.BitVector |
bvnor | ToySolver.BitVector.Base, ToySolver.BitVector |
bvnot | ToySolver.BitVector.Base, ToySolver.BitVector |
bvor | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsdiv | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsge | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsgt | ToySolver.BitVector.Base, ToySolver.BitVector |
bvshl | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsle | ToySolver.BitVector.Base, ToySolver.BitVector |
bvslt | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsmod | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsrem | ToySolver.BitVector.Base, ToySolver.BitVector |
bvsub | ToySolver.BitVector.Base, ToySolver.BitVector |
bvudiv | ToySolver.BitVector.Base, ToySolver.BitVector |
bvuge | ToySolver.BitVector.Base, ToySolver.BitVector |
bvugt | ToySolver.BitVector.Base, ToySolver.BitVector |
bvule | ToySolver.BitVector.Base, ToySolver.BitVector |
bvult | ToySolver.BitVector.Base, ToySolver.BitVector |
bvurem | ToySolver.BitVector.Base, ToySolver.BitVector |
bvxnor | ToySolver.BitVector.Base, ToySolver.BitVector |
bvxor | ToySolver.BitVector.Base, ToySolver.BitVector |
cabook_proposition_5_10 | ToySolver.Data.Polynomial.Factorization.Hensel.Internal |
cabook_proposition_5_11 | ToySolver.Data.Polynomial.Factorization.Hensel.Internal |
CAMUS | ToySolver.SAT.MUS.Enum |
cancel | ToySolver.SAT |
Canceled | |
1 (Type/Class) | ToySolver.SAT |
2 (Data Constructor) | ToySolver.SAT |
cardinalityReduction | ToySolver.SAT.Types |
CBC | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.CBC, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.CBC, ToySolver.Data.MIP.Solver |
cbc | ToySolver.Data.MIP.Solver.CBC, ToySolver.Data.MIP.Solver |
cbcPath | ToySolver.Data.MIP.Solver.CBC, ToySolver.Data.MIP.Solver |
ceiling' | ToySolver.Data.Delta |
Cell | ToySolver.Arith.CAD |
check | |
1 (Function) | ToySolver.EUF.EUFSolver |
2 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
3 (Function) | ToySolver.Arith.Simplex |
4 (Function) | ToySolver.Arith.Simplex.Simple |
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.Text.QDimacs |
2 (Type/Class) | ToySolver.SAT.Types, ToySolver.SAT |
3 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
clauses | |
1 (Function) | ToySolver.Text.CNF |
2 (Function) | ToySolver.Text.GCNF |
3 (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.Simplex |
clone | |
1 (Function) | ToySolver.Internal.Data.Vec |
2 (Function) | ToySolver.Internal.Data.IndexedPriorityQueue |
3 (Function) | ToySolver.Internal.Data.PriorityQueue |
cloneSolver | ToySolver.Arith.Simplex |
CNF | |
1 (Type/Class) | ToySolver.Text.CNF |
2 (Data Constructor) | ToySolver.Text.CNF |
cnfBuilder | ToySolver.Text.CNF |
CNFStore | ToySolver.SAT.Store.CNF |
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.Textbook |
collectBounds | ToySolver.Arith.FourierMotzkin.Base |
collectNonnegVars | ToySolver.Arith.Simplex.Textbook.LPSolver |
combineMaybe | ToySolver.Internal.Util |
ComparisonResult | ToySolver.BitVector.Base, ToySolver.BitVector |
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.Config, ToySolver.SAT |
2 (Data Constructor) | ToySolver.SAT.Config, ToySolver.SAT |
configBranchingStrategy | ToySolver.SAT.Config, ToySolver.SAT |
configCCMin | ToySolver.SAT.Config, ToySolver.SAT |
configCheckModel | ToySolver.SAT.Config, ToySolver.SAT |
configConstrDecay | ToySolver.SAT.Config, ToySolver.SAT |
configEMADecay | ToySolver.SAT.Config, ToySolver.SAT |
configEnableBackwardSubsumptionRemoval | ToySolver.SAT.Config, ToySolver.SAT |
configEnableForwardSubsumptionRemoval | ToySolver.SAT.Config, ToySolver.SAT |
configEnablePBSplitClausePart | ToySolver.SAT.Config, ToySolver.SAT |
configEnablePhaseSaving | ToySolver.SAT.Config, ToySolver.SAT |
configERWAStepSizeDec | ToySolver.SAT.Config, ToySolver.SAT |
configERWAStepSizeFirst | ToySolver.SAT.Config, ToySolver.SAT |
configERWAStepSizeMin | ToySolver.SAT.Config, ToySolver.SAT |
configLearningStrategy | ToySolver.SAT.Config, ToySolver.SAT |
configLearntSizeFirst | ToySolver.SAT.Config, ToySolver.SAT |
configLearntSizeInc | ToySolver.SAT.Config, ToySolver.SAT |
configPBHandlerType | ToySolver.SAT.Config, ToySolver.SAT |
configRandomFreq | ToySolver.SAT.Config, ToySolver.SAT |
configRestartFirst | ToySolver.SAT.Config, ToySolver.SAT |
configRestartInc | ToySolver.SAT.Config, ToySolver.SAT |
configRestartStrategy | ToySolver.SAT.Config, ToySolver.SAT |
configVarDecay | ToySolver.SAT.Config, 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.Simplex |
ConstrIDSet | ToySolver.Arith.Simplex |
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.PB2WBO |
2 (Function) | ToySolver.Converter.PB2SMP |
3 (Function) | ToySolver.Converter.PB2LSP |
4 (Function) | ToySolver.Converter.MIP2SMT |
5 (Function) | ToySolver.Converter.PB2IP |
6 (Function) | ToySolver.Converter.MIP2PB |
7 (Function) | ToySolver.Converter.WBO2PB |
8 (Function) | ToySolver.Converter.SAT2PB |
9 (Function) | ToySolver.Converter.SAT2IP |
10 (Function) | ToySolver.Converter.PB2SAT |
11 (Function) | ToySolver.Converter.SAT2KSAT |
12 (Function) | ToySolver.Converter.GCNF2MaxSAT |
13 (Function) | ToySolver.Converter.MaxSAT2WBO |
14 (Function) | ToySolver.Converter.MaxSAT2IP |
15 (Function) | ToySolver.Converter.WBO2MaxSAT |
convertWBO | |
1 (Function) | ToySolver.Converter.PB2LSP |
2 (Function) | ToySolver.Converter.PB2IP |
Cost | ToySolver.SAT.Encoder.PB.Internal.Sorter |
costs | ToySolver.Text.SDPFile |
CPLEX | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.CPLEX, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.CPLEX, ToySolver.Data.MIP.Solver |
cplex | ToySolver.Data.MIP.Solver.CPLEX, ToySolver.Data.MIP.Solver |
cplexPath | ToySolver.Data.MIP.Solver.CPLEX, ToySolver.Data.MIP.Solver |
CS | ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.Enum |
currentObjValue | ToySolver.Arith.Simplex.Textbook |
currentValue | ToySolver.Arith.Simplex.Textbook |
cutResolve | ToySolver.SAT.Types |
DAA | ToySolver.SAT.MUS.Enum |
declareConst | ToySolver.SMT |
declareFSym | ToySolver.SMT |
declareFun | ToySolver.SMT |
declareSort | ToySolver.SMT |
declareSSym | ToySolver.SMT |
decode | ToySolver.SAT.Encoder.PB.Internal.Sorter |
def | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
Default | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
defaultBounds | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
defaultCCMin | ToySolver.SAT.Config, ToySolver.SAT |
defaultEnableBackwardSubsumptionRemoval | ToySolver.SAT.Config, ToySolver.SAT |
defaultEnableForwardSubsumptionRemoval | ToySolver.SAT.Config, ToySolver.SAT |
defaultEnableObjFunVarsHeuristics | ToySolver.SAT.PBO |
defaultEnablePhaseSaving | ToySolver.SAT.Config, ToySolver.SAT |
defaultGrow | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
defaultLB | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
defaultLearntSizeFirst | ToySolver.SAT.Config, ToySolver.SAT |
defaultLearntSizeInc | ToySolver.SAT.Config, ToySolver.SAT |
defaultMaximalInterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
defaultMinimalUninterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
defaultMinimalUninterestingSetOrMaximalInterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
defaultPBSplitClausePart | ToySolver.SAT.Config, ToySolver.SAT |
defaultRandomFreq | ToySolver.SAT.Config, ToySolver.SAT |
defaultRestartFirst | ToySolver.SAT.Config, ToySolver.SAT |
defaultRestartInc | ToySolver.SAT.Config, ToySolver.SAT |
defaultShrink | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
defaultTrialLimitConf | ToySolver.SAT.PBO |
defaultUB | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
define | ToySolver.Arith.Simplex.Textbook.LPSolver |
deg | ToySolver.Data.Polynomial |
Degree | ToySolver.Data.Polynomial |
deleteRedundancy | ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 |
deleteSolver | ToySolver.SAT.MessagePassing.SurveyPropagation |
Deletion | ToySolver.SAT.MUS |
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 |
Diff | ToySolver.Arith.DifferenceLogic |
dijkstra | ToySolver.Graph.ShortestPath |
disableTimeRecording | ToySolver.Arith.Simplex |
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.Simplex.Textbook |
2 (Function) | ToySolver.Arith.Simplex |
3 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
dump | ToySolver.Arith.Simplex |
E | ToySolver.Text.QDimacs, ToySolver.QBF |
EAp | ToySolver.SMT |
EConst | ToySolver.BitVector.Base, ToySolver.BitVector |
Edge | ToySolver.Graph.ShortestPath |
eisensteinsCriterion | ToySolver.Data.Polynomial |
eliminateQuantifiers | |
1 (Function) | ToySolver.Arith.FourierMotzkin.FOL, ToySolver.Arith.FourierMotzkin |
2 (Function) | ToySolver.Arith.Cooper.FOL, ToySolver.Arith.Cooper |
eliminateQuantifiers' | ToySolver.Arith.FourierMotzkin.FOL |
Empty | ToySolver.Graph.ShortestPath |
emptySolver | ToySolver.Arith.Simplex.Textbook.LPSolver |
emptyTableau | ToySolver.Arith.Simplex.Textbook |
emptyTheory | ToySolver.SAT.TheorySolver |
enableTimeRecording | ToySolver.Arith.Simplex |
encode | ToySolver.SAT.Encoder.PB.Internal.Sorter |
encodeConj | ToySolver.SAT.Encoder.Tseitin |
encodeConjWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodeDisj | ToySolver.SAT.Encoder.Tseitin |
encodeDisjWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodeFACarry | ToySolver.SAT.Encoder.Tseitin |
encodeFACarryWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodeFASum | ToySolver.SAT.Encoder.Tseitin |
encodeFASumWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodeFormula | ToySolver.SAT.Encoder.Tseitin |
encodeFormulaWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodeITE | ToySolver.SAT.Encoder.Tseitin |
encodeITEWithPolarity | ToySolver.SAT.Encoder.Tseitin |
encodePBLinAtLeast | ToySolver.SAT.Encoder.PB |
encodePBLinAtLeastAdder | ToySolver.SAT.Encoder.PB.Internal.Adder |
encodePBLinAtLeastBDD | ToySolver.SAT.Encoder.PB.Internal.BDD |
encodePBLinAtLeastSorter | ToySolver.SAT.Encoder.PB.Internal.Sorter |
Encoder | |
1 (Type/Class) | ToySolver.SAT.Encoder.Tseitin |
2 (Type/Class) | ToySolver.SAT.Encoder.PB |
3 (Type/Class) | ToySolver.SAT.Encoder.PBNLC |
encodeXOR | ToySolver.SAT.Encoder.Tseitin |
encodeXORWithPolarity | ToySolver.SAT.Encoder.Tseitin |
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 |
enumMinimalHittingSets | |
1 (Function) | ToySolver.Combinatorial.HittingSet.Simple |
2 (Function) | ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 |
EOp1 | ToySolver.BitVector.Base, ToySolver.BitVector |
EOp2 | ToySolver.BitVector.Base, ToySolver.BitVector |
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.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
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 | ToySolver.Data.IntVar, ToySolver.Data.LA, ToySolver.Arith.VirtualSubstitution, ToySolver.Arith.Cooper.Base |
eval | |
1 (Function) | ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
2 (Function) | ToySolver.Data.Polynomial |
3 (Function) | ToySolver.Data.IntVar, ToySolver.Data.LA, ToySolver.Arith.VirtualSubstitution, ToySolver.Arith.Cooper.Base |
4 (Function) | ToySolver.SAT.Encoder.Integer |
5 (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 |
4 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
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 |
3 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
evalFormula | |
1 (Function) | ToySolver.SAT.Encoder.Tseitin |
2 (Function) | ToySolver.EUF.FiniteModelFinder |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
evalPBConstraint | ToySolver.SAT.Types |
evalPBLinAtLeast | ToySolver.SAT.Types, ToySolver.SAT |
evalPBLinExactly | ToySolver.SAT.Types, ToySolver.SAT |
evalPBLinSum | ToySolver.SAT.Types, ToySolver.SAT |
evalPBSum | ToySolver.SAT.Types |
evalPoint | ToySolver.Arith.CAD |
evalQFFormula | |
1 (Function) | ToySolver.Arith.VirtualSubstitution |
2 (Function) | ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper |
evalTerm | ToySolver.EUF.FiniteModelFinder |
EValue | ToySolver.SMT |
evalVar | ToySolver.SAT.Types, ToySolver.SAT |
evalXORClause | ToySolver.SAT.Types, ToySolver.SAT |
EVar | ToySolver.BitVector.Base, ToySolver.BitVector |
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.BitVector.Solver, ToySolver.BitVector |
4 (Function) | ToySolver.Arith.Simplex |
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.Encoder.Integer |
6 (Data Constructor) | ToySolver.SAT.Encoder.Integer |
7 (Type/Class) | ToySolver.BitVector.Base, ToySolver.BitVector |
8 (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 | |
1 (Function) | ToySolver.Data.LA |
2 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
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 |
FancyError | ToySolver.Data.MIP |
FileOptions | |
1 (Type/Class) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
2 (Data Constructor) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
findModel | ToySolver.EUF.FiniteModelFinder |
findMUSAssumptions | ToySolver.SAT.MUS |
findPoly | ToySolver.Data.AlgebraicNumber.Root |
findPrimeImplicateOrPrimeImplicant | ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 |
findSample | ToySolver.Arith.CAD |
Finite | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
firstOutEdge | ToySolver.Graph.ShortestPath |
fixLit | ToySolver.SAT.MessagePassing.SurveyPropagation |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
floor' | ToySolver.Data.Delta |
floydWarshall | ToySolver.Graph.ShortestPath |
Fold | |
1 (Type/Class) | ToySolver.Graph.ShortestPath |
2 (Data Constructor) | ToySolver.Graph.ShortestPath |
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.SAT.Encoder.Tseitin |
4 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
fracPart | ToySolver.Internal.Util |
fromAscBits | ToySolver.BitVector.Base, ToySolver.BitVector |
fromBV | ToySolver.BitVector.Base, ToySolver.BitVector |
fromCoeffMap | |
1 (Function) | ToySolver.Data.Polynomial |
2 (Function) | ToySolver.Data.LA |
fromDescBits | ToySolver.BitVector.Base, ToySolver.BitVector |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
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 |
4 (Data Constructor) | 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 |
gcnfBuilder | 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.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
generateCNFAndDNF | |
1 (Function) | ToySolver.Combinatorial.HittingSet.MARCO |
2 (Function) | ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 |
3 (Function) | ToySolver.Combinatorial.HittingSet.DAA |
GenericSolver | ToySolver.Arith.Simplex |
GenericSolverM | ToySolver.Arith.Simplex |
GenericVec | ToySolver.Internal.Data.Vec |
GenFormula | ToySolver.EUF.FiniteModelFinder |
GenLit | ToySolver.EUF.FiniteModelFinder |
genSorterCircuit | ToySolver.SAT.Encoder.PB.Internal.Sorter |
getArray | ToySolver.Internal.Data.Vec |
getAssumptionsImplications | ToySolver.SAT |
getBestModel | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.Arith.MIP |
getBestSolution | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.Arith.MIP |
getBestValue | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.Arith.MIP |
getBounds | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
getCapacity | ToySolver.Internal.Data.Vec |
getCNFFormula | ToySolver.SAT.Store.CNF |
getCoeff | ToySolver.Arith.Simplex |
getCol | ToySolver.Arith.Simplex |
getConfig | ToySolver.SAT |
getDefinitions | ToySolver.SAT.Encoder.Tseitin |
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 |
getIterationLimit | ToySolver.SAT.MessagePassing.SurveyPropagation |
getLB | ToySolver.Arith.Simplex |
getLitFixed | ToySolver.SAT |
getLowerBound | ToySolver.SAT.PBO.Context |
getMethod | ToySolver.SAT.PBO |
getModel | |
1 (Function) | ToySolver.EUF.CongruenceClosure |
2 (Function) | ToySolver.EUF.EUFSolver |
3 (Function) | ToySolver.SAT |
4 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
5 (Function) | ToySolver.Arith.Simplex |
6 (Function) | ToySolver.SMT |
7 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
getNConstraints | |
1 (Function) | ToySolver.SAT.MessagePassing.SurveyPropagation |
2 (Function) | ToySolver.SAT |
getNLearntConstraints | ToySolver.SAT |
getNThreads | ToySolver.SAT.MessagePassing.SurveyPropagation |
getNVars | |
1 (Function) | ToySolver.SAT.MessagePassing.SurveyPropagation |
2 (Function) | ToySolver.SAT |
getObj | ToySolver.Arith.Simplex |
getObjectiveFunction | ToySolver.SAT.PBO.Context |
getObjValue | ToySolver.Arith.Simplex |
getOptDir | ToySolver.Arith.Simplex |
getPBFormula | ToySolver.SAT.Store.PB |
getPBSplitClausePart | ToySolver.SAT |
getRandomGen | ToySolver.SAT |
getRawModel | ToySolver.Arith.Simplex |
getRow | ToySolver.Arith.Simplex |
getSearchUpperBound | ToySolver.SAT.PBO.Context |
getSize | ToySolver.Internal.Data.Vec |
getTableau | |
1 (Function) | ToySolver.Arith.Simplex |
2 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
getTolerance | ToySolver.SAT.MessagePassing.SurveyPropagation |
getTrialLimitConf | ToySolver.SAT.PBO |
getTseitinEncoder | ToySolver.SAT.Encoder.PBNLC |
getUB | ToySolver.Arith.Simplex |
getUnsatAssumptions | ToySolver.SMT |
getUnsatCore | ToySolver.SMT |
getValue | ToySolver.Arith.Simplex |
getVarFixed | ToySolver.SAT |
getVarProb | ToySolver.SAT.MessagePassing.SurveyPropagation |
getVarType | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
gitHash | ToySolver.Version |
Glpsol | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.Glpsol, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.Glpsol, ToySolver.Data.MIP.Solver |
glpsol | ToySolver.Data.MIP.Solver.Glpsol, ToySolver.Data.MIP.Solver |
glpsolPath | ToySolver.Data.MIP.Solver.Glpsol, ToySolver.Data.MIP.Solver |
goldenRatio | ToySolver.Data.AlgebraicNumber.Real |
Graph | ToySolver.Graph.ShortestPath |
grevlex | ToySolver.Data.Polynomial |
grlex | ToySolver.Data.Polynomial |
GroupIndex | ToySolver.Text.GCNF |
grow | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
growTo | ToySolver.Internal.Data.Vec |
Gt | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
GurobiCl | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.GurobiCl, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.GurobiCl, ToySolver.Data.MIP.Solver |
gurobiCl | ToySolver.Data.MIP.Solver.GurobiCl, ToySolver.Data.MIP.Solver |
gurobiClPath | ToySolver.Data.MIP.Solver.GurobiCl, ToySolver.Data.MIP.Solver |
GurvichKhachiyan1999 | ToySolver.SAT.MUS.Enum |
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 |
hPutCNF | ToySolver.Text.CNF |
hPutGCNF | ToySolver.Text.GCNF |
hPutWCNF | ToySolver.Text.MaxSAT |
Hybrid | ToySolver.SAT.Encoder.PB |
IfThenElse | ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
imagPart | ToySolver.Data.AlgebraicNumber.Complex |
IModel | ToySolver.SAT.Types, ToySolver.SAT |
Implicant | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
Implicate | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
ImplicateOrImplicant | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
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 |
4 (Type/Class) | ToySolver.SMT |
IndexNumeral | ToySolver.SMT |
IndexSymbol | ToySolver.SMT |
InEdge | ToySolver.Graph.ShortestPath |
inferBounds | ToySolver.Arith.BoundsInference |
initializeRandom | ToySolver.SAT.MessagePassing.SurveyPropagation |
initializeRandomDirichlet | ToySolver.SAT.MessagePassing.SurveyPropagation |
Insertion | ToySolver.SAT.MUS |
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 |
InterestingOrUninterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
InterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
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.Simplex |
IsBV | ToySolver.BitVector.Base, ToySolver.BitVector |
isCounterExampleOf | ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 |
IsEqRel | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector |
isFeasible | |
1 (Function) | ToySolver.Arith.Simplex.Textbook |
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 |
isInteresting | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
isInteresting' | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
isNegativeCoeff | ToySolver.Data.Polynomial |
isNonBasicVariable | ToySolver.Arith.Simplex |
IsNonneg | ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin |
isolatingInterval | ToySolver.Data.AlgebraicNumber.Real |
isOptimal | |
1 (Function) | ToySolver.Arith.Simplex.Textbook |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
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 |
IsProblem | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
isRational | ToySolver.Data.AlgebraicNumber.Real |
isRedundant | ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 |
isRepresentable | ToySolver.SAT.Encoder.PB.Internal.Sorter |
isRootOf | ToySolver.Data.Polynomial |
IsSolver | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
isSquareFree | ToySolver.Data.Polynomial |
isUnsat | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
isValid | ToySolver.Wang |
isValidTableau | ToySolver.Arith.Simplex.Textbook |
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 |
lastInEdge | ToySolver.Graph.ShortestPath |
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.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
LearningClause | ToySolver.SAT.Config, ToySolver.SAT |
LearningHybrid | ToySolver.SAT.Config, ToySolver.SAT |
LearningStrategy | ToySolver.SAT.Config, ToySolver.SAT |
lex | ToySolver.Data.Polynomial |
lFalse | ToySolver.Data.LBool |
lift1 | ToySolver.Data.LA |
lift2 | ToySolver.Data.AlgebraicNumber.Root |
liftBool | ToySolver.Data.LBool |
linearize | |
1 (Function) | ToySolver.SAT.Encoder.Integer |
2 (Function) | ToySolver.Converter.PBLinearization |
linearizePBSum | ToySolver.SAT.Encoder.PBNLC |
linearizePBSumWithPolarity | ToySolver.SAT.Encoder.PBNLC |
linearizeWBO | ToySolver.Converter.PBLinearization |
LinearSearch | ToySolver.SAT.PBO |
Lit | |
1 (Type/Class) | ToySolver.Text.QDimacs |
2 (Type/Class) | ToySolver.SAT.Types, ToySolver.SAT |
3 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
4 (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.Textbook |
LP | ToySolver.Arith.Simplex.Textbook.LPSolver |
LPSolve | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.LPSolve, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.LPSolve, ToySolver.Data.MIP.Solver |
lpSolve | ToySolver.Data.MIP.Solver.LPSolve, ToySolver.Data.MIP.Solver |
lpSolvePath | ToySolver.Data.MIP.Solver.LPSolve, ToySolver.Data.MIP.Solver |
Lt | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
lt | ToySolver.Data.Polynomial |
lTrue | ToySolver.Data.LBool |
LubyRestarts | ToySolver.SAT.Config, ToySolver.SAT |
lUndef | ToySolver.Data.LBool |
magnitude | ToySolver.Data.AlgebraicNumber.Complex |
maintainNoSupersets | ToySolver.Combinatorial.HittingSet.Util |
mapCoeff | |
1 (Function) | ToySolver.Data.Polynomial |
2 (Function) | ToySolver.Data.LA |
mapCoeffWithVar | ToySolver.Data.LA |
MARCO | ToySolver.SAT.MUS.Enum |
matrices | ToySolver.Text.SDPFile |
Matrix | |
1 (Type/Class) | ToySolver.Text.SDPFile |
2 (Type/Class) | ToySolver.QBF |
matrix | ToySolver.Text.QDimacs |
maximalInterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
maximize | |
1 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple |
2 (Function) | ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
maximumCardinalityMatching | ToySolver.Combinatorial.BipartiteMatching |
maximumWeightMatching | ToySolver.Combinatorial.BipartiteMatching |
maximumWeightMatchingComplete | ToySolver.Combinatorial.BipartiteMatching |
maximumWeightPerfectMatching | ToySolver.Combinatorial.BipartiteMatching |
maximumWeightPerfectMatchingComplete | ToySolver.Combinatorial.BipartiteMatching |
maxsatPrintModel | ToySolver.SAT.Printer |
maxSubsetSum | ToySolver.Combinatorial.SubsetSum |
mcoprime | ToySolver.Data.Polynomial |
MCS | ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.Enum |
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 | |
1 (Type/Class) | ToySolver.SAT.MUS |
2 (Type/Class) | ToySolver.SAT.MUS.Enum |
3 (Type/Class) | ToySolver.SAT.PBO |
4 (Type/Class) | 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.MARCO |
4 (Function) | ToySolver.Combinatorial.HittingSet.HTCBDD |
5 (Function) | ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 |
minimalPolynomial | |
1 (Function) | ToySolver.Data.AlgebraicNumber.Real |
2 (Function) | ToySolver.Data.AlgebraicNumber.Complex |
minimalUninterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
minimalUninterestingSetOrMaximalInterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
minimize | |
1 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple |
2 (Function) | ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
minimumCardinalityEdgeCover | ToySolver.Combinatorial.BipartiteMatching |
minimumWeightEdgeCover | ToySolver.Combinatorial.BipartiteMatching |
minimumWeightEdgeCoverComplete | ToySolver.Combinatorial.BipartiteMatching |
minimumWeightPerfectMatching | ToySolver.Combinatorial.BipartiteMatching |
minimumWeightPerfectMatchingComplete | ToySolver.Combinatorial.BipartiteMatching |
MiniSATRestarts | ToySolver.SAT.Config, 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.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
2 (Data Constructor) | ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
3 (Type/Class) | ToySolver.Data.IntVar, ToySolver.Arith.VirtualSubstitution, ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper, ToySolver.Arith.OmegaTest |
4 (Type/Class) | ToySolver.SAT.Types, ToySolver.SAT |
5 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
6 (Data Constructor) | ToySolver.EUF.FiniteModelFinder |
7 (Type/Class) | ToySolver.BitVector.Base, ToySolver.BitVector |
8 (Type/Class) | ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple |
9 (Type/Class) | ToySolver.SMT |
10 (Type/Class) | ToySolver.Arith.CAD |
modelGetAssertions | ToySolver.SMT |
modify | ToySolver.Internal.Data.Vec |
modify' | ToySolver.Internal.Data.Vec |
modifyConfig | ToySolver.SAT |
modifyIOURef | ToySolver.Internal.Data.IOURef |
mone | ToySolver.Data.Polynomial |
monoid | ToySolver.Graph.ShortestPath |
monoid' | ToySolver.Graph.ShortestPath |
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.Enum |
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.Enum |
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 |
nat2bv | ToySolver.BitVector.Base, ToySolver.BitVector |
nBlock | ToySolver.Text.SDPFile |
nConstraints | ToySolver.SAT |
Neg | ToySolver.EUF.FiniteModelFinder |
negatePBLinAtLeast | ToySolver.SAT.Types |
negatePolarity | ToySolver.SAT.Encoder.Tseitin |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
NEq | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
new | ToySolver.Internal.Data.Vec |
newCNFStore | ToySolver.SAT.Store.CNF |
newConst | |
1 (Function) | ToySolver.EUF.CongruenceClosure |
2 (Function) | ToySolver.EUF.EUFSolver |
newEncoder | |
1 (Function) | ToySolver.SAT.Encoder.Tseitin |
2 (Function) | ToySolver.SAT.Encoder.PB |
3 (Function) | ToySolver.SAT.Encoder.PBNLC |
newEncoderWithPBLin | ToySolver.SAT.Encoder.Tseitin |
newEncoderWithStrategy | ToySolver.SAT.Encoder.PB |
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 |
newPBStore | ToySolver.SAT.Store.PB |
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.MessagePassing.SurveyPropagation |
4 (Function) | ToySolver.SAT |
5 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
6 (Function) | ToySolver.Arith.Simplex |
7 (Function) | ToySolver.SMT |
8 (Function) | ToySolver.Arith.MIP |
newSolverWithConfig | ToySolver.SAT |
NewVar | ToySolver.SAT.Types |
newVar | |
1 (Function) | ToySolver.SAT.Types, ToySolver.SAT |
2 (Function) | ToySolver.SAT.Encoder.Integer |
3 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
4 (Function) | ToySolver.Arith.Simplex |
5 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
newVar' | ToySolver.BitVector.Solver, ToySolver.BitVector |
newVars | ToySolver.SAT.Types, ToySolver.SAT |
newVars_ | ToySolver.SAT.Types, 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 |
normalizePrefix | ToySolver.QBF |
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.QDimacs |
2 (Function) | ToySolver.Text.CNF |
3 (Function) | ToySolver.Text.GCNF |
4 (Function) | ToySolver.Text.MaxSAT |
numRoots | ToySolver.Data.AlgebraicNumber.Sturm |
numRoots' | ToySolver.Data.AlgebraicNumber.Sturm |
numVars | |
1 (Function) | ToySolver.Text.QDimacs |
2 (Function) | ToySolver.Text.CNF |
3 (Function) | ToySolver.Text.GCNF |
4 (Function) | ToySolver.Text.MaxSAT |
nVars | |
1 (Function) | ToySolver.SAT |
2 (Function) | ToySolver.Arith.Simplex |
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.Simplex, ToySolver.Arith.Simplex.Simple |
objLimit | ToySolver.Arith.Simplex |
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.Textbook |
ObjType | ToySolver.Converter.ObjType, ToySolver.Converter.PBSetObj |
occurFreq | ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 |
Op1 | ToySolver.BitVector.Base, ToySolver.BitVector |
Op2 | ToySolver.BitVector.Base, ToySolver.BitVector |
OpAdd | ToySolver.BitVector.Base, ToySolver.BitVector |
OpAnd | ToySolver.BitVector.Base, ToySolver.BitVector |
OpAShr | ToySolver.BitVector.Base, ToySolver.BitVector |
OpComp | ToySolver.BitVector.Base, ToySolver.BitVector |
OpConcat | ToySolver.BitVector.Base, ToySolver.BitVector |
OpExtract | ToySolver.BitVector.Base, ToySolver.BitVector |
OpLShr | ToySolver.BitVector.Base, ToySolver.BitVector |
OpMul | ToySolver.BitVector.Base, ToySolver.BitVector |
OpNeg | ToySolver.BitVector.Base, ToySolver.BitVector |
OpNot | ToySolver.BitVector.Base, ToySolver.BitVector |
OpOr | ToySolver.BitVector.Base, ToySolver.BitVector |
OpSDiv | ToySolver.BitVector.Base, ToySolver.BitVector |
OpShl | ToySolver.BitVector.Base, ToySolver.BitVector |
OpSMod | ToySolver.BitVector.Base, ToySolver.BitVector |
OpSRem | ToySolver.BitVector.Base, ToySolver.BitVector |
optCheckReal | ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest |
optCheckSAT | ToySolver.Converter.MIP2SMT |
OptDir | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex.Textbook, ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optEnableBiasedSearch | ToySolver.SAT.PBO.BCD2 |
optEnableHardening | ToySolver.SAT.PBO.BCD2 |
optEvalConstr | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.MUS.Enum |
optFileEncoding | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
optHTCBDDCommand | ToySolver.Combinatorial.HittingSet.HTCBDD |
optimize | |
1 (Function) | ToySolver.SAT.PBO |
2 (Function) | ToySolver.Arith.Simplex |
3 (Function) | ToySolver.Arith.Simplex.Simple |
4 (Function) | ToySolver.Arith.MIP |
5 (Function) | ToySolver.Arith.FourierMotzkin.Optimization |
6 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple |
7 (Function) | ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optimizeBase | ToySolver.SAT.Encoder.PB.Internal.Sorter |
Optimizer | ToySolver.SAT.PBO |
Optimum | |
1 (Data Constructor) | ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple |
2 (Data Constructor) | ToySolver.Arith.Simplex.Textbook.LPSolver |
3 (Data Constructor) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
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 |
6 (Data Constructor) | ToySolver.SAT.MUS |
7 (Type/Class) | ToySolver.SAT.MUS.Enum |
8 (Data Constructor) | ToySolver.SAT.MUS.Enum |
9 (Type/Class) | ToySolver.SAT.PBO.BCD2 |
10 (Data Constructor) | ToySolver.SAT.PBO.BCD2 |
11 (Type/Class) | ToySolver.Combinatorial.HittingSet.SHD |
12 (Data Constructor) | ToySolver.Combinatorial.HittingSet.SHD |
13 (Type/Class) | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
14 (Data Constructor) | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
15 (Type/Class) | ToySolver.Combinatorial.HittingSet.HTCBDD |
16 (Data Constructor) | ToySolver.Combinatorial.HittingSet.HTCBDD |
17 (Type/Class) | ToySolver.Arith.Simplex |
18 (Data Constructor) | ToySolver.Arith.Simplex |
19 (Type/Class) | ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest |
20 (Data Constructor) | ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest |
optKnownCSes | ToySolver.SAT.MUS.Enum |
optKnownMCSes | ToySolver.SAT.MUS.Enum |
optKnownMUSes | ToySolver.SAT.MUS.Enum |
optLanguage | ToySolver.Converter.MIP2SMT |
optLogger | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.MUS.Enum |
OptMax | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex.Textbook, ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optMaximalInterestingSets | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
optMethod | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.MUS.Enum |
3 (Function) | ToySolver.Combinatorial.HittingSet.HTCBDD |
OptMin | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Arith.Simplex.Textbook, ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optMinimalHittingSets | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
optMinimalUninterestingSets | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
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 |
optOnMaximalInterestingSetFound | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
optOnMCSFound | ToySolver.SAT.MUS.Enum |
optOnMinimalUninterestingSetFound | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
optOnMUSFound | ToySolver.SAT.MUS.Enum |
optOptimize | ToySolver.Converter.MIP2SMT |
optProduceModel | ToySolver.Converter.MIP2SMT |
OptResult | |
1 (Type/Class) | ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple |
2 (Type/Class) | ToySolver.Arith.Simplex.Textbook.LPSolver |
3 (Type/Class) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optSetLogic | ToySolver.Converter.MIP2SMT |
optSHDArgs | ToySolver.Combinatorial.HittingSet.SHD |
optSHDCommand | ToySolver.Combinatorial.HittingSet.SHD |
optShowLit | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.MUS.Enum |
optSolvingNormalFirst | ToySolver.SAT.PBO.BCD2 |
optStrategy | ToySolver.Data.Polynomial.GroebnerBasis |
OptUnsat | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
optUpdateBest | ToySolver.SAT.MUS |
OpUDiv | ToySolver.BitVector.Base, ToySolver.BitVector |
OpURem | ToySolver.BitVector.Base, ToySolver.BitVector |
OpXOr | ToySolver.BitVector.Base, ToySolver.BitVector |
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, ToySolver.BitVector.Base, ToySolver.BitVector |
2 (Data Constructor) | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector |
ordRel | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector |
OutEdge | ToySolver.Graph.ShortestPath |
packageVersions | ToySolver.Version |
pair | ToySolver.Graph.ShortestPath |
PApp | ToySolver.EUF.FiniteModelFinder |
parse | |
1 (Function) | ToySolver.Data.MIP.Solution.CBC |
2 (Function) | ToySolver.Data.MIP.Solution.CPLEX |
3 (Function) | ToySolver.Data.MIP.Solution.GLPK |
4 (Function) | ToySolver.Data.MIP.Solution.Gurobi |
5 (Function) | ToySolver.Data.MIP.Solution.SCIP |
parseBranchingStrategy | ToySolver.SAT.Config, ToySolver.SAT |
parseByteString | |
1 (Function) | ToySolver.Text.QDimacs |
2 (Function) | ToySolver.Text.CNF |
3 (Function) | ToySolver.Text.GCNF |
4 (Function) | ToySolver.Text.MaxSAT |
parseData | ToySolver.Text.SDPFile |
parseDataFile | ToySolver.Text.SDPFile |
ParseError | |
1 (Type/Class) | ToySolver.Data.MIP |
2 (Type/Class) | ToySolver.Text.SDPFile |
parseFile | |
1 (Function) | ToySolver.Text.QDimacs |
2 (Function) | ToySolver.Data.MIP.LPFile |
3 (Function) | ToySolver.Data.MIP.MPSFile |
4 (Function) | ToySolver.Text.CNF |
5 (Function) | ToySolver.Text.GCNF |
6 (Function) | ToySolver.Text.MaxSAT |
parseLearningStrategy | ToySolver.SAT.Config, ToySolver.SAT |
parseLPString | ToySolver.Data.MIP |
parseMethod | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.SAT.MUS.Enum |
parseMPSString | ToySolver.Data.MIP |
parsePBHandlerType | ToySolver.SAT.Config, ToySolver.SAT |
parser | |
1 (Function) | ToySolver.Data.MIP.LPFile |
2 (Function) | ToySolver.Data.MIP.MPSFile |
parseRestartStrategy | ToySolver.SAT.Config, ToySolver.SAT |
parseSparseData | ToySolver.Text.SDPFile |
parseSparseDataFile | ToySolver.Text.SDPFile |
parseString | |
1 (Function) | ToySolver.Data.MIP.LPFile |
2 (Function) | ToySolver.Data.MIP.MPSFile |
Path | ToySolver.Graph.ShortestPath |
path | ToySolver.Graph.ShortestPath |
pathAppend | ToySolver.Graph.ShortestPath |
pathCost | ToySolver.Graph.ShortestPath |
pathEdges | ToySolver.Graph.ShortestPath |
pathEdgesBackward | ToySolver.Graph.ShortestPath |
pathEdgesSeq | ToySolver.Graph.ShortestPath |
pathEmpty | ToySolver.Graph.ShortestPath |
pathFold | ToySolver.Graph.ShortestPath |
pathFrom | ToySolver.Graph.ShortestPath |
pathTo | ToySolver.Graph.ShortestPath |
pathVertexes | ToySolver.Graph.ShortestPath |
pathVertexesBackward | ToySolver.Graph.ShortestPath |
pathVertexesSeq | ToySolver.Graph.ShortestPath |
PBHandlerType | ToySolver.SAT.Config, ToySolver.SAT |
PBHandlerTypeCounter | ToySolver.SAT.Config, ToySolver.SAT |
PBHandlerTypePueblo | ToySolver.SAT.Config, 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 |
PBStore | ToySolver.SAT.Store.PB |
pbSubsume | ToySolver.SAT.Types |
PBSum | ToySolver.SAT.Types |
PBTerm | ToySolver.SAT.Types |
pbUpperBound | ToySolver.SAT.Types |
pdiv | ToySolver.Data.Polynomial |
pdivMod | ToySolver.Data.Polynomial |
peek | ToySolver.Internal.Data.Vec |
phaseI | |
1 (Function) | ToySolver.Arith.Simplex.Textbook |
2 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
pivot | ToySolver.Arith.Simplex.Textbook |
PivotStrategy | ToySolver.Arith.Simplex |
PivotStrategyBlandRule | ToySolver.Arith.Simplex |
PivotStrategyLargestCoefficient | ToySolver.Arith.Simplex |
pmod | ToySolver.Data.Polynomial |
Point | |
1 (Data Constructor) | ToySolver.Arith.CAD |
2 (Type/Class) | ToySolver.Arith.CAD |
Polarity | |
1 (Type/Class) | ToySolver.SAT.Encoder.Tseitin |
2 (Data Constructor) | ToySolver.SAT.Encoder.Tseitin |
polarityBoth | ToySolver.SAT.Encoder.Tseitin |
polarityNeg | ToySolver.SAT.Encoder.Tseitin |
polarityNegOccurs | ToySolver.SAT.Encoder.Tseitin |
polarityNone | ToySolver.SAT.Encoder.Tseitin |
polarityPos | ToySolver.SAT.Encoder.Tseitin |
polarityPosOccurs | ToySolver.SAT.Encoder.Tseitin |
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.BitVector.Solver, ToySolver.BitVector |
4 (Function) | ToySolver.Arith.Simplex |
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 |
PPCoeff | ToySolver.Data.Polynomial |
pPrintCoeff | ToySolver.Data.Polynomial |
pPrintVar | ToySolver.Data.Polynomial |
Prefix | ToySolver.QBF |
prefix | ToySolver.Text.QDimacs |
PrettyCoeff | ToySolver.Data.Polynomial |
prettyPrint | ToySolver.Data.Polynomial |
PrettyVar | ToySolver.Data.Polynomial |
primalDualSimplex | |
1 (Function) | ToySolver.Arith.Simplex.Textbook |
2 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
printInfo | ToySolver.SAT.MessagePassing.SurveyPropagation |
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.SAT.ExistentialQuantification |
2 (Function) | ToySolver.Arith.VirtualSubstitution |
3 (Function) | ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin |
4 (Function) | ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper |
5 (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 |
propagate | ToySolver.SAT.MessagePassing.SurveyPropagation |
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.BitVector.Solver, ToySolver.BitVector |
4 (Function) | ToySolver.Arith.Simplex |
pushNot | ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
putTableau | ToySolver.Arith.Simplex.Textbook.LPSolver |
QDimacs | |
1 (Type/Class) | ToySolver.Text.QDimacs |
2 (Data Constructor) | ToySolver.Text.QDimacs |
QFFormula | |
1 (Type/Class) | ToySolver.Arith.VirtualSubstitution |
2 (Type/Class) | ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper |
Quantifier | ToySolver.Text.QDimacs, ToySolver.QBF |
quantifyFreeVariables | ToySolver.QBF |
QuantSet | ToySolver.Text.QDimacs |
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 |
QuickXplain | ToySolver.SAT.MUS |
Rat | ToySolver.Arith.FourierMotzkin.Base |
RawModel | ToySolver.Arith.Simplex |
read | ToySolver.Internal.Data.Vec |
readFile | |
1 (Function) | ToySolver.Data.MIP |
2 (Function) | ToySolver.Data.MIP.Solution.CBC |
3 (Function) | ToySolver.Data.MIP.Solution.CPLEX |
4 (Function) | ToySolver.Data.MIP.Solution.GLPK |
5 (Function) | ToySolver.Data.MIP.Solution.Gurobi |
6 (Function) | ToySolver.Data.MIP.Solution.SCIP |
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 |
rebuild | |
1 (Function) | ToySolver.Internal.Data.IndexedPriorityQueue |
2 (Function) | ToySolver.Internal.Data.PriorityQueue |
reduce | ToySolver.Data.Polynomial |
reduceGBasis | ToySolver.Data.Polynomial.GroebnerBasis |
refineIsolatingInterval | ToySolver.Data.AlgebraicNumber.Real |
Rel | ToySolver.BitVector.Base, ToySolver.BitVector |
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.BitVector.Base, ToySolver.BitVector, ToySolver.Arith.Simplex |
render | |
1 (Function) | ToySolver.Text.SDPFile |
2 (Function) | ToySolver.Data.MIP.LPFile |
3 (Function) | ToySolver.Data.MIP.MPSFile |
4 (Function) | ToySolver.Data.MIP.Solution.Gurobi |
renderSparse | ToySolver.Text.SDPFile |
repeat | ToySolver.BitVector.Base, ToySolver.BitVector |
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.Config, ToySolver.SAT |
restrictModel | ToySolver.SAT.Types |
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.Textbook |
RowIndex | ToySolver.Arith.Simplex.Textbook |
run | |
1 (Function) | ToySolver.Combinatorial.HittingSet.MARCO |
2 (Function) | ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 |
3 (Function) | ToySolver.Combinatorial.HittingSet.DAA |
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 |
sBitVec | ToySolver.SMT |
sBool | ToySolver.SMT |
SCIP | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.SCIP, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.SCIP, ToySolver.Data.MIP.Solver |
scip | ToySolver.Data.MIP.Solver.SCIP, ToySolver.Data.MIP.Solver |
scipPath | ToySolver.Data.MIP.Solver.SCIP, ToySolver.Data.MIP.Solver |
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 |
setEncodingChar8 | ToySolver.Internal.Util |
setFinished | ToySolver.SAT.PBO.Context |
setGlobalDeclarations | ToySolver.SMT |
setIterationLimit | ToySolver.SAT.MessagePassing.SurveyPropagation |
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.Simplex |
5 (Function) | ToySolver.Arith.MIP |
setMethod | ToySolver.SAT.PBO |
setNThread | ToySolver.Arith.MIP |
setNThreads | ToySolver.SAT.MessagePassing.SurveyPropagation |
setObj | |
1 (Function) | ToySolver.Converter.PBSetObj |
2 (Function) | ToySolver.Arith.Simplex |
setObjFun | ToySolver.Arith.Simplex.Textbook |
setOnUpdateBestSolution | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.Arith.MIP |
setOnUpdateLowerBound | |
1 (Function) | ToySolver.SAT.PBO.Context |
2 (Function) | ToySolver.SAT.PBO |
setOptDir | ToySolver.Arith.Simplex |
setPBHandlerType | ToySolver.SAT |
setPBSplitClausePart | ToySolver.SAT |
setPivotStrategy | ToySolver.Arith.Simplex |
setRandomFreq | ToySolver.SAT |
setRandomGen | ToySolver.SAT |
setRestartFirst | ToySolver.SAT |
setRestartInc | ToySolver.SAT |
setRestartStrategy | ToySolver.SAT |
setShowRational | ToySolver.Arith.MIP |
setTheory | ToySolver.SAT |
setTolerance | ToySolver.SAT.MessagePassing.SurveyPropagation |
setTrialLimitConf | ToySolver.SAT.PBO |
setUnsat | ToySolver.SAT.PBO.Context |
setUsePB | ToySolver.SAT.Encoder.Tseitin |
setVarPolarity | ToySolver.SAT |
shortestImplicants | ToySolver.SAT.ExistentialQuantification |
showAtom | ToySolver.Data.LA |
showBranchingStrategy | ToySolver.SAT.Config, ToySolver.SAT |
showEntity | ToySolver.EUF.FiniteModelFinder |
showExpr | ToySolver.Data.LA |
showLearningStrategy | ToySolver.SAT.Config, ToySolver.SAT |
showMethod | |
1 (Function) | ToySolver.SAT.MUS |
2 (Function) | ToySolver.SAT.PBO |
3 (Function) | ToySolver.SAT.MUS.Enum |
showModel | ToySolver.EUF.FiniteModelFinder |
showOp | ToySolver.Data.OrdRel, ToySolver.Data.FOL.Arith, ToySolver.Data.LA, ToySolver.BitVector.Base, ToySolver.BitVector |
showPBHandlerType | ToySolver.SAT.Config, ToySolver.SAT |
showRational | ToySolver.Internal.Util |
showRationalAsFiniteDecimal | ToySolver.Internal.Util |
showRestartStrategy | ToySolver.SAT.Config, ToySolver.SAT |
showValue | ToySolver.Arith.Simplex |
shrink | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
signExtend | ToySolver.BitVector.Base, ToySolver.BitVector |
simpARealPoly | ToySolver.Data.AlgebraicNumber.Real |
SimpleAtom | ToySolver.Arith.DifferenceLogic |
SimpleContext | ToySolver.SAT.PBO.Context |
SimpleProblem | |
1 (Type/Class) | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
2 (Data Constructor) | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
simplex | |
1 (Function) | ToySolver.Arith.Simplex.Textbook |
2 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
simplify | |
1 (Function) | ToySolver.Data.BoolExpr |
2 (Function) | ToySolver.Arith.FourierMotzkin.Base |
simplifyAtom | ToySolver.Arith.Simplex |
Singleton | ToySolver.Graph.ShortestPath |
SMTLIB2 | ToySolver.Converter.MIP2SMT |
solObjectiveValue | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Data.MIP.Solution.CBC, ToySolver.Data.MIP.Solution.CPLEX, ToySolver.Data.MIP.Solution.GLPK, ToySolver.Data.MIP.Solution.Gurobi, ToySolver.Data.MIP.Solution.SCIP |
solStatus | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Data.MIP.Solution.CBC, ToySolver.Data.MIP.Solution.CPLEX, ToySolver.Data.MIP.Solution.GLPK, ToySolver.Data.MIP.Solution.Gurobi, ToySolver.Data.MIP.Solution.SCIP |
Solution | |
1 (Type/Class) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Data.MIP.Solution.CBC, ToySolver.Data.MIP.Solution.CPLEX, ToySolver.Data.MIP.Solution.GLPK, ToySolver.Data.MIP.Solution.Gurobi, ToySolver.Data.MIP.Solution.SCIP |
2 (Data Constructor) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Data.MIP.Solution.CBC, ToySolver.Data.MIP.Solution.CPLEX, ToySolver.Data.MIP.Solution.GLPK, ToySolver.Data.MIP.Solution.Gurobi, ToySolver.Data.MIP.Solution.SCIP |
solVariables | ToySolver.Data.MIP.Base, ToySolver.Data.MIP, ToySolver.Data.MIP.Solution.CBC, ToySolver.Data.MIP.Solution.CPLEX, ToySolver.Data.MIP.Solution.GLPK, ToySolver.Data.MIP.Solution.Gurobi, ToySolver.Data.MIP.Solution.SCIP |
solve | |
1 (Function) | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
2 (Function) | ToySolver.SAT |
3 (Function) | ToySolver.QBF |
4 (Function) | ToySolver.SAT.PBO.BC |
5 (Function) | ToySolver.SAT.PBO.BCD |
6 (Function) | ToySolver.SAT.PBO.BCD2 |
7 (Function) | ToySolver.SAT.PBO.MSU4 |
8 (Function) | ToySolver.SAT.PBO.UnsatBased |
9 (Function) | ToySolver.Combinatorial.Knapsack.DPSparse |
10 (Function) | ToySolver.Combinatorial.Knapsack.DPDense |
11 (Function) | ToySolver.Combinatorial.Knapsack.BB |
12 (Function) | ToySolver.Arith.VirtualSubstitution |
13 (Function) | ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin |
14 (Function) | ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest |
15 (Function) | ToySolver.Arith.DifferenceLogic |
16 (Function) | ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper |
17 (Function) | ToySolver.Arith.CAD |
18 (Function) | ToySolver.Arith.ContiTraverso |
19 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple |
solve' | |
1 (Function) | ToySolver.Arith.FourierMotzkin.Base |
2 (Function) | ToySolver.Arith.CAD |
3 (Function) | ToySolver.Arith.ContiTraverso |
solveCEGAR | ToySolver.QBF |
solveCEGARIncremental | ToySolver.QBF |
solveErrorLogger | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
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 |
solveLogger | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
solveNaive | ToySolver.QBF |
SolveOptions | |
1 (Type/Class) | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
2 (Data Constructor) | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
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.MessagePassing.SurveyPropagation |
4 (Type/Class) | ToySolver.SAT |
5 (Type/Class) | ToySolver.BitVector.Solver, ToySolver.BitVector |
6 (Type/Class) | ToySolver.Arith.Simplex |
7 (Type/Class) | ToySolver.SMT |
8 (Type/Class) | ToySolver.Arith.MIP |
9 (Type/Class) | ToySolver.Arith.Simplex.Textbook.LPSolver |
SolverValue | ToySolver.Arith.Simplex |
solveTimeLimit | ToySolver.Data.MIP.Solver.Base, ToySolver.Data.MIP.Solver |
solveWith | ToySolver.SAT |
Sort | |
1 (Type/Class) | ToySolver.SMT |
2 (Data Constructor) | ToySolver.SMT |
Sorter | ToySolver.SAT.Encoder.PB |
sortVector | ToySolver.SAT.Encoder.PB.Internal.Sorter |
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.Enum |
SSym | ToySolver.SMT |
ssymArity | ToySolver.SMT |
SSymBitVec | ToySolver.SMT |
SSymBool | ToySolver.SMT |
SSymReal | ToySolver.SMT |
SSymUninterpreted | ToySolver.SMT |
Status | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusFeasible | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusInfeasible | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusInfeasibleOrUnbounded | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusOptimal | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusUnbounded | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
StatusUnknown | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
Strategy | |
1 (Type/Class) | ToySolver.Data.Polynomial.GroebnerBasis |
2 (Type/Class) | ToySolver.SAT.Encoder.PB |
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.Textbook |
tableau | ToySolver.Arith.Simplex.Textbook.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 |
toAscBits | ToySolver.BitVector.Base, ToySolver.BitVector |
toCSV | ToySolver.Arith.Simplex.Textbook |
toDescBits | ToySolver.BitVector.Base, ToySolver.BitVector |
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.Simplex |
toVar | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
TrivialError | ToySolver.Data.MIP |
true | ToySolver.Data.Boolean, ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
tscale | ToySolver.Data.Polynomial |
twoPhaseSimplex | ToySolver.Arith.Simplex.Textbook.LPSolver |
UDigit | ToySolver.SAT.Encoder.PB.Internal.Sorter |
UMonomial | ToySolver.Data.Polynomial |
Unbounded | |
1 (Data Constructor) | ToySolver.Arith.Simplex, ToySolver.Arith.Simplex.Simple |
2 (Data Constructor) | ToySolver.Arith.Simplex.Textbook.LPSolver |
3 (Data Constructor) | ToySolver.Arith.Simplex.Textbook.LPSolver.Simple, ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple |
unDNF | ToySolver.Data.DNF |
unfixLit | ToySolver.SAT.MessagePassing.SurveyPropagation |
UninterestingSet | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
unit | ToySolver.Graph.ShortestPath |
unitVar | ToySolver.Data.LA |
universe | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.MARCO, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA |
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.Simplex, ToySolver.Arith.Simplex.Simple |
3 (Data Constructor) | ToySolver.Arith.Simplex.Textbook.LPSolver |
UnsatBased | ToySolver.SAT.PBO |
Unsupported | ToySolver.SMT |
UNumber | ToySolver.SAT.Encoder.PB.Internal.Sorter |
update | ToySolver.Internal.Data.IndexedPriorityQueue |
UPolynomial | ToySolver.Data.Polynomial |
US | ToySolver.SAT.MUS.Types, ToySolver.SAT.MUS, ToySolver.SAT.MUS.Enum |
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 |
ValBitVec | 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.Polynomial |
2 (Type/Class) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
3 (Type/Class) | ToySolver.Data.IntVar, ToySolver.Data.LA |
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.BitVector.Base, ToySolver.BitVector |
9 (Data Constructor) | ToySolver.BitVector.Base, ToySolver.BitVector |
10 (Type/Class) | ToySolver.Arith.Simplex |
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.MIP.Base, ToySolver.Data.MIP |
2 (Type/Class) | ToySolver.Data.IntVar |
variables | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
varId | ToySolver.BitVector.Base, ToySolver.BitVector |
VarMap | |
1 (Type/Class) | ToySolver.Data.IntVar |
2 (Type/Class) | ToySolver.SAT.Types |
Vars | ToySolver.Data.Polynomial |
vars | |
1 (Function) | ToySolver.Data.Polynomial |
2 (Function) | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
3 (Function) | ToySolver.Data.IntVar |
VarSet | |
1 (Type/Class) | ToySolver.Data.IntVar |
2 (Type/Class) | ToySolver.SAT.Types |
VarType | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
varType | ToySolver.Data.MIP.Base, ToySolver.Data.MIP |
varWidth | ToySolver.BitVector.Base, ToySolver.BitVector |
VASortFun | ToySolver.SMT |
Vec | ToySolver.Internal.Data.Vec |
version | ToySolver.Version |
WCNF | |
1 (Type/Class) | ToySolver.Text.MaxSAT |
2 (Data Constructor) | ToySolver.Text.MaxSAT |
wcnfBuilder | 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 |
width | ToySolver.BitVector.Base, ToySolver.BitVector |
withVArgs | ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
write | ToySolver.Internal.Data.Vec |
writeFile | |
1 (Function) | ToySolver.Data.MIP |
2 (Function) | ToySolver.Data.MIP.Solution.Gurobi |
3 (Function) | ToySolver.Text.CNF |
4 (Function) | ToySolver.Text.GCNF |
5 (Function) | ToySolver.Text.MaxSAT |
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 |
zeroExtend | ToySolver.BitVector.Base, ToySolver.BitVector |
zmod | ToySolver.Arith.OmegaTest.Base |