libgsjj  1
Deterministic finite automata learning library
UnaryNonCNFMethod.h
Go to the documentation of this file.
1 #pragma once
2 
5 
6 namespace gsjj {
7  namespace passive {
8  namespace NonCNF {
14  class UnaryNonCNFMethod : public SATNonCNFMethod, public RegisterInFactory<UnaryNonCNFMethod> {
15  public:
16  UnaryNonCNFMethod() = delete;
18 
19  static std::string getFactoryName();
20 
21  protected:
22  virtual bool createFormula(std::ostream &stream) override;
23  std::unique_ptr<DFA<char>> toDFA(std::istream &stream) const override;
24  virtual std::string getFileName() const override;
25 
26  UnaryNonCNFMethod(const std::set<std::string> &SpSet, const std::set<std::string> &SmSet, const std::set<std::string> &SSet, const std::set<std::string> &prefixesSet, const std::set<char> &alphabetSet, unsigned int n);
27  };
28  }
29  }
30 }
The namespace of the library.
Definition: binary.h:11
virtual std::string getFileName() const override
Gives the name of the file in which the boolean formula must be written.
The Grinchtein, Leucker and Piterman&#39;s unary method.
virtual bool createFormula(std::ostream &stream) override
Creates the boolean formula (must not be in CNF) and writes it in the stream.
Helps to register a method in the factory.
Definition: MethodFactory.h:84
Base class for every method that relies on a non-CNF SAT solver.
std::unique_ptr< DFA< char > > toDFA(std::istream &stream) const override
Effectively creates the DFA.