RFE: implement += in TemplateDomain and use it to remove unnecessary memory allocation in ExprLinearity::visit(const ExprMul& e)

[ANogin]

https://github.com/ibex-team/ibex-lib/blob/e478f10168aa057000c8224be2f4553287709a69/src/symbolic/ibex_ExprLinearity.cpp#L207 has a comment '//TODO: implement += in TemplateDomain'. In running https://github.com/dreal/dreal4/blob/master/dreal/examples/verify_nn.cc (with a slightly different set of constants), I see that ~14% of all memory allocation (by # of bytes allocated) is from that operator + in ExprLinearity::visit(const ExprMul& e) - presumably would go away if that TODO was addressed.

P.S. In the same execution, 17% of all allocation was due to operator * - from https://github.com/ibex-team/ibex-lib/blob/e478f10168aa057000c8224be2f4553287709a69/src/symbolic/ibex_ExprLinearity.cpp#L206 I am guessing. It looks likes some of that is unavoidable, but could it be reduced perhaps? (Could perhaps the same memory area be used for both multiplications? I do not know much about the underlying code, so just guessing.)

[gchabert]

Dear @ANogin Thanks for reporting the issue and investigating. I don't think that implementing "+=" in TemplateDomain will change your performance issue. The problem is that doing automated symbolic processing is slow with Ibex, merely because Ibex was not designed for that purpose (as far as I understand, this is more or less what you do in your project). For your information, this part of Ibex (ExprLinearity) is about to be dropped and replaced by a new and more powerful simplification engine. But this will probably not make symbolic processing faster.

However, there is a recent functionality that might still drastically improve your performance if you are generating similar expressions with only constants changing. The idea is simple: we keep the same expression and just change de constants' value. It is the new ExprConstant::new_mutable constructor. This will be integrated and documented in the next release but you can already test it by switching to the 'develop' branch. This is very simple. Up to now, if you need to generate an expression x+c where c is some constant, you would do :

    const ExprSymbol& x=ExprSymbol::new_("x");
    const ExprConstant& c=ExprConstant::new_scalar(Interval::zero());
    const ExprNode& e(x+c);

and if the constant change, you have to build a new expression again from scratch. Now you can do this:

    const ExprSymbol& x=ExprSymbol::new_("x");
    Interval _c(Interval::zero());
    const ExprConstant& c=ExprConstant::new_mutable(_c);
    const ExprNode& e(x+c);
    cout << e << endl;

    _c=1;  // constant has changed --> no need to re-build the expression!
    cout << e << endl;

This prints:

(x+0)
(x+1)

Tell me if this helps you.

[ANogin]

Thanks a lot for the info - while I am not doing any of the ibex-related development (just doing some profiling of the end-result), I passed this along to a few people who do.

[gchabert]

I think the issue can be closed but fell free to reopen it if I'm wrong