Symbolic `pick_cube`

[SSoelvsten]

For some model checking algorithms, one needs to be able to obtain a BDD for a single state, i.e. a single satisfying assignment. In BuDDy, these are the two functions:

• bdd_satone(f): Create a cube with a satisfying assignment (can be multiple within the total domain of variables).
• bdd_satoneset(f, vars): Create a cube with a satisfying assignment. Variables not mentioned in f but mentioned in vars are also added to the result (preferably based on the polarity of each respective variable in vars).

[SSoelvsten]

Indeed, you can fake it (but without the polarity) with this piece of code, but it can be much faster (and more pleasant to the end user) by not having to convert back and forth between different data structures.

  inline oxidd::bdd_function
  satone(const oxidd::bdd_function& f)
  {
    oxidd::util::assignment sat = f.pick_cube();

    oxidd::bdd_function res = top();
    for (int x = sat.size() - 1; 0 <= x; --x) {
      const oxidd::util::opt_bool val = sat[x];
      if (val == oxidd::util::opt_bool::NONE) continue;

      res &= val == oxidd::util::opt_bool::TRUE ? _vars[x] : ~_vars[x];
    }
    return res;
  }

  inline oxidd::bdd_function
  satoneset(const oxidd::bdd_function& f, const oxidd::bdd_function& c)
  {
    oxidd::util::assignment f_sat = f.pick_cube();
    oxidd::util::assignment c_sat = f.pick_cube();
    assert(f_sat.size() == c_sat.size());

    oxidd::bdd_function res = top();
    for (int x = c_sat.size() - 1; 0 <= x; --x) {
      if (c_sat[x] == oxidd::util::opt_bool::NONE) continue;

      res &= f_sat[x] == oxidd::util::opt_bool::TRUE ? _vars[x] : ~_vars[x];
    }
    return res;
  }

[nhusung]

Sorry for the long delay. If you have suggestions for a better naming of pick_cube_symbolic()/pick_cube_symbolic_set(), please comment on that.

[SSoelvsten]

The solution I found for Adiar was to circumvent this with overloading:

  //////////////////////////////////////////////////////////////////////////////////////////////////
  bdd
  bdd_satmin(const bdd& f);

  //////////////////////////////////////////////////////////////////////////////////////////////////
  bdd
  bdd_satmin(const bdd& f,
             const generator<bdd::label_type>& d,
             const size_t d_size = bdd::max_label + 1);

  //////////////////////////////////////////////////////////////////////////////////////////////////
  template <typename ForwardIt>
  bdd
  bdd_satmin(const bdd& f, ForwardIt cbegin, ForwardIt cend)
  {
    return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
  }

  //////////////////////////////////////////////////////////////////////////////////////////////////
  bdd
  bdd_satmin(const bdd& f, const bdd& d);

  //////////////////////////////////////////////////////////////////////////////////////////////////
  void
  bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c);

  //////////////////////////////////////////////////////////////////////////////////////////////////
  template <typename ForwardIt>
  ForwardIt
  bdd_satmin(const bdd& f, ForwardIt begin)
  {
    bdd_satmin(f, make_consumer(begin));
    return begin;
  }

Alternatively, you could use the phrase point for a single symbolic value (rather than an entire set of values). So, it could be pick_point_symbolic and pick_cube_symbolic.