ufmg-smite / carcara

Apache License 2.0
33 stars 11 forks source link

[rules] [strings] Add support for some core Strings theory rules that reason about Regular expressions #46

Closed vinisilvag closed 1 month ago

vinisilvag commented 2 months ago

This PR adds the re_inter, re_unfold_neg and re_unfold_neg_concat_fixed rules from the Strings theory. For simplification reasons, the re_unfold_neg_concat_fixed rule was splitted in a prefix version and suffix version (resp. re_unfold_neg_concat_fixed_prefix and re_unfold_neg_concat_fixed_suffix), just like it was done for other previously implemented rules.

Future PR's will add the re_unfold_pos rule.

Rules reference can be found in the cvc5 documentation and in the CPC specification.