BoundImplicator.h

 
#pragma once
 
#include <compare>
#include <functional>
#include <map>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/LpRowSense.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Config.h"
#include "dlinear/util/SortedVector.hpp"
 
namespace dlinear {
 
class BoundImplicator {
 public:
  BoundImplicator(const Config& config, std::function<void(const Formula&)> assert,
                  const PredicateAbstractor& predicate_abstractor);
 
  void Propagate();
 
 private:
  struct Constraint {
    mpq_class value;           
    LpRowSense row_sense;      
    const Variable* variable;  
 
    std::strong_ordering operator<=>(const Constraint& o) const;
    bool operator==(const Constraint& o) const;
  };
 
  template <int NVariables>
  void AddAssertion(const Formula& assertion);
 
  void PropagateAssertions();
 
  const Config& config_;                                      
  const std::function<void(const Formula&)> assert_;          
  const PredicateAbstractor& predicate_abstractor_;           
  std::map<Variable, SortedVector<Constraint>> constraints_;  
};
 
}  // namespace dlinear