SATNonCNFMethod.h

Go to the documentation of this file.

#pragma once

#include <ostream>
#include <atomic>

#include "gsjj/passive/Method.h"

// Since limboole is written in C, we must force the compiler
extern "C" {
    #include "limboole/limboole.h"
}

namespace gsjj {
    namespace passive {
        namespace NonCNF {
            class SATNonCNFMethod : public Method {
            public:
                SATNonCNFMethod() = delete;
                virtual ~SATNonCNFMethod();

                virtual bool solve() override;

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

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

            protected:
                virtual std::string getFileName() const = 0;

                bool isSatisfiable() const;

                virtual bool createFormula(std::ostream &stream) = 0;

                virtual std::unique_ptr<DFA<char>> toDFA(std::istream &stream) const = 0;

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

            protected:
                const bool *mustStop;

            private:
                std::string getInputFile() const;
                std::string getOutputFile() const;
            };
        }
    }
}