| Sat | ToySolver.Data.FOL.Arith |
| sat2ip | ToySolver.Converter.MIP, ToySolver.Converter |
| SAT2IPInfo | ToySolver.Converter.MIP, ToySolver.Converter |
| SAT2ISInfo | ToySolver.Converter.SAT2MIS, ToySolver.Converter |
| sat2ksat | ToySolver.Converter.SAT2KSAT, ToySolver.Converter |
| SAT2KSATInfo | ToySolver.Converter.SAT2KSAT, ToySolver.Converter |
| sat2maxcut | ToySolver.Converter.SAT2MaxCut, ToySolver.Converter |
| SAT2MaxCutInfo | ToySolver.Converter.SAT2MaxCut, ToySolver.Converter |
| sat2naesat | ToySolver.Converter.NAESAT, ToySolver.Converter |
| SAT2NAESATInfo | |
| 1 (Type/Class) | ToySolver.Converter.NAESAT, ToySolver.Converter |
| 2 (Data Constructor) | ToySolver.Converter.NAESAT, ToySolver.Converter |
| sat2pb | ToySolver.Converter.PB, ToySolver.Converter |
| SAT2PBInfo | ToySolver.Converter.PB, ToySolver.Converter |
| sat3ToIS | ToySolver.Converter.SAT2MIS, ToySolver.Converter |
| SAT3ToISInfo | ToySolver.Converter.SAT2MIS, ToySolver.Converter |
| sat3ToMaxSAT2 | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| SAT3ToMaxSAT2Info | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| satPrintModel | ToySolver.SAT.Printer |
| SatResult | ToySolver.Data.FOL.Arith |
| satToIS | ToySolver.Converter.SAT2MIS, ToySolver.Converter |
| satToMaxSAT2 | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| SATToMaxSAT2Info | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| satToSimpleMaxCut | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| SATToSimpleMaxCutInfo | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| sBitVec | ToySolver.SMT |
| sBool | ToySolver.SMT |
| separate | ToySolver.Data.AlgebraicNumber.Sturm |
| separate' | ToySolver.Data.AlgebraicNumber.Sturm |
| SeqQueue | ToySolver.Internal.Data.SeqQueue |
| Sequent | ToySolver.Wang |
| SequentialCounter | ToySolver.SAT.Encoder.Cardinality |
| setConfBudget | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| setConfig | |
| 1 (Function) | ToySolver.Arith.Simplex |
| 2 (Function) | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| setEnableObjFunVarsHeuristics | ToySolver.SAT.PBO |
| setEncodingChar8 | ToySolver.Internal.Util |
| setFinished | ToySolver.SAT.PBO.Context |
| setGlobalDeclarations | ToySolver.SMT |
| setIterationLimit | ToySolver.SAT.Solver.MessagePassing.SurveyPropagation |
| setLearnCallback | ToySolver.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 |
| setMethod | ToySolver.SAT.PBO |
| setNThread | ToySolver.Arith.MIP |
| setNThreads | ToySolver.SAT.Solver.MessagePassing.SurveyPropagation |
| setObj | |
| 1 (Function) | ToySolver.Arith.Simplex |
| 2 (Function) | ToySolver.Converter.PB, ToySolver.Converter |
| setObjFun | ToySolver.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 |
| setOptDir | ToySolver.Arith.Simplex |
| setPivotStrategy | ToySolver.Arith.Simplex |
| setRandomGen | |
| 1 (Function) | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| 2 (Function) | ToySolver.SAT.Solver.SLS.ProbSAT |
| setShowRational | ToySolver.Arith.MIP |
| setTerminateCallback | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| setTheory | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| setTolerance | ToySolver.SAT.Solver.MessagePassing.SurveyPropagation |
| setTrialLimitConf | ToySolver.SAT.PBO |
| setUnsat | ToySolver.SAT.PBO.Context |
| setUsePB | ToySolver.SAT.Encoder.Tseitin |
| setVarPolarity | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| shortestImplicantsE | ToySolver.SAT.ExistentialQuantification |
| showAtom | ToySolver.Data.LA |
| showBranchingStrategy | ToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| showEntity | ToySolver.EUF.FiniteModelFinder |
| showExpr | ToySolver.Data.LA |
| showLearningStrategy | ToySolver.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 |
| showModel | ToySolver.EUF.FiniteModelFinder |
| showOp | ToySolver.Data.OrdRel, ToySolver.Data.LA, ToySolver.Data.FOL.Arith, ToySolver.BitVector.Base, ToySolver.BitVector |
| showPBHandlerType | ToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| showPivotStrategy | ToySolver.Arith.Simplex |
| showRational | ToySolver.Internal.Util |
| showRationalAsFiniteDecimal | ToySolver.Internal.Util |
| showRestartStrategy | ToySolver.SAT.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| showStrategy | ToySolver.SAT.Encoder.PB |
| showValue | ToySolver.Arith.Simplex |
| shrink | ToySolver.Combinatorial.HittingSet.InterestingSets, ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999, ToySolver.Combinatorial.HittingSet.DAA, ToySolver.Combinatorial.HittingSet.MARCO |
| signExtend | ToySolver.BitVector.Base, ToySolver.BitVector |
| simpARealPoly | ToySolver.Data.AlgebraicNumber.Real |
| SimpleAtom | ToySolver.Arith.DifferenceLogic |
| SimpleContext | ToySolver.SAT.PBO.Context |
| SimpleMaxSAT2 | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| simpleMaxSAT2ToSimpleMaxCut | ToySolver.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 |
| simplifyAtom | ToySolver.Arith.Simplex |
| simplifyMaxSAT2 | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| SimplifyMaxSAT2Info | ToySolver.Converter.SAT2MaxSAT, ToySolver.Converter |
| Singleton | ToySolver.Graph.ShortestPath |
| SMTLIB2 | ToySolver.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 |
| solveCEGAR | ToySolver.QBF |
| solveCEGARIncremental | ToySolver.QBF |
| 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 |
| solveNaive | ToySolver.QBF |
| solveQE | ToySolver.QBF |
| solveQE_CNF | ToySolver.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 |
| SolverValue | ToySolver.Arith.Simplex |
| solveWith | ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| SomeWCNF | ToySolver.FileFormat.CNF |
| SomeWCNFNew | ToySolver.FileFormat.CNF |
| SomeWCNFOld | ToySolver.FileFormat.CNF |
| Sort | |
| 1 (Type/Class) | ToySolver.SMT |
| 2 (Data Constructor) | ToySolver.SMT |
| Sorter | ToySolver.SAT.Encoder.PB |
| sortVector | ToySolver.SAT.Encoder.PB.Internal.Sorter |
| Source | ToySolver.Converter.Base, ToySolver.Converter.PB, ToySolver.Converter.PB, ToySolver.Converter, ToySolver.Converter |
| SourceObjValue | ToySolver.Converter.Base, ToySolver.Converter.PB, ToySolver.Converter.PB, ToySolver.Converter, ToySolver.Converter |
| 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.Enum, ToySolver.SAT.MUS |
| SSym | ToySolver.SMT |
| ssymArity | ToySolver.SMT |
| SSymBitVec | ToySolver.SMT |
| SSymBool | ToySolver.SMT |
| SSymReal | ToySolver.SMT |
| SSymUninterpreted | ToySolver.SMT |
| statFlips | ToySolver.SAT.Solver.SLS.ProbSAT |
| statFlipsPerSecond | ToySolver.SAT.Solver.SLS.ProbSAT |
| Statistics | |
| 1 (Type/Class) | ToySolver.SAT.Solver.SLS.ProbSAT |
| 2 (Data Constructor) | ToySolver.SAT.Solver.SLS.ProbSAT |
| statTotalCPUTime | ToySolver.SAT.Solver.SLS.ProbSAT |
| Strategy | |
| 1 (Type/Class) | ToySolver.Data.Polynomial.GroebnerBasis |
| 2 (Type/Class) | ToySolver.SAT.Encoder.Cardinality |
| 3 (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 |