SoplexTheorySolver.h

 
#pragma once
 
#ifndef DLINEAR_ENABLED_SOPLEX
#error SoPlex is not enabled. Please enable it by adding "--//tools:enable_soplex" to the bazel command.
#endif
 
#include <optional>
#include <string>
#include <utility>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/libs/libsoplex.h"
#include "dlinear/solver/LpRowSense.h"
#include "dlinear/solver/TheorySolver.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Box.h"
 
namespace dlinear {
 
class SoplexTheorySolver : public TheorySolver {
 public:
  explicit SoplexTheorySolver(PredicateAbstractor& predicate_abstractor,
                              const std::string& class_name = "SoplexTheorySolver");
 
  void AddVariable(const Variable& var) override;
  void AddLiterals() override;
  void Consolidate(const Box& box) override;
  void Reset() override;
 
 protected:
  static mpq_class infinity_;   
  static mpq_class ninfinity_;  
 
  void UpdateModelBounds() override;
  void UpdateModelSolution() override;
  void UpdateExplanation(LiteralSet& explanation) override;
 
  virtual void EnableSpxVarBound();
 
  void EnableSpxRow(int spx_row);
  virtual void EnableSpxRow(int spx_row, bool truth) = 0;
 
  void DisableSpxRows();
 
  soplex::DSVectorRational ParseRowCoeff(const Formula& formula);
  void SetSPXVarCoeff(soplex::DSVectorRational& coeffs, const Variable& var, const mpq_class& value) const;
  void CreateArtificials(int spx_row);
 
  void GetSpxInfeasibilityRay(soplex::VectorRational& farkas_ray);
  void GetSpxInfeasibilityRay(soplex::VectorRational& farkas_ray, std::vector<BoundViolationType>& bounds_ray);
 
  std::vector<std::pair<int, soplex::Rational>> GetActiveRows();
  std::vector<std::pair<int, soplex::Rational>> GetActiveRows(const std::vector<int>& spx_rows);
  std::optional<soplex::Rational> IsRowActive(int spx_row);
  bool IsRowActive(int spx_row, const soplex::Rational& value);
 
  soplex::SoPlex spx_;  
 
  soplex::LPColSetRational spx_cols_;  
  soplex::LPRowSetRational spx_rows_;  
 
  std::vector<mpq_class> spx_rhs_;     
  std::vector<LpRowSense> spx_sense_;  
};
 
}  // namespace dlinear