| E | ToySolver.FileFormat.CNF, ToySolver.QBF |
| EAp | ToySolver.SMT |
| EConst | ToySolver.BitVector.Base, ToySolver.BitVector |
| Edge | |
| 1 (Type/Class) | ToySolver.Graph.Base |
| 2 (Type/Class) | ToySolver.Graph.ShortestPath |
| EdgeLabeledGraph | ToySolver.Graph.Base |
| 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 | |
| 1 (Function) | ToySolver.SAT.Encoder.PB.Internal.Sorter |
| 2 (Function) | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| encodeAtLeast | ToySolver.SAT.Encoder.Cardinality |
| encodeAtLeastWithPolarity | |
| 1 (Function) | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| 2 (Function) | ToySolver.SAT.Encoder.Cardinality |
| encodeAtLeastWithPolarityNaive | ToySolver.SAT.Encoder.Cardinality.Internal.Naive |
| encodeAtLeastWithPolarityParallelCounter | ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter |
| encodeCardinalityWithPolarity | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| 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 |
| encodePBLinAtLeastSorter | ToySolver.SAT.Encoder.PB.Internal.Sorter |
| encodePBLinAtLeastWithPolarity | ToySolver.SAT.Encoder.PB |
| encodePBLinAtLeastWithPolarityAdder | ToySolver.SAT.Encoder.PB.Internal.Adder |
| encodePBLinAtLeastWithPolarityBCCNF | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| encodePBLinAtLeastWithPolarityBDD | ToySolver.SAT.Encoder.PB.Internal.BDD |
| encodePrefixSum | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| encodePrefixSumBuggy | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| encodePrefixSumNaive | ToySolver.SAT.Encoder.PB.Internal.BCCNF |
| Encoder | |
| 1 (Type/Class) | ToySolver.SAT.Encoder.Tseitin |
| 2 (Type/Class) | ToySolver.SAT.Encoder.PBNLC |
| 3 (Type/Class) | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| 4 (Data Constructor) | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| 5 (Type/Class) | ToySolver.SAT.Encoder.Cardinality |
| 6 (Type/Class) | ToySolver.SAT.Encoder.PB |
| 7 (Data Constructor) | ToySolver.SAT.Encoder.PB |
| encodeSum | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| encodeXOR | ToySolver.SAT.Encoder.Tseitin |
| encodeXORWithPolarity | ToySolver.SAT.Encoder.Tseitin |
| Enqueue | ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.PriorityQueue, ToySolver.Internal.Data.IndexedPriorityQueue |
| enqueue | ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.PriorityQueue, ToySolver.Internal.Data.IndexedPriorityQueue |
| enqueueBatch | ToySolver.Internal.Data.SeqQueue, ToySolver.Internal.Data.PriorityQueue, ToySolver.Internal.Data.IndexedPriorityQueue |
| 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 | ToySolver.Data.OrdRel, ToySolver.Data.LA, ToySolver.Data.FOL.Arith, ToySolver.BitVector.Base, ToySolver.Arith.Simplex, ToySolver.BitVector |
| 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 |
| 4 (Data Constructor) | ToySolver.SAT.Formula, ToySolver.SAT.Encoder.Tseitin |
| Error | ToySolver.SMT |
| Eval | ToySolver.Data.IntVar, ToySolver.Data.LA, ToySolver.Arith.VirtualSubstitution, ToySolver.Arith.Cooper.Base |
| eval | |
| 1 (Function) | ToySolver.Data.IntVar, ToySolver.Data.LA, ToySolver.Arith.VirtualSubstitution, ToySolver.Arith.Cooper.Base |
| 2 (Function) | ToySolver.Data.Polynomial |
| 3 (Function) | ToySolver.Graph.MaxCut |
| 4 (Function) | ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
| 5 (Function) | ToySolver.QUBO |
| 6 (Function) | ToySolver.SAT.Encoder.Integer |
| 7 (Function) | ToySolver.SMT |
| evalAp | ToySolver.EUF.CongruenceClosure, ToySolver.EUF.EUFSolver |
| evalAtLeast | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalAtom | |
| 1 (Function) | ToySolver.Data.FOL.Arith |
| 2 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
| 3 (Function) | ToySolver.EUF.FiniteModelFinder |
| evalBounds | ToySolver.Arith.FourierMotzkin.Base |
| evalCell | ToySolver.Arith.CAD |
| evalClause | |
| 1 (Function) | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| 2 (Function) | ToySolver.EUF.FiniteModelFinder |
| evalClauses | ToySolver.EUF.FiniteModelFinder |
| evalClausesU | ToySolver.EUF.FiniteModelFinder |
| evalDefinitions | ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer |
| evalDualObjective | ToySolver.Text.SDPFile |
| evalEdge | ToySolver.Graph.MaxCut |
| evalExactly | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalExpr | |
| 1 (Function) | ToySolver.Data.FOL.Arith |
| 2 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
| evalFormula | |
| 1 (Function) | ToySolver.EUF.FiniteModelFinder |
| 2 (Function) | ToySolver.SAT.Formula, ToySolver.SAT.Encoder.Tseitin |
| evalFSym | ToySolver.SMT |
| evalIsingModel | ToySolver.QUBO |
| evalLinear | ToySolver.Data.LA |
| evalLit | |
| 1 (Function) | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| 2 (Function) | ToySolver.EUF.FiniteModelFinder |
| evalNAEClause | ToySolver.Converter.NAESAT, ToySolver.Converter |
| evalNAESAT | ToySolver.Converter.NAESAT, ToySolver.Converter |
| evalObjectiveFunction | ToySolver.SAT.PBO.Context |
| evalOp | ToySolver.Data.OrdRel, ToySolver.Data.LA, ToySolver.Data.FOL.Arith, ToySolver.BitVector.Base, ToySolver.BitVector |
| evalPBConstraint | ToySolver.SAT.Types |
| evalPBFormula | ToySolver.SAT.Types |
| evalPBLinAtLeast | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalPBLinExactly | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalPBLinSum | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalPBSoftFormula | ToySolver.SAT.Types |
| evalPBSum | ToySolver.SAT.Types |
| evalPoint | ToySolver.Arith.CAD |
| evalPrimalObjective | ToySolver.Text.SDPFile |
| evalSOS2 | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalTerm | ToySolver.EUF.FiniteModelFinder |
| evalTotalizerDefinitions | ToySolver.SAT.Encoder.Cardinality |
| EValue | ToySolver.SMT |
| evalVar | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| evalXORClause | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| EVar | ToySolver.BitVector.Base, ToySolver.BitVector |
| Exactly | ToySolver.SAT.Types, ToySolver.SAT.Solver.CDCL, ToySolver.SAT |
| Exception | ToySolver.SMT |
| exgcd | ToySolver.Data.Polynomial |
| Exists | |
| 1 (Data Constructor) | ToySolver.Data.FOL.Formula, ToySolver.Data.FOL.Arith |
| 2 (Data Constructor) | ToySolver.EUF.FiniteModelFinder |
| explain | |
| 1 (Function) | ToySolver.EUF.CongruenceClosure |
| 2 (Function) | ToySolver.EUF.EUFSolver |
| 3 (Function) | ToySolver.Arith.Simplex |
| 4 (Function) | ToySolver.BitVector.Solver, ToySolver.BitVector |
| explainConst | ToySolver.EUF.CongruenceClosure |
| explainFlatTerm | ToySolver.EUF.CongruenceClosure |
| Expr | |
| 1 (Type/Class) | ToySolver.Data.LA |
| 2 (Type/Class) | ToySolver.Data.FOL.Arith |
| 3 (Type/Class) | ToySolver.BitVector.Base, ToySolver.BitVector |
| 4 (Type/Class) | ToySolver.SAT.Encoder.Integer |
| 5 (Data Constructor) | ToySolver.SAT.Encoder.Integer |
| 6 (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 |
| extract | |
| 1 (Function) | ToySolver.Data.LA |
| 2 (Function) | ToySolver.BitVector.Base, ToySolver.BitVector |
| extractMaybe | ToySolver.Data.LA |