dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
dlinear::CompleteSoplexTheorySolver Member List

This is the complete list of members for dlinear::CompleteSoplexTheorySolver, including all inherited members.

AddLiteral(const Variable &formula_var, const Formula &formula) overridedlinear::CompleteSoplexTheorySolvervirtual
AddLiterals() overridedlinear::SoplexTheorySolvervirtual
AddVariable(const Variable &var) overridedlinear::CompleteSoplexTheorySolvervirtual
Bound typedefdlinear::TheorySolver
BoundViolationType enum namedlinear::TheorySolverprotected
CheckSat(const Box &box, mpq_class *actual_precision, std::set< LiteralSet > &explanations)dlinear::TheorySolver
dlinear::SoplexTheorySolver::CheckSatCore(mpq_class *actual_precision, std::set< LiteralSet > &explanations)=0dlinear::TheorySolverpure virtual
config() constdlinear::TheorySolverinline
config_dlinear::TheorySolverprotected
Consolidate(const Box &box) overridedlinear::CompleteSoplexTheorySolverprivatevirtual
DisableNqLiterals(const std::set< std::size_t > &nq_constraints)dlinear::CompleteSoplexTheorySolverprivate
DisableSpxRows()dlinear::SoplexTheorySolverprotected
enabled_literals() constdlinear::TheorySolver
EnableLiteral(const Literal &lit) overridedlinear::CompleteSoplexTheorySolvervirtual
EnableLiterals(std::span< const Literal > theory_literals)dlinear::TheorySolver
EnableNqLiteral(int spx_row, bool truth)dlinear::CompleteSoplexTheorySolverprivate
EnableNqLiterals(const std::vector< bool > &nq_status, bool force=false)dlinear::CompleteSoplexTheorySolverprivate
EnableSpxRow(int spx_row, bool truth) overridedlinear::CompleteSoplexTheorySolverprivatevirtual
dlinear::SoplexTheorySolver::EnableSpxRow(int spx_row)dlinear::SoplexTheorySolverprotected
EnableSpxVarBound() overridedlinear::CompleteSoplexTheorySolverprivatevirtual
Explanations typedefdlinear::TheorySolver
fixed_preprocessor() constdlinear::TheorySolverinline
fixed_preprocessor_dlinear::TheorySolverprotected
fixed_theory_bounds() constdlinear::TheorySolverinline
GetActiveRows()dlinear::SoplexTheorySolverprotected
GetActiveRows(const std::vector< int > &spx_rows)dlinear::SoplexTheorySolverprotected
GetExplanation(Explanations &explanations)dlinear::CompleteSoplexTheorySolverprivate
GetSpxInfeasibilityRay(soplex::VectorRational &farkas_ray)dlinear::SoplexTheorySolverprotected
GetSpxInfeasibilityRay(soplex::VectorRational &farkas_ray, std::vector< BoundViolationType > &bounds_ray)dlinear::SoplexTheorySolverprotected
infinity_dlinear::SoplexTheorySolverprotectedstatic
is_consolidated_dlinear::TheorySolverprotected
IsRowActive(int spx_row)dlinear::SoplexTheorySolverprotected
IsRowActive(int spx_row, const soplex::Rational &value)dlinear::SoplexTheorySolverprotected
IteratorNqRowsInLastExplanation() constdlinear::CompleteSoplexTheorySolverprivate
last_nq_status_dlinear::CompleteSoplexTheorySolverprivate
last_theory_rows_to_explanation_dlinear::CompleteSoplexTheorySolverprivate
lit_to_theory_row() constdlinear::TheorySolverinline
lit_to_theory_row_dlinear::TheorySolverprotected
locked_solver_dlinear::CompleteSoplexTheorySolverprivate
m_fixed_preprocessor()dlinear::TheorySolverinline
m_preprocessor()dlinear::TheorySolverinline
model() constdlinear::TheorySolver
model_dlinear::TheorySolverprotected
ninfinity_dlinear::SoplexTheorySolverprotectedstatic
nq_explanations_dlinear::CompleteSoplexTheorySolverprivate
nq_row_to_theory_rows_dlinear::CompleteSoplexTheorySolverprivate
ParseRowCoeff(const Formula &formula)dlinear::SoplexTheorySolverprotected
predicate_abstractor() constdlinear::TheorySolverinline
predicate_abstractor_dlinear::TheorySolverprotected
PreprocessFixedLiterals(const LiteralSet &fixed_literals)dlinear::TheorySolvervirtual
preprocessor() constdlinear::TheorySolverinline
preprocessor_dlinear::TheorySolverprotected
Reset() overridedlinear::CompleteSoplexTheorySolvervirtual
SetSPXVarCoeff(soplex::DSVectorRational &coeffs, const Variable &var, const mpq_class &value) constdlinear::SoplexTheorySolverprotected
single_nq_rows_dlinear::CompleteSoplexTheorySolverprivate
spx_dlinear::SoplexTheorySolverprotected
spx_cols_dlinear::SoplexTheorySolverprotected
spx_rhs_dlinear::SoplexTheorySolverprotected
spx_rows_dlinear::SoplexTheorySolverprotected
spx_sense_dlinear::SoplexTheorySolverprotected
SpxCheckSat()dlinear::CompleteSoplexTheorySolverprivate
stats() constdlinear::TheorySolverinline
stats_dlinear::TheorySolverprotected
strict_col_lb_dlinear::CompleteSoplexTheorySolverprivatestatic
strict_col_ub_dlinear::CompleteSoplexTheorySolverprivatestatic
theory_bounds() constdlinear::TheorySolverinline
theory_col_count() constdlinear::TheorySolverinline
theory_col_to_var() constdlinear::TheorySolverinline
theory_col_to_var_dlinear::TheorySolverprotected
theory_row_count() constdlinear::TheorySolverinline
theory_row_to_lit() constdlinear::TheorySolverinline
theory_row_to_lit_dlinear::TheorySolverprotected
theory_rows_state_dlinear::TheorySolverprotected
theory_rows_to_explanations_dlinear::CompleteSoplexTheorySolverprivate
TheorySolver(const PredicateAbstractor &predicate_abstractor, const std::string &class_name="TheorySolver")dlinear::TheorySolverexplicit
UpdateBitIncrementIteratorBasedOnExplanation(BitIncrementIterator &bit_iterator)dlinear::CompleteSoplexTheorySolverprivate
UpdateExplanation(LiteralSet &explanation) overridedlinear::SoplexTheorySolverprotectedvirtual
UpdateExplanationInfeasible()dlinear::CompleteSoplexTheorySolverprivate
UpdateExplanations(Explanations &explanations)dlinear::TheorySolverprotected
UpdateExplanationStrictInfeasible()dlinear::CompleteSoplexTheorySolverprivate
UpdateModelBounds() overridedlinear::SoplexTheorySolverprotectedvirtual
UpdateModelSolution() overridedlinear::SoplexTheorySolverprotectedvirtual
var_to_theory_col() constdlinear::TheorySolverinline
var_to_theory_col_dlinear::TheorySolverprotected
Violation typedefdlinear::TheorySolver