Synthesizer.h

#ifndef SYNTHESIZER_H
#define SYNTHESIZER_H
 
#include <memory>
 
#include "game/Transducer.h"
#include <tuple>
#include <optional>
 
 
namespace Syft {
 
    static const std::string REALIZABLE_STR = "REALIZABLE";
    static const std::string UNREALIZABLE_STR = "UNREALIZABLE";
 
    struct SynthesisResult {
        bool realizability;
        CUDD::BDD winning_states;
        CUDD::BDD winning_moves;
        std::unique_ptr<Transducer> transducer;
        CUDD::BDD safe_states;
    };
 
    struct MaxSetSynthesisResult {
        bool realizability;
        CUDD::BDD deferring_strategy;
        CUDD::BDD nondeferring_strategy;
    };
 
    struct OneStepSynthesisResult {
        std::optional<bool> realizability = std::nullopt;
        CUDD::BDD winning_move;
    };
 
    template<class Spec>
    class Synthesizer {
    protected:
        Spec spec_;
 
    public:
 
        Synthesizer(Spec spec)
                : spec_(std::move(spec)) {}
 
 
        virtual ~Synthesizer() {}
 
        virtual SynthesisResult run() const = 0;
    };
 
}
 
#endif // SYNTHESIZER_H