How to correctly represent "else" when manually working with `powerset_domain` about crab HOT 9 CLOSED

Probably the best way is to split the else branch into two more
branches so the disjunction is handled directly by the join abstract
operator. So what I'm suggesting is to apply the abstract operations
for this equivalent code:

if (y > 10 && y < 20) {
  w=1;
} else if (y <= 10) {
  w=2;
} else if (y >= 20) {
  w=2;
}

Crab has also abstract operations for boolean operations that you can
use them to encode the disjunction of the else branch. So you can also do:

abs_val.assign_cst(b1, y <= 10); // b1 := (y <=10);
abs_val.assign_cst(b2, y >= 10); // b2 := (y >=20); 
abs_val.apply_binary_bool(crab::OP_BOR, b3, b1, b2);  // b3 := b1 or b2;
abs_val.assume_bool(b3, false /*meaning that b3 is not negated*/);

where b1, b2, and b3 are declared as boolean variables:

  z_var b1(vfac["b1"], crab::BOOL_TYPE, 1);
  z_var b2(vfac["b2"], crab::BOOL_TYPE, 1);
  z_var b3(vfac["b3"], crab::BOOL_TYPE, 1);

The problem is that there is no way to get around disjunctions. Most
of the domains will ignore the third abstract operation (i.e., the OR abstract operator).

So if you are using the powerset domain, follow the first approach. If you are ok with non-wrapped intervals, then you can use the boxes domain that represents precisely boolean combinations of interval constraints, and thus, it should be precise with boolean operations, included OR operations.

from crab.

Ah, okay, I would have never thought about doing that!

I guess for the case when it is a conjunction, you can just create the permutation of possibilities (excluding the true case), and then create a "duplicate branch" for each false evaluation. For disjunction, you could try to enumerate all true/false solutions using something like an ALLSAT solver, and then encode all of these with the corresponding true/false outcome. It would probably be enough just to encode a proposition skeleton to the solver, and then let crab tell you it is bottom if the outcome is "impossible".

I tried to play around with assign_cst, but this seems to work in neither of master or dev :(

from crab.

Did you tried assign_cst with the boxes domain? The wrapped interval domain completely ignores boolean operations. In crab, there is a reduced product (a pair of domains) of a simple domain for booleans (called flat_boolean_domain) with an arbitrary numerical domain. It's called flat_boolean_numerical_domain. That one does something but nothing really with boolean ORs.

from crab.

Maybe I'm crazy, but I couldn't even find a definition of that method:

[avj@tempvm master]$ pwd
/home/avj/clones/crab/master
[avj@tempvm master]$ ag "assign_cst\("
include/crab/cfg/cfg.hpp
311:  bool is_bool_assign_cst() const { return (m_stmt_code == BOOL_ASSIGN_CST); }
1527:  bool_assign_cst(variable_t lhs, linear_constraint_t rhs)

from crab.

(also, I think because I have a "domain" then what's in the cfg namespace won't work for me -- maybe I missed the point 😬 )

from crab.

Sorry I meant bool_assign_cst.

from crab.

Do you expect bool_assign_cst to work with:

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

?

from crab.

Btw, I didn't ignore:

So if you are using the powerset domain, follow the first approach.

I had just presumed it would work just not with disjunction ...

from crab.

Do you expect bool_assign_cst to work with:

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

?

Only flat_boolean_numerical_domain and boxes will do something with bool_assign_cst.
So you can do powerset_domain<flat_boolean_numerical_domain<z_wrapped_interval_domain>>

from crab.