aiger.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 <iosfwd>
#include <spot/misc/common.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twa/fwd.hh>
#include <spot/twa/bdddict.hh>
#include <spot/tl/formula.hh>
#include <spot/tl/apcollect.hh>
 
#include <unordered_map>
#include <vector>
#include <set>
#include <memory>
#include <algorithm> // std::none_of
#include <sstream>
 
 
namespace spot
{
  // Forward for synthesis
  struct mealy_like;
 
  class aig;
 
  typedef std::shared_ptr<aig> aig_ptr;
  typedef std::shared_ptr<const aig> const_aig_ptr;
 
  class SPOT_API aig
  {
  protected:
    const unsigned num_inputs_;
    const unsigned num_outputs_;
    const unsigned num_latches_;
    const std::vector<std::string> input_names_;
    const std::vector<std::string> output_names_;
    unsigned max_var_;
 
    std::vector<unsigned> next_latches_;
    std::vector<unsigned> outputs_;
    std::vector<std::pair<unsigned, unsigned>> and_gates_;
    bdd_dict_ptr dict_;
    // Cache the function computed by each variable as a bdd.
    // Bidirectional map
    std::unordered_map<unsigned, bdd> var2bdd_;
    std::unordered_map<int, unsigned> bdd2var_; //uses id
    // First anonymous var marking the beginning of variables used
    // as latches
    int l0_;
 
    bdd all_ins_;
    bdd all_latches_;
 
    // For simulation
    std::vector<bool> state_;
 
  public:
 
    using safe_point = std::pair<unsigned, unsigned>;
    using safe_stash =
            std::tuple<std::vector<std::pair<unsigned, unsigned>>,
                       std::vector<std::pair<unsigned, bdd>>,
                       std::vector<bdd>>;
 
    aig(const std::vector<std::string>& inputs,
        const std::vector<std::string>& outputs,
        unsigned num_latches,
        bdd_dict_ptr dict = make_bdd_dict());
 
    aig(unsigned num_inputs, unsigned num_outputs,
        unsigned num_latches, bdd_dict_ptr dict = make_bdd_dict());
 
    ~aig()
    {
      dict_->unregister_all_my_variables(this);
    }
 
  protected:
    void register_new_lit_(unsigned v, const bdd &b);
    void register_latch_(unsigned i, const bdd& b);
    void register_input_(unsigned i, const bdd& b);
    void unregister_lit_(unsigned v);
 
    void split_cond_(const bdd& b, char so_mode,
                     std::vector<bdd>& cond_parts);
 
    bdd accum_common_(const bdd& b) const;
 
    unsigned cube2var_(const bdd& b, const int use_split_off);
 
  public:
 
    safe_point get_safe_point_() const;
 
    safe_stash roll_back_(safe_point sp,
                          bool do_stash = false);
    void reapply_(safe_point sp, const safe_stash& ss);
 
    unsigned num_outputs() const
    {
      return num_outputs_;
    }
    const std::vector<unsigned>& outputs() const
    {
      SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(),
                               [](unsigned o){return o == -1u; }));
      return outputs_;
    }
 
    unsigned output(unsigned num) const
    {
      return outputs_[num];
    }
 
    const std::vector<std::string>& output_names() const
    {
      return output_names_;
    }
 
    unsigned num_inputs() const
    {
      return num_inputs_;
    }
    const std::vector<std::string>& input_names() const
    {
      return input_names_;
    }
 
    unsigned num_latches() const
    {
      return num_latches_;
    }
    const std::vector<unsigned>& next_latches() const
    {
      SPOT_ASSERT(std::none_of(next_latches_.begin(), next_latches_.end(),
                               [](unsigned o){return o == -1u; }));
      return next_latches_;
    };
 
    unsigned num_gates() const
    {
      return and_gates_.size();
    };
    const std::vector<std::pair<unsigned, unsigned>>& gates() const
    {
      return and_gates_;
    };
 
    unsigned max_var() const
    {
      return max_var_;
    };
 
    unsigned input_var(unsigned i, bool neg = false) const
    {
      SPOT_ASSERT(i < num_inputs_);
      return (1 + i) * 2 + neg;
    }
    bdd input_bdd(unsigned i, bool neg = false) const
    {
      return aigvar2bdd(input_var(i, neg));
    }
 
    unsigned latch_var(unsigned i, bool neg = false) const
    {
      SPOT_ASSERT(i < num_latches_);
      return (1 + num_inputs_ + i) * 2 + neg;
    }
    bdd latch_bdd(unsigned i, bool neg = false) const
    {
      return aigvar2bdd(latch_var(i, neg));
    }
 
    unsigned gate_var(unsigned i, bool neg = false) const
    {
      SPOT_ASSERT(i < num_gates());
      return (1 + num_inputs_ + num_latches_ + i) * 2 + neg;
    }
    bdd gate_bdd(unsigned i, bool neg = false) const
    {
      return aigvar2bdd(gate_var(i, neg));
    }
 
    bdd aigvar2bdd(unsigned v, bool neg = false) const
    {
      return neg ? bdd_not(var2bdd_.at(v)) : var2bdd_.at(v);
    }
 
    unsigned bdd2aigvar(const bdd& b) const
    {
      return bdd2var_.at(b.id());
    }
 
    unsigned bdd2INFvar(const bdd& b);
 
    unsigned bdd2ISOPvar(const bdd& b, const int use_split_off = 0);
 
    unsigned encode_bdd(const std::vector<bdd>& c_alt,
                        char method = 1, bool use_dual = false,
                        int use_split_off = 0);
 
    unsigned encode_bdd(const bdd& b,
                        char method = 1, bool use_dual = false,
                        int use_split_off = 0);
 
    void set_output(unsigned i, unsigned v);
 
    void set_next_latch(unsigned i, unsigned v);
 
    static constexpr unsigned aig_true() noexcept
    {
      return 1;
    };
 
    static constexpr unsigned aig_false() noexcept
    {
      return 0;
    };
 
    unsigned aig_not(unsigned v);
 
    unsigned aig_and(unsigned v1, unsigned v2);
 
    unsigned aig_and(std::vector<unsigned>& vs);
 
    unsigned aig_or(unsigned v1, unsigned v2);
 
    unsigned aig_or(std::vector<unsigned>& vs);
 
    unsigned aig_pos(unsigned v);
 
    void encode_all_bdds(const std::vector<bdd>& all_bdd);
 
    static aig_ptr
    parse_aag(const std::string& aig_file,
              bdd_dict_ptr dict = make_bdd_dict());
 
    static aig_ptr
    parse_aag(const char* data,
              const std::string& filename,
              bdd_dict_ptr dict = make_bdd_dict());
 
    static aig_ptr
    parse_aag(std::istream& iss,
              const std::string& filename,
              bdd_dict_ptr dict = make_bdd_dict());
 
    twa_graph_ptr as_automaton(bool keepsplit = false) const;
 
    const std::vector<bool>& circ_state() const
    {
      SPOT_ASSERT(state_.size() == max_var_ + 2
                  && "State vector does not have the correct size.\n"
                     "Forgot to initialize?");
      return state_;
    }
 
    bool circ_state_of(unsigned var) const
    {
      SPOT_ASSERT(var <= max_var_ + 1
                  && "Variable out of range");
      return circ_state()[var];
    }
 
    void circ_init();
 
    void circ_step(const std::vector<bool>& inputs);
 
  };
 
  SPOT_API aig_ptr
  mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode);
  SPOT_API aig_ptr
  mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode,
                       const std::vector<std::string>& ins,
                       const std::vector<std::string>& outs,
                       const realizability_simplifier* rs = nullptr);
 
  SPOT_API aig_ptr
  mealy_machine_to_aig(const mealy_like& m, const char* mode);
  SPOT_API aig_ptr
  mealy_machine_to_aig(mealy_like& m, const char *mode,
                       const std::vector<std::string>& ins,
                       const std::vector<std::string>& outs,
                       const realizability_simplifier* rs = nullptr);
 
  SPOT_API aig_ptr
  mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
                        const char* mode);
  SPOT_API aig_ptr
  mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
                        const char* mode);
  SPOT_API aig_ptr
  mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
                        const char* mode,
                        const std::vector<std::string>& ins,
                        const std::vector<std::vector<std::string>>& outs,
                        const realizability_simplifier* rs = nullptr);
  SPOT_API aig_ptr
  mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
                        const char* mode,
                        const std::vector<std::string>& ins,
                        const std::vector<std::vector<std::string>>& outs,
                        const realizability_simplifier* rs = nullptr);
 
  SPOT_API std::ostream&
  print_aiger(std::ostream& os, const_aig_ptr circuit);
 
  SPOT_API std::ostream&
  print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
              const char* mode);
}