| AddLiteral(const Variable &formula_var, const Formula &formula) override | dlinear::NNSoplexTheorySolver | virtual |
| AddLiterals() override | dlinear::SoplexTheorySolver | virtual |
| AddVariable(const Variable &var) override | dlinear::SoplexTheorySolver | virtual |
| Bound typedef | dlinear::TheorySolver | |
| BoundViolationType enum name | dlinear::TheorySolver | protected |
| CheckSat(const Box &box, mpq_class *actual_precision, std::set< LiteralSet > &explanations) | dlinear::TheorySolver | |
| CheckSatCore(mpq_class *actual_precision, std::set< LiteralSet > &explanations) override | dlinear::NNSoplexTheorySolver | virtual |
| config() const | dlinear::TheorySolver | inline |
| config_ | dlinear::TheorySolver | protected |
| Consolidate(const Box &box) override | dlinear::NNSoplexTheorySolver | privatevirtual |
| DisableSpxRows() | dlinear::SoplexTheorySolver | protected |
| enabled_literals() const | dlinear::TheorySolver | |
| EnableLiteral(const Literal &lit) override | dlinear::NNSoplexTheorySolver | virtual |
| EnableLiterals(std::span< const Literal > theory_literals) | dlinear::TheorySolver | |
| EnableSpxRow(int spx_row, bool truth) override | dlinear::NNSoplexTheorySolver | privatevirtual |
| dlinear::SoplexTheorySolver::EnableSpxRow(int spx_row) | dlinear::SoplexTheorySolver | protected |
| EnableSpxVarBound() | dlinear::SoplexTheorySolver | protectedvirtual |
| Explanations typedef | dlinear::TheorySolver | |
| fixed_preprocessor() const | dlinear::TheorySolver | inline |
| fixed_preprocessor_ | dlinear::TheorySolver | protected |
| fixed_theory_bounds() const | dlinear::TheorySolver | inline |
| GetActiveRows() | dlinear::SoplexTheorySolver | protected |
| GetActiveRows(const std::vector< int > &spx_rows) | dlinear::SoplexTheorySolver | protected |
| GetSpxInfeasibilityRay(soplex::VectorRational &farkas_ray) | dlinear::SoplexTheorySolver | protected |
| GetSpxInfeasibilityRay(soplex::VectorRational &farkas_ray, std::vector< BoundViolationType > &bounds_ray) | dlinear::SoplexTheorySolver | protected |
| infinity_ | dlinear::SoplexTheorySolver | protectedstatic |
| InvertGreatestViolation() | dlinear::NNSoplexTheorySolver | private |
| is_consolidated_ | dlinear::TheorySolver | protected |
| IsRowActive(int spx_row) | dlinear::SoplexTheorySolver | protected |
| IsRowActive(int spx_row, const soplex::Rational &value) | dlinear::SoplexTheorySolver | protected |
| lit_to_theory_row() const | dlinear::TheorySolver | inline |
| lit_to_theory_row_ | dlinear::TheorySolver | protected |
| m_fixed_preprocessor() | dlinear::TheorySolver | inline |
| m_preprocessor() | dlinear::TheorySolver | inline |
| model() const | dlinear::TheorySolver | |
| model_ | dlinear::TheorySolver | protected |
| ninfinity_ | dlinear::SoplexTheorySolver | protectedstatic |
| ParseRowCoeff(const Formula &formula) | dlinear::SoplexTheorySolver | protected |
| predicate_abstractor() const | dlinear::TheorySolver | inline |
| predicate_abstractor_ | dlinear::TheorySolver | protected |
| PreprocessFixedLiterals(const LiteralSet &fixed_literals) | dlinear::TheorySolver | virtual |
| preprocessor() const | dlinear::TheorySolver | inline |
| preprocessor_ | dlinear::TheorySolver | protected |
| Reset() override | dlinear::NNSoplexTheorySolver | virtual |
| SetSPXVarCoeff(soplex::DSVectorRational &coeffs, const Variable &var, const mpq_class &value) const | dlinear::SoplexTheorySolver | protected |
| SoiToObjFunction() | dlinear::NNSoplexTheorySolver | private |
| spx_ | dlinear::SoplexTheorySolver | protected |
| spx_cols_ | dlinear::SoplexTheorySolver | protected |
| spx_rhs_ | dlinear::SoplexTheorySolver | protected |
| spx_rows_ | dlinear::SoplexTheorySolver | protected |
| spx_sense_ | dlinear::SoplexTheorySolver | protected |
| stats() const | dlinear::TheorySolver | inline |
| stats_ | dlinear::TheorySolver | protected |
| theory_bounds() const | dlinear::TheorySolver | inline |
| theory_col_count() const | dlinear::TheorySolver | inline |
| theory_col_to_var() const | dlinear::TheorySolver | inline |
| theory_col_to_var_ | dlinear::TheorySolver | protected |
| theory_row_count() const | dlinear::TheorySolver | inline |
| theory_row_to_lit() const | dlinear::TheorySolver | inline |
| theory_row_to_lit_ | dlinear::TheorySolver | protected |
| theory_rows_state_ | dlinear::TheorySolver | protected |
| TheorySolver(const PredicateAbstractor &predicate_abstractor, const std::string &class_name="TheorySolver") | dlinear::TheorySolver | explicit |
| UpdateExplanation(LiteralSet &explanation) override | dlinear::SoplexTheorySolver | protectedvirtual |
| UpdateExplanations(Explanations &explanations) | dlinear::TheorySolver | protected |
| UpdateModelBounds() override | dlinear::SoplexTheorySolver | protectedvirtual |
| UpdateModelSolution() override | dlinear::SoplexTheorySolver | protectedvirtual |
| var_to_theory_col() const | dlinear::TheorySolver | inline |
| var_to_theory_col_ | dlinear::TheorySolver | protected |
| Violation typedef | dlinear::TheorySolver | |