NaiveCnfizer.h

 
#pragma once
 
#include "dlinear/symbolic/FormulaVisitor.h"
#include "dlinear/symbolic/Nnfizer.h"
#include "dlinear/symbolic/symbolic.h"
 
namespace dlinear {
 
class NaiveCnfizer : public FormulaVisitor<> {
 public:
  explicit NaiveCnfizer(const Config &config) : FormulaVisitor{config, "NaiveCnfizer"} {}
 
  [[nodiscard]] Formula Process(const Formula &f) const;
  [[nodiscard]] Formula operator()(const Formula &f) const;
 
 private:
  [[nodiscard]] Formula VisitEqualTo(const Formula &f) const override;
  [[nodiscard]] Formula VisitNotEqualTo(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;
 
  Nnfizer nnfizer_{config_};  
};
 
}  // namespace dlinear