"compress" `powerset_domain` domain after projection

[aytey]

Current status

I have code that looks like this:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

using analysis_domain = powerset_of_z_wrapped_intervals;

int main(void) {
  variable_factory_t vfac;
  z_var y(vfac["y"], crab::INT_TYPE, 32);
  z_var x(vfac["x"], crab::INT_TYPE, 32);

  analysis_domain d1;
  d1 += (y > 10);
  d1.assign(x, 0);

  analysis_domain d2;
  d2 += (y > 20);
  d2.assign(x, 1);

  analysis_domain d3;
  d3 += (y > 30);
  d3.assign(x, 2);

  analysis_domain d4 = d1 | d2 | d3;
  crab::outs() << d4 << "\n\n\n";

  std::vector<z_var> vars;
  vars.push_back(x);

  analysis_domain proj = d4;
  proj.project(vars);
  crab::outs() << proj << "\n\n\n";

  return 0;
}

(the code is purposely brain-dead, but that's fine)

Which gives this:

{y -> [[11, 2147483647]]_32; x -> [[0, 0]]_32} or
{y -> [[21, 2147483647]]_32; x -> [[1, 1]]_32} or
{y -> [[31, 2147483647]]_32; x -> [[2, 2]]_32}


{x -> [[0, 0]]_32} or
{x -> [[1, 1]]_32} or
{x -> [[2, 2]]_32}

Question

After doing the projection, I get a powerset domain that has three elements (0, 1 and 2). Is it possible to ask crab to "compress" this domain into a single range of [0, 2]?

[caballa]

The powerset domain has that operation but it's currently a private method

https://github.com/seahorn/crab/blob/dev/include/crab/domains/powerset_domain.hpp#L135

[aytey]

Of all the words I grepped for, "smash" was not one of them 🤦

[aytey]

I just tested it -- works perfectly!

Would you accept a PR to make that public?

[caballa]

I just tested it -- works perfectly!

Would you accept a PR to make that public?

Not sure. Typically I make public only those methods which are part from the generic abstract_domain base class. That is, I like the idea of manipulating an abstract domain always in the same way (i.e,. with the same operations) regardless whether the abstract domain is relational or non-relational, convex or non-convex, etc.

It would make more sense to have a generic abstract operation convexify or something like that (implemented by all domains) that it makes the internal state of the abstract domain convex if such notion exists. Anyway, thinking loudly ...