Symbolic PickOneCube(const BddSet &variables)

[SSoelvsten]

While Model Checking, to obtain a specific (symbolic) state s in a set S, one would want to use the PickOneCube(S) function. Yet to only obtain a single state, the resulting cube needs to fix a value for each variable. Hence, I would then want to provide some cube c of all states (similar to the Exists function).

Yet, doing so returns a non-symbolic vector of assignments which I have to convert back into a BDD.

  inline sylvan::Bdd
  satone(const sylvan::Bdd& f, const sylvan::Bdd& c)
  {
    const auto f_vals = f.PickOneCube(c);
    const auto c_vars = sylvan::BddSet(c).toVector();

    sylvan::Bdd res = top();
    for (int i = c_vars.size() - 1; 0 <= i; --i) {
      const int  var = c_vars[i];
      const bool val = f_vals[i];

      res &= val ? ithvar(var) : nithvar(var);
    }
    return res;
  }

As you are working towards v2.0, I would propose this is changed to return a sylvan::Bdd instead. If the user wants to have these values output instead then they can provide a begin iterator to some data structure they would like to feed the result into.

[SSoelvsten]

This might just be a lack of exposing sylvan_sat_single in the C++ API?