This PR splits the concat_csplit rule into a prefix version and a suffix version.
The main reason for this modification is to simplify how the rule works, since it's premises and conclusion changes substantially based on the reverse parameter value (if the parameter is set to true, the rule is reasoning about suffixes, and if it's set to false, about prefixes).
All unit tests where converted and some additional cases where incorporated to cover previously untested scenarios.
This PR splits the
concat_csplitrule into a prefix version and a suffix version. The main reason for this modification is to simplify how the rule works, since it's premises and conclusion changes substantially based on the reverse parameter value (if the parameter is set totrue, the rule is reasoning about suffixes, and if it's set tofalse, about prefixes).All unit tests where converted and some additional cases where incorporated to cover previously untested scenarios.
The rule reference can be found in the cvc5 documentation and in the AletheLF specification.