[rules] [strings] Add support for some core Strings theory rules that…

… reason about Regular expressions (#46)

* Add some core Strings theory rules that reason about RegEx

* Rename prefix and suffix functions

* Replace sanity checks with unreachable!()

* PR modifications

* Modifications in str_fixed_len_re

* Fix linting

carcara/src/ast/macros.rs

@@ -136,6 +136,9 @@ macro_rules! match_term {
     (@ARGS ($arg1:tt $arg2:tt $arg3:tt) = $var:expr) => {
         match_term!(@ARGS_IDENT (arg1: $arg1, arg2: $arg2, arg3: $arg3) = $var)
     };
+    (@ARGS ($arg1:tt $arg2:tt $arg3:tt $arg4:tt) = $var:expr) => {
+        match_term!(@ARGS_IDENT (arg1: $arg1, arg2: $arg2, arg3: $arg3, arg4: $arg4) = $var)
+    };
     (@ARGS_IDENT ( $($name:ident : $arg:tt),* ) = $var:expr) => {
         if let [$($name),*] = $var {
             #[allow(unused_parens)]
@@ -178,6 +181,9 @@ macro_rules! match_term {
     (@GET_VARIANT strconcat) => { $crate::ast::Operator::StrConcat };
     (@GET_VARIANT strsubstr) => { $crate::ast::Operator::Substring };
     (@GET_VARIANT strlen)    => { $crate::ast::Operator::StrLen };
+
+    (@GET_VARIANT strinre)    => { $crate::ast::Operator::StrInRe };
+    (@GET_VARIANT reinter)    => { $crate::ast::Operator::ReIntersection };
 }
 
 /// A variant of `match_term` that returns a `Result<_, CheckerError>` instead of an `Option`.

carcara/src/checker/error.rs

@@ -68,6 +68,9 @@ pub enum CheckerError {
     #[error("term '{0}' is not a valid n-ary operation")]
     NotValidNaryTerm(Rc<Term>),
 
+    #[error("cannot evaluate the fixed length of the term '{0}'")]
+    LengthCannotBeEvaluated(Rc<Term>),
+
     // General errors
     #[error("expected {0} premises, got {1}")]
     WrongNumberOfPremises(Range, usize),

carcara/src/checker/mod.rs

@@ -478,6 +478,11 @@ impl<'c> ProofChecker<'c> {
             "string_length_pos" => strings::string_length_pos,
             "string_length_non_empty" => strings::string_length_non_empty,
 
+            "re_inter" => strings::re_inter,
+            "re_unfold_neg" => strings::re_unfold_neg,
+            "re_unfold_neg_concat_fixed_prefix" => strings::re_unfold_neg_concat_fixed_prefix,
+            "re_unfold_neg_concat_fixed_suffix" => strings::re_unfold_neg_concat_fixed_suffix,
+
             // Special rules that always check as valid, and are used to indicate holes in the
             // proof.
             "hole" => |_| Ok(()),