PlaistedGreenbaumCnfizer.h

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