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

[vinisilvag]

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.

[bpandreotti]

I think here it's simpler to use .first().unwrap(), since you're just pattern-matching on Some.

Suggested change

	if let Some(s_1) = args.first() {
	match s_1.as_ref() {
	Term::Const(Constant::String(s)) => Ok(s.len()),
	_ => Err(CheckerError::LengthCannotBeEvaluated(r.clone())),
	}
	} else {
	unreachable!()
	}
	let s_1 = args.first().unwrap();
	match s_1.as_ref() {
	Term::Const(Constant::String(s)) => Ok(s.len()),
	_ => Err(CheckerError::LengthCannotBeEvaluated(r.clone())),
	}

[vinisilvag]

Alright!

[bpandreotti]

Is this correct? If r_2.len() >= 2, concat will return a str.++ term, which will lead to an error when you call str_fixed_len_r(pool, r_2_concat). If it was instead an re.++ term, I suppose it would work. Either way, I think it would be simpler to just call str_fixed_len_re to each argument directly, and sum the results, e.g.

Suggested change

	if let [r_1, r_2 @ ..] = &args[..] {
	let r_2_concat = concat(pool, r_2.to_vec());
	Ok(str_fixed_len_re(pool, r_1.clone())? + str_fixed_len_re(pool, r_2_concat)?)
	} else {
	unreachable!()
	}
	let mut lengths = args.iter().map(|a| str_fixed_len_re(pool, a.clone()));
	lengths.try_fold(0, |acc, x| Ok(acc + x?))

[vinisilvag]

It is not correct, indeed :(

I confused this function with another one I previously implemented and ended up calling the wrong one. Also, I did not call str_fixed_len_re for each argument directly because I got too focused on how CPC represents re.++ and str.++ terms ((str.++ a b c) is transformed into (str.++ a (str.++ b (str.++ c "")))). However, with the representation in arrays that we have internally, it is, in fact, the same as applying str_fixed_len_re directly to each argument.

I am going to change that there and in other places where a similar behavior occurs.

[bpandreotti]

Similarly to the ReConcat case, in these two cases you are constructing a re.union/re.inter term with the remaining arguments just to call str_fixed_re_len recursively, which is not very efficient (for each argument, you allocate a vector with all the remaining arguments). I think it would be best to call str_fixed_re_len on each argument directly to get their lenghts, and then check if they are all the same.

Also, since these two cases are almost identical, differing only in which terms they ignore (re.none or re.all), it might make sense to put this logic in a separate function and call it in each case.