BinaryCNFMethod.h

Go to the documentation of this file.

#pragma once

#include "bcsat/bc.hh"
 
#include "gsjj/passive/Method.h"
#include "gsjj/passive/MethodFactory.h"

namespace gsjj {
    namespace passive {
        namespace CNF {
            class BinaryCNFMethod : public Method, public RegisterInFactory<BinaryCNFMethod> {
            public:
                BinaryCNFMethod() = delete;
                virtual ~BinaryCNFMethod();

                bool solve() override;

                std::unique_ptr<DFA<char>> constructDFA() override;

                static std::string getFactoryName();

                virtual void setStopTrigger(const std::chrono::seconds &timeLimit, std::atomic_bool &stopTrigger, const bool *stopPointer) override;

            protected:
                typedef std::map<std::pair<std::string, unsigned int>, Gate*> m_mapType;

            protected:
                BinaryCNFMethod(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);

                virtual void createVariables();
                virtual Gate* createFormula();

                Gate* equal(const std::string &u, const std::string &v);
                Gate* phi_different(const std::string &u, const std::string &v);
                Gate* phi_not_q_i(const std::string &u, unsigned int i);

                unsigned int toState(const std::string &u) const;

                std::unique_ptr<DFA<char>> toDFA() const;

            protected:
                std::unique_ptr<BC> m_solver;
                SimplifyOptions m_simplify_opts;
                unsigned int m_binarySize;
                m_mapType m_stateToVar;
            };
        }
    }
}