BoundPreprocessor.h

 
#pragma once
 
#include <iosfwd>
#include <list>
#include <map>
#include <set>
#include <span>
#include <tuple>
#include <unordered_map>
#include <utility>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/BoundVector.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/environment.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Config.h"
 
namespace dlinear {
 
class BoundPreprocessor {
 public:
  using Explanations = std::set<LiteralSet>;
  using VarToEqBinomialMap = std::unordered_map<Variable, mpq_class>;
 
  explicit BoundPreprocessor(const PredicateAbstractor& predicate_abstractor);
 
  void AddVariable(const Variable& var);
 
  std::set<LiteralSet> EnableLiterals(const std::vector<Literal>& enabled_literals);
  void EnableLiterals(const std::vector<Literal>& enabled_literals, std::set<LiteralSet>& explanation);
 
  std::set<LiteralSet> EnableLiteral(const Literal& lit);
  void EnableLiteral(const Literal& lit, std::set<LiteralSet>& explanations);
 
  Explanations Process();
  void Process(Explanations& explanations);
  Explanations Process(const LiteralSet& enabled_literals);
  void Process(const LiteralSet& enabled_literals, Explanations& explanations);
 
  void GetActiveExplanation(const Variable& var, LiteralSet& explanation);
 
  void SetInfinityBounds(const Variable& var, const mpq_class& lb, const mpq_class& ub);
 
  void Clear();
  void Clear(const BoundPreprocessor& fixed_preprocessor);
 
  [[nodiscard]] const Config& config() const { return config_; }
  [[nodiscard]] const BoundVectorMap& theory_bounds() const { return theory_bounds_; }
  [[nodiscard]] const PredicateAbstractor& predicate_abstractor() const { return predicate_abstractor_; }
  [[nodiscard]] const Environment& env() const { return env_; }
  [[nodiscard]] const IterationStats& stats() const { return stats_; }
 
  static bool IsSimpleBound(const Formula& formula);
  static bool IsEqualTo(const Formula& formula, bool truth = true);
  static bool IsNotEqualTo(const Formula& formula, bool truth = true);
  static bool IsGreaterThan(const Formula& formula, bool truth = true);
  static bool IsLessThan(const Formula& formula, bool truth = true);
  static bool IsGreaterThanOrEqualTo(const Formula& formula, bool truth = true);
  static bool IsLessThanOrEqualTo(const Formula& formula, bool truth = true);
 
  bool PropagateEqPolynomial(const Literal& lit, const Variable& var_to_propagate, Explanations& explanations);
  bool PropagateBoundsPolynomial(const Literal& lit, const Variable& var_to_propagate, Explanations& explanations);
 
  bool PropagateBoundsPolynomial(const Literal& lit, const Variable& var_to_propagate,
                                 const std::vector<Bound>& assumptions, Explanations& explanations);
 
 protected:
  const Variable* ShouldPropagateEqPolynomial(const Literal& lit) const;
  const Variable* ShouldPropagateEqPolynomial(const Formula& formula) const;
  const Variable* ShouldPropagateBoundsPolynomial(const Literal& lit) const;
  const Variable* ShouldPropagateBoundsPolynomial(const Formula& formula) const;
  bool ShouldEvaluate(const Literal& lit) const;
  bool ShouldEvaluate(const Formula& formula) const;
 
  Bound GetSimpleBound(const dlinear::Literal& lit) const;
  Bound GetSimpleBound(const Literal& lit, const Formula& formula) const;
 
  void PropagateConstraints(std::list<Literal>& enabled_literals, Explanations& explanations);
  void PropagateEqConstraints(std::list<Literal>& enabled_literals, Explanations& explanations);
  void PropagateBoundConstraints(std::list<Literal>& enabled_literals, Explanations& explanations);
  void EvaluateFormulas(std::list<Literal>& enabled_literals, Explanations& explanations);
  void FormulaViolationExplanation(const Literal& lit, const Formula& formula, Explanations& explanations);
 
  std::pair<Variable, Variable> ExtractBoundEdge(const Formula& formula) const;
  mpq_class ExtractEqBoundCoefficient(const Formula& formula) const;
 
  void GetExplanation(const Variable& var, LiteralSet& explanation);
 
  const mpq_class* StoreTemporaryMpq(const mpq_class& value);
 
#if DEBUGGING_PREPROCESSOR
  std::vector<Variable> GetExplanationOrigins(const Variable& var);
#endif
 
 private:
  std::list<mpq_class>
      temporary_mpq_vector_;  
 
  const Config& config_;  
  const PredicateAbstractor&
      predicate_abstractor_;  
 
  LiteralSet enabled_literals_;
 
  BoundVectorMap theory_bounds_;  
  Environment env_;               
 
  IterationStats stats_;  
};
 
std::ostream& operator<<(std::ostream& os, const BoundPreprocessor& preprocessor);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::BoundPreprocessor)
 
#endif