UnaryCNFMethod.h

Go to the documentation of this file.

#pragma once

#include "gsjj/passive/CNF/SATCNFMethod.h"
#include "gsjj/passive/MethodFactory.h"

namespace gsjj {
    namespace passive {
        namespace CNF {
            class UnaryCNFMethod : public SATCNFMethod, public RegisterInFactory<UnaryCNFMethod> {
            public:
                UnaryCNFMethod() = delete;
                ~UnaryCNFMethod();

                static std::string getFactoryName();

            protected:
                void createVariables() override;
                void createClauses() override;
                std::unique_ptr<DFA<char>> toDFA(const Minisat::vec<Minisat::lbool> &model) const override;

                UnaryCNFMethod(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);

            private:
                typedef std::map<std::pair<std::string, unsigned int>, Minisat::Var> states_map;
                typedef states_map::value_type state;

            private:
                states_map m_stateName;
            };
        }
    }
}