SMTMethod.h

Go to the documentation of this file.

#pragma once

#include <map>

#include <cvc4/cvc4.h>

#include "gsjj/passive/Method.h"

namespace gsjj {
    namespace passive {
        namespace SMT {
            class SMTMethod : public Method {
            public:
                SMTMethod() = delete;
                virtual ~SMTMethod();

                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:
                CVC4::ExprManager m_exprManager;
                CVC4::SmtEngine m_SMTEngine;

            protected:
                virtual void createVariables() = 0;
                virtual CVC4::Expr createConstraints() = 0;
                virtual std::unique_ptr<DFA<char>> toDFA() = 0;

                SMTMethod(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);
            };
        }
    }
}