Not for free

Since last week Jan has extended the Boolean expression language supported by the Acumen enclosure interpreter to include disjunction (||) and logical negation (not). The main difficulty with the former was to extend the constraint solver used to narrow initial condition boxes while performing piecewise IVP solving, and the domains of guard and invariant predicates during event detection and handling. In particular, the intersection operation used by the event tree algorithm (EVT semantics option) relies on domain narrowing to reduce information loss errors while evaluating predicates. The issue with the latter, i.e. supporting negation in the enclosure semantics, was that narrowing cannot be effectively implemented directly on negated predicates. Instead, negations are pushed through the predicate using standard logical identities and into the relations, where e.g. not(x <= 1) becomes x > 1. The main remining issue is that of reducing the effects due to inefficient narrowing over disjunction. The method that Jan believes is easiest to implement is the one used in e.g. the RealPaver constraint solver. There, disjunctive constraints are translated into nonpositivity constraints on minimum expressions, e.g. x > y || x <= 0 becomes min(y-x,x) <= 0.