| A | ToySolver.FileFormat.CNF, ToySolver.QBF |
| AComplex | ToySolver.Data.AlgebraicNumber.Complex |
| AdaptiveSearch | ToySolver.SAT.PBO |
| addAtLeast | |
| 1 (Function) | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| 2 (Function) | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| addAtLeastNaive | ToySolver.SAT.Encoder.Cardinality.Internal.Naive |
| addAtLeastParallelCounter | ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter |
| addAtMost | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| AddCardinality | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addCardinality | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| AddClause | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addClause | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addConstraint | |
| 1 (Function) | ToySolver.Arith.Simplex.Textbook.LPSolver |
| 2 (Function) | ToySolver.SAT.Encoder.Integer |
| addConstraintSoft | ToySolver.SAT.Encoder.Integer |
| addConstraintWithArtificialVariable | ToySolver.Arith.Simplex.Textbook.LPSolver |
| Adder | ToySolver.SAT.Encoder.PB |
| addExactly | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addFormula | ToySolver.SAT.Encoder.Tseitin |
| addLowerBound | ToySolver.SAT.PBO.Context |
| addMIP | ToySolver.Converter.MIP, ToySolver.Converter |
| addPBAtLeast | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBAtLeastSoft | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBAtMost | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBAtMostSoft | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBExactly | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBExactlySoft | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| AddPBLin | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addPBLinAtLeastAdder | ToySolver.SAT.Encoder.PB.Internal.Adder |
| addPBLinAtLeastBCCNF | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| 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 |
| addSOS2 | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addWBO | ToySolver.Converter.PB, ToySolver.Converter |
| AddXORClause | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addXORClause | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| addXORClauseSoft | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, 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 |
| 4 (Data Constructor) | ToySolver.SAT.Formula, ToySolver.SAT.Encoder.Tseitin |
| 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.Solver.CDCL.Config, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| asConst | ToySolver.Data.LA |
| assert | ToySolver.SMT |
| assertAtom | |
| 1 (Function) | ToySolver.Arith.Simplex |
| 2 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
| 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.Solver.CDCL, ToySolver.SAT |
| Atom | |
| 1 (Data Constructor) | ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
| 2 (Data Constructor) | ToySolver.Data.BoolExpr |
| 3 (Type/Class) | ToySolver.Data.LA, ToySolver.Arith.Simplex |
| 4 (Type/Class) | ToySolver.Data.FOL.Arith |
| 5 (Type/Class) | ToySolver.BitVector.Base, ToySolver.BitVector |
| 6 (Data Constructor) | ToySolver.EUF.FiniteModelFinder |
| 7 (Type/Class) | ToySolver.EUF.FiniteModelFinder |
| 8 (Data Constructor) | ToySolver.SAT.Formula, ToySolver.SAT.Encoder.Tseitin |
| 9 (Type/Class) | ToySolver.FileFormat.CNF |