PredicateAbstractor.h

 
#pragma once
 
#include <unordered_map>
#include <vector>
 
#include "dlinear/symbolic/FormulaVisitor.h"
#include "dlinear/symbolic/LinearFormulaFlattener.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Config.h"
 
namespace dlinear {
 
class PredicateAbstractor : public FormulaVisitor<> {
 public:
  explicit PredicateAbstractor(const Config &config)
      : FormulaVisitor{config, "PredicateAbstractor"}, flattener_{config} {}
  [[nodiscard]] Formula Process(const Formula &f);
  [[nodiscard]] Formula operator()(const Formula &f);
 
  [[nodiscard]] Formula Process(const std::vector<Formula> &formulas);
  [[nodiscard]] Formula operator()(const std::vector<Formula> &formulas);
 
  [[nodiscard]] const std::unordered_map<Variable, Formula> &var_to_formula_map() const { return var_to_formula_map_; }
 
  [[nodiscard]] const Variable &operator[](const Formula &f) const { return formula_to_var_map_.at(f); }
  [[nodiscard]] const Formula &operator[](const Variable &var) const { return var_to_formula_map_.at(var); }
 
 private:
  [[nodiscard]] Formula VisitFormula(const Formula &f) const override;
  [[nodiscard]] Formula VisitAtomic(const Formula &f) const;
  [[nodiscard]] Formula VisitEqualTo(const Formula &f) const override;
  [[nodiscard]] Formula VisitNotEqualTo(const Formula &f) const override;
  [[nodiscard]] Formula VisitGreaterThan(const Formula &f) const override;
  [[nodiscard]] Formula VisitGreaterThanOrEqualTo(const Formula &f) const override;
  [[nodiscard]] Formula VisitLessThan(const Formula &f) const override;
  [[nodiscard]] Formula VisitLessThanOrEqualTo(const Formula &f) const override;
  [[nodiscard]] Formula VisitConjunction(const Formula &f) const override;
  [[nodiscard]] Formula VisitDisjunction(const Formula &f) const override;
  [[nodiscard]] Formula VisitNegation(const Formula &f) const override;
  [[nodiscard]] Formula VisitForall(const Formula &f) const override;
 
  mutable std::unordered_map<Variable, Formula>
      var_to_formula_map_;  
  mutable std::unordered_map<Formula, Variable>
      formula_to_var_map_;                    
  mutable LinearFormulaFlattener flattener_;  
};
 
}  // namespace dlinear