toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Index - S

SatToySolver.Data.FOL.Arith
sat2ipToySolver.Converter.PB2IP, ToySolver.Converter
SAT2IPInfoToySolver.Converter.PB2IP, ToySolver.Converter
SAT2ISInfoToySolver.Converter.SAT2MIS, ToySolver.Converter
sat2ksatToySolver.Converter.SAT2KSAT, ToySolver.Converter
SAT2KSATInfo 
1 (Type/Class)ToySolver.Converter.SAT2KSAT, ToySolver.Converter
2 (Data Constructor)ToySolver.Converter.SAT2KSAT, ToySolver.Converter
sat2maxcutToySolver.Converter.SAT2MaxCut, ToySolver.Converter
SAT2MaxCutInfoToySolver.Converter.SAT2MaxCut, ToySolver.Converter
sat2naesatToySolver.Converter.NAESAT, ToySolver.Converter
SAT2NAESATInfo 
1 (Type/Class)ToySolver.Converter.NAESAT, ToySolver.Converter
2 (Data Constructor)ToySolver.Converter.NAESAT, ToySolver.Converter
sat2pbToySolver.Converter.PB, ToySolver.Converter
SAT2PBInfoToySolver.Converter.PB, ToySolver.Converter
sat3ToISToySolver.Converter.SAT2MIS, ToySolver.Converter
SAT3ToISInfoToySolver.Converter.SAT2MIS, ToySolver.Converter
sat3ToMaxSAT2ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SAT3ToMaxSAT2Info 
1 (Type/Class)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
2 (Data Constructor)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
satPrintModelToySolver.SAT.Printer
SatResultToySolver.Data.FOL.Arith
satToISToySolver.Converter.SAT2MIS, ToySolver.Converter
satToMaxSAT2ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SATToMaxSAT2InfoToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
satToSimpleMaxCutToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SATToSimpleMaxCutInfoToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
sBitVecToySolver.SMT
sBoolToySolver.SMT
separateToySolver.Data.AlgebraicNumber.Sturm
separate'ToySolver.Data.AlgebraicNumber.Sturm
SeqQueueToySolver.Internal.Data.SeqQueue
SequentToySolver.Wang
SequentialCounterToySolver.SAT.Encoder.Cardinality
setConfBudgetToySolver.SAT.Solver.CDCL, ToySolver.SAT
setConfig 
1 (Function)ToySolver.Arith.Simplex
2 (Function)ToySolver.SAT.Solver.CDCL, ToySolver.SAT
setEnableObjFunVarsHeuristicsToySolver.SAT.PBO
setEncodingChar8ToySolver.Internal.Util
setFinishedToySolver.SAT.PBO.Context
setGlobalDeclarationsToySolver.SMT
setIterationLimitToySolver.SAT.Solver.MessagePassing.SurveyPropagation
setLearnCallbackToySolver.SAT.Solver.CDCL, ToySolver.SAT
setLogger 
1 (Function)ToySolver.Arith.Simplex
2 (Function)ToySolver.Arith.MIP
3 (Function)ToySolver.SAT.Solver.CDCL, ToySolver.SAT
4 (Function)ToySolver.SAT.PBO.Context
5 (Function)ToySolver.SAT.PBO
setMethodToySolver.SAT.PBO
setNThreadToySolver.Arith.MIP
setNThreadsToySolver.SAT.Solver.MessagePassing.SurveyPropagation
setObj 
1 (Function)ToySolver.Converter.PBSetObj
2 (Function)ToySolver.Arith.Simplex
setObjFunToySolver.Arith.Simplex.Textbook
setOnUpdateBestSolution 
1 (Function)ToySolver.Arith.MIP
2 (Function)ToySolver.SAT.PBO.Context
3 (Function)ToySolver.SAT.PBO
setOnUpdateLowerBound 
1 (Function)ToySolver.SAT.PBO.Context
2 (Function)ToySolver.SAT.PBO
setOptDirToySolver.Arith.Simplex
setPivotStrategyToySolver.Arith.Simplex
setRandomGen 
1 (Function)ToySolver.SAT.Solver.CDCL, ToySolver.SAT
2 (Function)ToySolver.SAT.Solver.SLS.ProbSAT
setShowRationalToySolver.Arith.MIP
setTerminateCallbackToySolver.SAT.Solver.CDCL, ToySolver.SAT
setTheoryToySolver.SAT.Solver.CDCL, ToySolver.SAT
setToleranceToySolver.SAT.Solver.MessagePassing.SurveyPropagation
setTrialLimitConfToySolver.SAT.PBO
setUnsatToySolver.SAT.PBO.Context
setUsePBToySolver.SAT.Encoder.Tseitin
setVarPolarityToySolver.SAT.Solver.CDCL, ToySolver.SAT
shortestImplicantsEToySolver.SAT.ExistentialQuantification
showAtomToySolver.Data.LA
showBranchingStrategyToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT
showEntityToySolver.EUF.FiniteModelFinder
showExprToySolver.Data.LA
showLearningStrategyToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT
showMethod 
1 (Function)ToySolver.SAT.PBO
2 (Function)ToySolver.SAT.MUS.Enum
3 (Function)ToySolver.SAT.MUS
showModelToySolver.EUF.FiniteModelFinder
showOpToySolver.Data.OrdRel, ToySolver.Data.LA, ToySolver.Data.FOL.Arith, ToySolver.BitVector.Base, ToySolver.BitVector
showPBHandlerTypeToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT
showPivotStrategyToySolver.Arith.Simplex
showRationalToySolver.Internal.Util
showRationalAsFiniteDecimalToySolver.Internal.Util
showRestartStrategyToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT
showValueToySolver.Arith.Simplex
shrinkToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA, ToySolver.Combinatorial.HittingSet.MARCO
signExtendToySolver.BitVector.Base, ToySolver.BitVector
simpARealPolyToySolver.Data.AlgebraicNumber.Real
SimpleAtomToySolver.Arith.DifferenceLogic
SimpleContextToySolver.SAT.PBO.Context
SimpleMaxSAT2ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
simpleMaxSAT2ToSimpleMaxCutToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SimpleMaxSAT2ToSimpleMaxCutInfo 
1 (Type/Class)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
2 (Data Constructor)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SimpleProblem 
1 (Type/Class)ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA, ToySolver.Combinatorial.HittingSet.MARCO
2 (Data Constructor)ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA, ToySolver.Combinatorial.HittingSet.MARCO
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
3 (Function)ToySolver.SAT.Formula, ToySolver.SAT.Encoder.Tseitin
simplifyAtomToySolver.Arith.Simplex
simplifyMaxSAT2ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SimplifyMaxSAT2Info 
1 (Type/Class)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
2 (Data Constructor)ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter
SingletonToySolver.Graph.ShortestPath
SMTLIB2ToySolver.Converter.MIP2SMT
Solution 
1 (Type/Class)ToySolver.Graph.MaxCut
2 (Type/Class)ToySolver.QUBO
3 (Type/Class)ToySolver.Text.SDPFile
4 (Data Constructor)ToySolver.Text.SDPFile
solve 
1 (Function)ToySolver.Combinatorial.Knapsack.BB
2 (Function)ToySolver.Combinatorial.Knapsack.DPDense
3 (Function)ToySolver.Combinatorial.Knapsack.DPSparse
4 (Function)ToySolver.Arith.VirtualSubstitution
5 (Function)ToySolver.Arith.FourierMotzkin.Base, ToySolver.Arith.FourierMotzkin
6 (Function)ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
7 (Function)ToySolver.Arith.CAD
8 (Function)ToySolver.Arith.DifferenceLogic
9 (Function)ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
10 (Function)ToySolver.Arith.Simplex.Textbook.LPSolver.Simple
11 (Function)ToySolver.Arith.ContiTraverso
12 (Function)ToySolver.SAT.Solver.CDCL, ToySolver.SAT
13 (Function)ToySolver.SAT.PBO.UnsatBased
14 (Function)ToySolver.SAT.PBO.MSU4
15 (Function)ToySolver.SAT.PBO.BCD2
16 (Function)ToySolver.SAT.PBO.BCD
17 (Function)ToySolver.SAT.PBO.BC
18 (Function)ToySolver.QBF
solve' 
1 (Function)ToySolver.Arith.FourierMotzkin.Base
2 (Function)ToySolver.Arith.CAD
3 (Function)ToySolver.Arith.ContiTraverso
solveCEGARToySolver.QBF
solveCEGARIncrementalToySolver.QBF
solveForToySolver.Data.LA
solveFormula 
1 (Function)ToySolver.Arith.FourierMotzkin.FOL, ToySolver.Arith.FourierMotzkin
2 (Function)ToySolver.Arith.Cooper.FOL, ToySolver.Arith.Cooper
solveGenericToySolver.Combinatorial.Knapsack.DPSparse
solveIntToySolver.Combinatorial.Knapsack.DPSparse
solveIntegerToySolver.Combinatorial.Knapsack.DPSparse
solveNaiveToySolver.QBF
solveQEToySolver.QBF
solveQE_CNFToySolver.QBF
solveQFFormula 
1 (Function)ToySolver.Arith.VirtualSubstitution
2 (Function)ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
solveQFLIRAConj 
1 (Function)ToySolver.Arith.Cooper.Base, ToySolver.Arith.Cooper
2 (Function)ToySolver.Arith.OmegaTest.Base, ToySolver.Arith.OmegaTest
Solver 
1 (Type/Class)ToySolver.EUF.CongruenceClosure
2 (Type/Class)ToySolver.EUF.EUFSolver
3 (Type/Class)ToySolver.Arith.Simplex
4 (Type/Class)ToySolver.Arith.MIP
5 (Type/Class)ToySolver.Arith.Simplex.Textbook.LPSolver
6 (Type/Class)ToySolver.SAT.Solver.MessagePassing.SurveyPropagation
7 (Type/Class)ToySolver.SAT.Solver.CDCL, ToySolver.SAT
8 (Type/Class)ToySolver.BitVector.Solver, ToySolver.BitVector
9 (Type/Class)ToySolver.SAT.Solver.SLS.ProbSAT
10 (Type/Class)ToySolver.SMT
SolverValueToySolver.Arith.Simplex
solveWithToySolver.SAT.Solver.CDCL, ToySolver.SAT
SomeWCNFToySolver.FileFormat.CNF
SomeWCNFNewToySolver.FileFormat.CNF
SomeWCNFOldToySolver.FileFormat.CNF
Sort 
1 (Type/Class)ToySolver.SMT
2 (Data Constructor)ToySolver.SMT
SorterToySolver.SAT.Encoder.PB
sortVectorToySolver.SAT.Encoder.PB.Internal.Sorter
SourceToySolver.Converter.Base, ToySolver.Converter.PB, ToySolver.Converter.PB, ToySolver.Converter, ToySolver.Converter
SourceObjValueToySolver.Converter.Base, ToySolver.Converter.PB, ToySolver.Converter.PB, ToySolver.Converter, ToySolver.Converter
spolynomialToySolver.Data.Polynomial.GroebnerBasis
SQFreeToySolver.Data.Polynomial
sqfree 
1 (Function)ToySolver.Data.Polynomial
2 (Function)ToySolver.Data.Polynomial.Factorization.FiniteField
sqfreeChar0ToySolver.Data.Polynomial.Factorization.SquareFree
sRealToySolver.SMT
SSToySolver.SAT.MUS.Types, ToySolver.SAT.MUS.Enum, ToySolver.SAT.MUS
SSymToySolver.SMT
ssymArityToySolver.SMT
SSymBitVecToySolver.SMT
SSymBoolToySolver.SMT
SSymRealToySolver.SMT
SSymUninterpretedToySolver.SMT
statFlipsToySolver.SAT.Solver.SLS.ProbSAT
statFlipsPerSecondToySolver.SAT.Solver.SLS.ProbSAT
Statistics 
1 (Type/Class)ToySolver.SAT.Solver.SLS.ProbSAT
2 (Data Constructor)ToySolver.SAT.Solver.SLS.ProbSAT
statTotalCPUTimeToySolver.SAT.Solver.SLS.ProbSAT
Strategy 
1 (Type/Class)ToySolver.Data.Polynomial.GroebnerBasis
2 (Type/Class)ToySolver.SAT.Encoder.PB
3 (Type/Class)ToySolver.SAT.Encoder.Cardinality
SturmChainToySolver.Data.AlgebraicNumber.Sturm
sturmChainToySolver.Data.AlgebraicNumber.Sturm
subsetSumToySolver.Combinatorial.SubsetSum
substToySolver.Data.Polynomial
SugarStrategyToySolver.Data.Polynomial.GroebnerBasis