A reconstruction and extension of Maple’s assume facility via constraint contextual rewriting

AbstractMaple’s symbolic evaluator, together with a feature that is usually known as the assume facility, implements a powerful form of conditional rewriting. In a previous paper the authors showed that Maple’s evaluation process can be recast as constraint contextual rewriting (CCR), a form of conditional rewriting that incorporates the services provided by a decision procedure through a well-specified interface. In the present paper, this analysis is extended to a component of the assume facility that deals with problems beyond linear arithmetic and that we call the general solver. This led to the discovery of a fault that causes Maple to return wrong results with some contexts. The reason for this is that the facility wrongly assumes that the general solver is complete in the sense that it uses all the available assumptions in the context. While a simple fix to this problem would reduce the logical strength of the assume facility, we show that a more general approach inspired by techniques available in CCR does not suffer from the problem and naturally leads to stronger forms of simplification