SATCNFMethod.h

Go to the documentation of this file.

#pragma once

#include "MapleCOMSPS_LRB/mtl/Vec.h"
#include "MapleCOMSPS_LRB/core/SolverTypes.h"
#include "MapleCOMSPS_LRB/simp/SimpSolver.h"

#include "gsjj/passive/Method.h"

namespace gsjj {
    namespace passive {
        namespace CNF {
            class SATCNFMethod : public Method {
            public:
                SATCNFMethod() = delete;
                virtual ~SATCNFMethod();

                bool solve() override;

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

                virtual void setStopTrigger(const std::chrono::seconds &timeLimit, std::atomic_bool &stopTrigger, const bool *stopPointer) override;
            
            protected:
                Minisat::Var newVariable();
                void addClause(const Minisat::vec<Minisat::Lit> &clause);

                virtual void createVariables() = 0;
                virtual void createClauses() = 0;

                virtual std::unique_ptr<DFA<char>> toDFA(const Minisat::vec<Minisat::lbool> &model) const = 0;

                SATCNFMethod(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::unique_ptr<Minisat::SimpSolver> m_solver;

                std::atomic_bool *mustStop;
            };
        }
    }
}