TseitinCnfizer.h

 
#pragma once
 
#include <map>
#include <vector>
 
#include "dlinear/symbolic/FormulaVisitor.h"
#include "dlinear/symbolic/NaiveCnfizer.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Config.h"
 
namespace dlinear {
 
class TseitinCnfizer : public FormulaVisitor<std::map<Variable, Formula> &> {
 public:
  explicit TseitinCnfizer(const Config &config) : FormulaVisitor{config, "TseitinCnfizer"}, naive_cnfizer_{config_} {}
 
  [[nodiscard]] std::vector<Formula> Process(const Formula &f) const;
  [[nodiscard]] std::vector<Formula> operator()(const Formula &f) const;
 
 private:
  [[nodiscard]] Formula VisitConjunction(const Formula &f, std::map<Variable, Formula> &map) const override;
  [[nodiscard]] Formula VisitDisjunction(const Formula &f, std::map<Variable, Formula> &map) const override;
  [[nodiscard]] Formula VisitNegation(const Formula &f, std::map<Variable, Formula> &map) const override;
  [[nodiscard]] Formula VisitForall(const Formula &f, std::map<Variable, Formula> &map) const override;
 
  const NaiveCnfizer naive_cnfizer_;  
};
 
}  // namespace dlinear