CompleteSoplexTheorySolver.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 <cstddef>
#include <map>
#include <set>
#include <string>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/solver/SoplexTheorySolver.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/util/BitIncrementIterator.h"
#include "dlinear/util/Box.h"
 
namespace dlinear {
 
class CompleteSoplexTheorySolver : public SoplexTheorySolver {
 public:
  explicit CompleteSoplexTheorySolver(PredicateAbstractor& predicate_abstractor,
                                      const std::string& class_name = "CompleteSoplexTheorySolver");
 
  Explanations EnableLiteral(const Literal& lit) override;
 
  void AddVariable(const Variable& var) override;
 
  void AddLiteral(const Variable& formula_var, const Formula& formula) override;
 
  SatResult CheckSatCore(mpq_class* actual_precision, Explanations& explanations) override;
 
  void Reset() override;
 
 private:
  static const mpq_class strict_col_lb_;  
  static const mpq_class strict_col_ub_;  
 
  void EnableSpxVarBound() override;
  void EnableSpxRow(int spx_row, bool truth) override;
 
  SatResult SpxCheckSat();
 
  void UpdateExplanationStrictInfeasible();
 
  void UpdateExplanationInfeasible();
 
  void Consolidate(const Box& box) override;
 
  void EnableNqLiteral(int spx_row, bool truth);
  void EnableNqLiterals(const std::vector<bool>& nq_status, bool force = false);
  void DisableNqLiterals(const std::set<std::size_t>& nq_constraints);
 
  bool UpdateBitIncrementIteratorBasedOnExplanation(BitIncrementIterator& bit_iterator);
 
  std::set<std::size_t> IteratorNqRowsInLastExplanation() const;
 
  void GetExplanation(Explanations& explanations);
 
  struct NqExplanation {
    explicit NqExplanation(std::size_t size);
    explicit NqExplanation(const std::set<std::size_t>& size);
    std::set<int> explanation;  
    std::vector<bool> visited;  
  };
 
  std::vector<int> nq_row_to_theory_rows_;  
  std::vector<bool> last_nq_status_;        
 
  std::set<int> last_theory_rows_to_explanation_;        
  std::set<std::set<int>> theory_rows_to_explanations_;  
 
  std::map<std::set<std::size_t>, NqExplanation> nq_explanations_;  
 
  bool locked_solver_;  
  std::set<std::pair<std::size_t, bool>> single_nq_rows_;  
};
 
}  // namespace dlinear