BinaryNonCNFMethod.h

Go to the documentation of this file.

#pragma once

#include <vector>

#include "gsjj/passive/NonCNF/SATNonCNFMethod.h"
#include "gsjj/passive/MethodFactory.h"

namespace gsjj {
    namespace passive {
        namespace NonCNF {
            class BinaryNonCNFMethod : public SATNonCNFMethod, public RegisterInFactory<BinaryNonCNFMethod> {
            public:
                BinaryNonCNFMethod() = delete;
                ~BinaryNonCNFMethod();

                static std::string getFactoryName();

            protected:
                virtual bool createFormula(std::ostream &stream) override;
                virtual std::unique_ptr<DFA<char>> toDFA(std::istream &stream) const override;
                virtual std::string getFileName() const override;

                BinaryNonCNFMethod(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:
                std::string phi_different(std::string pref1, std::string pref2);
                std::string phi_not_q_i(std::string pref, unsigned int i);
                typedef std::map<std::pair<std::string, unsigned int>, unsigned int> states_map;
                typedef states_map::value_type state;
            };
        }
    }
}