TheorySolver.h

 
#pragma once
 
#include <map>
#include <set>
#include <string>
#include <tuple>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/BoundIterator.h"
#include "dlinear/solver/BoundPreprocessor.h"
#include "dlinear/solver/LpColBound.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Config.h"
#include "dlinear/util/Stats.h"
 
namespace dlinear {
 
class TheorySolver {
 public:
  using Bound = std::tuple<const Variable &, LpColBound, const mpq_class &>;  
  using Violation = BoundIterator;            
  using Explanations = std::set<LiteralSet>;  
  explicit TheorySolver(const PredicateAbstractor &predicate_abstractor,
                        const std::string &class_name = "TheorySolver");
  virtual ~TheorySolver() = default;
 
  virtual void AddLiterals();
  virtual void AddLiteral(const Variable &formula_var, const Formula &formula) = 0;
  virtual Explanations PreprocessFixedLiterals(const LiteralSet &fixed_literals);
  virtual void AddVariable(const Variable &var) = 0;
  Explanations EnableLiterals(std::span<const Literal> theory_literals);
  virtual Explanations EnableLiteral(const Literal &lit) = 0;
 
  [[nodiscard]] const Box &model() const;
  [[nodiscard]] const Config &config() const { return config_; }
  [[nodiscard]] const PredicateAbstractor &predicate_abstractor() const { return predicate_abstractor_; }
  [[nodiscard]] const std::map<Variable::Id, int> &var_to_theory_col() const { return var_to_theory_col_; }
  [[nodiscard]] const std::vector<Variable> &theory_col_to_var() const { return theory_col_to_var_; }
  [[nodiscard]] const std::map<Variable::Id, int> &lit_to_theory_row() const { return lit_to_theory_row_; }
  [[nodiscard]] const std::vector<Literal> &theory_row_to_lit() const { return theory_row_to_lit_; }
  [[nodiscard]] const BoundVectorMap &theory_bounds() const { return preprocessor_.theory_bounds(); }
  [[nodiscard]] const BoundVectorMap &fixed_theory_bounds() const { return fixed_preprocessor_.theory_bounds(); }
  [[nodiscard]] const BoundPreprocessor &preprocessor() const { return preprocessor_; }
  [[nodiscard]] BoundPreprocessor &m_preprocessor() { return preprocessor_; }
  [[nodiscard]] const BoundPreprocessor &fixed_preprocessor() const { return fixed_preprocessor_; }
  [[nodiscard]] BoundPreprocessor &m_fixed_preprocessor() { return fixed_preprocessor_; }
  [[nodiscard]] std::size_t theory_row_count() const { return theory_row_to_lit_.size(); }
  [[nodiscard]] std::size_t theory_col_count() const { return theory_col_to_var_.size(); }
  [[nodiscard]] std::set<Literal> enabled_literals() const;
 
  SatResult CheckSat(const Box &box, mpq_class *actual_precision, std::set<LiteralSet> &explanations);
  virtual SatResult CheckSatCore(mpq_class *actual_precision, std::set<LiteralSet> &explanations) = 0;
 
  virtual void Consolidate(const Box &box);
 
  virtual void Reset();
 
  [[nodiscard]] const IterationStats &stats() const { return stats_; }
 
#ifndef NDEBUG
  void DumpEnabledLiterals();
#endif
 
 protected:
  enum class BoundViolationType {
    NO_BOUND_VIOLATION,     
    LOWER_BOUND_VIOLATION,  
    UPPER_BOUND_VIOLATION,  //< The upper bound is involved in the infeasibility
  };
 
  void BoundsToTheoryRows(const Variable &var, const mpq_class &value, std::set<int> &theory_rows) const;
  void BoundsToTheoryRows(const Variable &var, BoundViolationType type, std::set<int> &bound_idxs) const;
  virtual void UpdateModelSolution() = 0;
  virtual void UpdateModelBounds() = 0;
  virtual void UpdateExplanation(LiteralSet &explanation) = 0;
  void UpdateExplanations(Explanations &explanations);
 
  const Config &config_;  
 
  bool is_consolidated_;  
 
  const PredicateAbstractor &predicate_abstractor_;  
 
  std::map<Variable::Id, int> var_to_theory_col_;  
  std::vector<Variable> theory_col_to_var_;        
  std::map<Variable::Id, int> lit_to_theory_row_;  
  std::vector<Literal> theory_row_to_lit_;         
  std::vector<bool> theory_rows_state_;            
 
 
  BoundPreprocessor fixed_preprocessor_;  
  BoundPreprocessor preprocessor_;        
  //< It will be reset to the @ref fixed_preprocessor_ at every iteration.
 
  Box model_;  
 
  IterationStats stats_;  
};
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::TheorySolver::Bound)
 
#endif