| ObjectiveFunction | Text.LPFile |
| objectiveFunction | Text.LPFile |
| ObjLimit | Algorithm.Simplex2 |
| objLimit | Algorithm.Simplex2 |
| ObjMaxOne | Converter.ObjType, Converter.PBSetObj |
| ObjMaxZero | Converter.ObjType, Converter.PBSetObj |
| ObjNone | Converter.ObjType, Converter.PBSetObj |
| objRow | Algorithm.Simplex |
| ObjType | Converter.ObjType, Converter.PBSetObj |
| Op | Text.PBFile |
| optCallback | SAT.CAMUS |
| optCheckReal | Algorithm.OmegaTest |
| optCheckSAT | Converter.LP2SMT |
| OptDir | Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL |
| optimize | |
| 1 (Function) | Algorithm.LPSolverHL |
| 2 (Function) | Algorithm.Simplex2 |
| 3 (Function) | Algorithm.MIPSolver2 |
| 4 (Function) | Algorithm.MIPSolverHL |
| Optimum | |
| 1 (Data Constructor) | Algorithm.LPSolverHL, Algorithm.MIPSolverHL |
| 2 (Data Constructor) | Algorithm.Simplex2 |
| Options | |
| 1 (Type/Class) | SAT.MUS |
| 2 (Data Constructor) | SAT.MUS |
| 3 (Type/Class) | SAT.CAMUS |
| 4 (Data Constructor) | SAT.CAMUS |
| 5 (Type/Class) | SAT.PBO.UnsatBased |
| 6 (Data Constructor) | SAT.PBO.UnsatBased |
| 7 (Type/Class) | SAT.PBO.MSU4 |
| 8 (Data Constructor) | SAT.PBO.MSU4 |
| 9 (Type/Class) | SAT.PBO |
| 10 (Data Constructor) | SAT.PBO |
| 11 (Type/Class) | Data.Polynomial.GroebnerBasis |
| 12 (Data Constructor) | Data.Polynomial.GroebnerBasis |
| 13 (Type/Class) | Converter.LP2SMT |
| 14 (Data Constructor) | Converter.LP2SMT |
| 15 (Type/Class) | Algorithm.Simplex2 |
| 16 (Data Constructor) | Algorithm.Simplex2 |
| 17 (Type/Class) | Algorithm.OmegaTest |
| 18 (Data Constructor) | Algorithm.OmegaTest |
| optLanguage | Converter.LP2SMT |
| optLitPrinter | SAT.MUS |
| optLogger | |
| 1 (Function) | SAT.MUS |
| 2 (Function) | SAT.CAMUS |
| 3 (Function) | SAT.PBO.UnsatBased |
| 4 (Function) | SAT.PBO.MSU4 |
| 5 (Function) | SAT.PBO |
| OptMax | Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL |
| OptMin | Text.LPFile, Algorithm.Simplex, Algorithm.Simplex2, Algorithm.MIPSolverHL |
| optObjFunVarsHeuristics | SAT.PBO |
| optOptimize | Converter.LP2SMT |
| optProduceModel | Converter.LP2SMT |
| OptResult | |
| 1 (Type/Class) | Algorithm.LPSolverHL, Algorithm.MIPSolverHL |
| 2 (Type/Class) | Algorithm.Simplex2 |
| optSearchStrategy | SAT.PBO |
| optStrategy | Data.Polynomial.GroebnerBasis |
| optTrialLimitConf | SAT.PBO |
| OptUnsat | Algorithm.LPSolverHL, Algorithm.MIPSolverHL |
| optUpdateBest | |
| 1 (Function) | SAT.MUS |
| 2 (Function) | SAT.PBO.UnsatBased |
| 3 (Function) | SAT.PBO.MSU4 |
| 4 (Function) | SAT.PBO |
| optUpdateLB | |
| 1 (Function) | SAT.PBO.UnsatBased |
| 2 (Function) | SAT.PBO.MSU4 |
| 3 (Function) | SAT.PBO |
| Or | |
| 1 (Data Constructor) | SAT.TseitinEncoder |
| 2 (Data Constructor) | Algorithm.FOLModelFinder |
| 3 (Data Constructor) | Data.FOL.Formula, Data.FOL.Arith |
| Or' | Algorithm.Cooper.Core, Algorithm.Cooper |
| orB | Algebra.Lattice.Boolean, Data.FOL.Formula, Data.FOL.Arith |