QsoptexTheorySolver.h

 
#pragma once
 
#ifndef DLINEAR_ENABLED_QSOPTEX
#error QSopt_ex is not enabled. Please enable it by adding "--//tools:enable_qsoptex" to the bazel command.
#endif
 
#include <vector>
 
#include "dlinear/libs/libqsopt_ex.h"
#include "dlinear/solver/LpRowSense.h"
#include "dlinear/solver/TheorySolver.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Box.h"
 
namespace dlinear {
 
extern "C" void QsoptexCheckSatPartialSolution(mpq_QSdata const *prob, mpq_t *x, const mpq_t infeas, const mpq_t delta,
                                               void *data);
class QsoptexTheorySolver : public TheorySolver {
 public:
  explicit QsoptexTheorySolver(PredicateAbstractor &predicate_abstractor,
                               const std::string &class_name = "QsoptexTheorySolver");
  ~QsoptexTheorySolver() override;
 
  void AddVariable(const Variable &var) override;
  void AddLiterals() override;
  void Consolidate(const Box &box) override;
 
 protected:
  void UpdateModelBounds() override;
  void UpdateModelSolution() override;
  void UpdateExplanation(LiteralSet &explanation) override;
 
  void EnableQsxVarBound();
  void EnableQsxRow(int qsx_row);
  virtual void EnableQsxRow(int qsx_row, bool truth) = 0;
 
  void DisableQsxRows();
  void SetRowCoeff(const Formula &formula, int qsx_row);
 
  void SetQsxVarCoeff(int qsx_row, const Variable &var, const mpq_class &value);
 
  void SetQsxVarObjCoeff(const Variable &var, const mpq_class &value);
 
  void SetLinearObjective(const Expression &expr);
  void ClearLinearObjective();
 
  // Exact LP solver (QSopt_ex)
  mpq_QSprob qsx_;
 
  std::vector<mpq_class> qsx_rhs_;     
  std::vector<LpRowSense> qsx_sense_;  
 
  qsopt_ex::MpqArray ray_;  
  qsopt_ex::MpqArray x_;    
};
 
void QsoptexCheckSatPartialSolution(mpq_QSdata const *prob, mpq_t *x, const mpq_t infeas, const mpq_t delta,
                                    void *data);
}  // namespace dlinear