Syntactic+semantic subsumption check

[rajdeep87]

Current subsumption check using SAT call solver << and_exprt(conjunction(value), not_exprt(m)) may subsume valid meet irreducibles in presence of octagonal constraints, which may further block the propagation phase from deducing closed abstract value.
We change the subsumption check to the following. Assume the function is_subsumption(A,m) where we want to determine if m is subsumed by abstract value A.
Step 1: Normalize all expressions in A as well as m (that is, !(x<=10) to (x>10))
Step 2: Collect all lhs templates of the meet irreducibles in A that matches with lhs of m in a vector value.
Step 3: Check using solver whether and_exprt(conjunction(value), not_exprt(m)) is SAT or UNSAT. If SAT, then m is not subsumed by A, else m is subsumed by A.

[rajdeep87]

Two bugs to be fixed:
Case 1:
learning0 regression shows termination problem with the new subsumption check. The sequence of decisions with the old subsumption check is as follows:
FINAL DECISION: y#18 <= 1073741823u
FINAL DECISION: y#18 <= 536870911u
FINAL DECISION: y#18 <= 268435455u
FINAL DECISION: y#18 <= 134217727u
FINAL DECISION: y#18 <= 67108863u
FINAL DECISION: y#18 <= 33554431u
FINAL DECISION: y#18 <= 16777215u
FINAL DECISION: y#18 <= 8388607u
FINAL DECISION: y#18 <= 4194303u
FINAL DECISION: y#18 <= 2097151u
FINAL DECISION: y#18 <= 1048575u
FINAL DECISION: y#18 <= 524287u
FINAL DECISION: y#18 <= 262143u
FINAL DECISION: y#18 <= 131071u
FINAL DECISION: y#18 <= 65535u
FINAL DECISION: y#18 <= 32767u
FINAL DECISION: y#18 <= 16383u
FINAL DECISION: y#18 <= 8191u
FINAL DECISION: y#18 <= 4095u
FINAL DECISION: y#18 <= 2047u
FINAL DECISION: y#18 <= 1023u
FINAL DECISION: y#18 <= 511u
FINAL DECISION: y#18 <= 255u
FINAL DECISION: y#18 <= 127u
FINAL DECISION: y#18 <= 63u
FINAL DECISION: y#18 <= 31u
FINAL DECISION: y#18 <= 15u
FINAL DECISION: y#18 <= 7u
FINAL DECISION: y#18 <= 3u
FINAL DECISION: y#18 <= 1u
FINAL DECISION: y#18 <= 0u

With the new check, it generates the full sequence as above, but then keeps on repeating the final decision FINAL DECISION: y#18 <= 0u

Case 2:
The new subsumption check still does not ensure that the abstract value is closed. The domain operator still returns no new deductions when true_exprt is popped out in is_closed() check

[rajdeep87]

The case1 above is handled by implementing a variant of the normalize_val in acdl_domain.cpp
The new function for normalization called normalize_val_syntactic() does the following:
1> It collects meet irreducibles with the same lhs and normalizes them using the is_subsumption_syntactic() method. Note that is_subsumption_syntactic() is weaker subsumption check than the purely semantic subsumption check with SAT solver, that is, it allows deduction (m) not to be subsumed by value (A) by just comparing m with matching meet irreducibles in A.
2> Note that normalize_val_syntactic() is only meant to work with is_subsumption_syntactic().