[rules] [strings] Add support for `concat_split` rule and splitted rules in prefix and suffix version - Githubissues

ufmg-smite / carcara

Apache License 2.0

33 stars 11 forks source link

[rules] [strings] Add support for `concat_split` rule and splitted rules in prefix and suffix version #35

Closed vinisilvag closed 6 months ago

vinisilvag commented 7 months ago

This PR adds the concat_csplit rule from the Strings theory. Rule reference can be found in the cvc5 documentation and in the AletheLF specification.

Furthermore, it:

Splits the rule into two versions: application over prefixes and over suffixes;
Makes the necessary modifications to allow other rules to be split in this way;
Standardizes variable names to how they appear in AletheLF documentation;
Fixes a bug in the function that creates Skolems in the concat_csplit rule.