bdddict.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <list>
#include <set>
#include <map>
#include <iosfwd>
#include <bddx.h>
#include <vector>
#include <memory>
#include <spot/tl/formula.hh>
 
namespace spot
{
  class bdd_dict_priv;
 
  class SPOT_API bdd_dict
  {
    bdd_dict_priv* priv_;
  public:
 
    bdd_dict();
 
    ~bdd_dict();
 
    typedef std::map<formula, int> fv_map;
    typedef std::map<int, formula> vf_map;
 
    fv_map var_map; 
    fv_map acc_map; 
 
    typedef std::set<const void*> ref_set;
 
    enum var_type
    {
      anon = 0, 
      var,      
      acc       
    };
 
    struct bdd_info {
      bdd_info() noexcept: type(anon) {}
      var_type type; 
      formula f;     
      ref_set refs;  
    };
    typedef std::vector<bdd_info> bdd_info_map;
    bdd_info_map bdd_map;
 
    int register_proposition(formula f, const void* for_me);
 
    template <typename T>
    int register_proposition(formula f, std::shared_ptr<T> for_me)
    {
      return register_proposition(f, for_me.get());
    }
 
    int has_registered_proposition(formula f, const void* me);
 
    template <typename T>
    int has_registered_proposition(formula f, std::shared_ptr<T> for_me)
    {
      return has_registered_proposition(f, for_me.get());
    }
 
    // \brief Return the BDD variable number for a registered proposition.
    //
    // Throws std::out_of_range if \a f is not a known proposition.
    int varnum(formula f)
    {
      return var_map.at(f);
    }
 
    formula ap_from_var(int var) const
    {
      if (unsigned(var) < bdd_map.size()
          && bdd_map[var].type == bdd_dict::var)
        return bdd_map[var].f;
      return nullptr;
    }
 
    int register_acceptance_variable(formula f, const void* for_me);
 
    template <typename T>
    int register_acceptance_variable(formula f, std::shared_ptr<T> for_me)
    {
      return register_acceptance_variable(f, for_me.get());
    }
 
    int register_anonymous_variables(int n, const void* for_me);
 
    template <typename T>
    int register_anonymous_variables(int n, std::shared_ptr<T> for_me)
    {
      return register_anonymous_variables(n, for_me.get());
    }
 
    void register_all_variables_of(const void* from_other, const void* for_me);
 
    template <typename T>
    void register_all_variables_of(const void* from_other,
                                   std::shared_ptr<T> for_me)
    {
      register_all_variables_of(from_other, for_me.get());
    }
 
    template <typename T>
    void register_all_variables_of(std::shared_ptr<T> from_other,
                                   const void* for_me)
    {
      register_all_variables_of(from_other.get(), for_me);
    }
 
    template <typename T, typename U>
    void register_all_variables_of(std::shared_ptr<T> from_other,
                                   std::shared_ptr<U> for_me)
    {
      register_all_variables_of(from_other.get(), for_me.get());
    }
 
    void register_all_propositions_of(const void* from_other,
                                     const void* for_me);
 
    template <typename T>
    void register_all_propositions_of(const void* from_other,
                                      std::shared_ptr<T> for_me)
    {
      register_all_propositions_of(from_other, for_me.get());
    }
 
    template <typename T>
    void register_all_propositions_of(std::shared_ptr<T> from_other,
                                   const void* for_me)
    {
      register_all_propotitions_of(from_other.get(), for_me);
    }
 
    template <typename T, typename U>
    void register_all_propositions_of(std::shared_ptr<T> from_other,
                                      std::shared_ptr<U> for_me)
    {
      register_all_propositions_of(from_other.get(), for_me.get());
    }
 
    void unregister_all_my_variables(const void* me);
 
    void unregister_variable(int var, const void* me);
 
    template <typename T>
    void unregister_variable(int var, std::shared_ptr<T> me)
    {
      unregister_variable(var, me.get());
    }
 
    std::ostream& dump(std::ostream& os) const;
 
    void assert_emptiness() const;
 
  private:
    // Disallow copy.
    bdd_dict(const bdd_dict& other) = delete;
    bdd_dict& operator=(const bdd_dict& other) = delete;
  };
 
  typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
 
  inline bdd_dict_ptr make_bdd_dict()
  {
    return std::make_shared<bdd_dict>();
  }
 
  class bdd_dict_preorder
  {
  public:
    bdd_dict_preorder() = default;
    bdd_dict_preorder(bdd_dict_ptr dict)
      : dict_(dict)
    {
    }
 
    operator bdd_dict_ptr() const
    {
      return dict_;
    }
 
    bdd_dict_ptr get_dict() const
    {
      return dict_;
    }
 
    int register_proposition(formula f)
    {
      return dict_->register_proposition(f, this);
    }
 
    int register_proposition(const std::string& f)
    {
      return register_proposition(formula::ap(f));
    }
 
    ~bdd_dict_preorder()
    {
      dict_->unregister_all_my_variables(this);
    }
 
  private:
    bdd_dict_ptr dict_ = make_bdd_dict();
  };
 
}