Adds support for String theory indexed operators

carcara/src/ast/mod.rs

@@ -418,6 +418,9 @@ pub enum IndexedOperator {
     ZeroExtend,
     SignExtend,
     BvConst,
+
+    RePower,
+    ReLoop,
 }
 
 impl_str_conversion_traits!(IndexedOperator {
@@ -426,6 +429,9 @@ impl_str_conversion_traits!(IndexedOperator {
     ZeroExtend: "zero_extend",
     SignExtend: "sign_extend",
     BvConst: "bv",
+
+    RePower: "re.^",
+    ReLoop: "re.loop"
 });
 
 impl_str_conversion_traits!(Operator {
@@ -733,6 +739,14 @@ impl Term {
         }
     }
 
+    /// Tries to extract a `Integer` from a term. Returns `Some` if the term is an integer constant.
+    pub fn as_integer_number(&self) -> Option<Integer> {
+        match self {
+            Term::Const(Constant::Integer(i)) => Some(i.clone()),
+            _ => None,
+        }
+    }
+
     /// Tries to extract a `Rational` from a term, allowing negative values represented with the
     /// unary `-` operator. Returns `Some` if the term is an integer or real constant, or one such
     /// constant negated with the `-` operator.
@@ -743,6 +757,16 @@ impl Term {
         }
     }
 
+    /// Tries to extract a `Integer` from a term, allowing negative values represented with the
+    /// unary `-` operator. Returns `Some` if the term is an integer constant, or one such
+    /// constant negated with the `-` operator.
+    pub fn as_signed_integer(&self) -> Option<Integer> {
+        match match_term!((-x) = self) {
+            Some(x) => x.as_integer_number().map(|r| -r),
+            None => self.as_integer_number(),
+        }
+    }
+
     /// Tries to extract a `Rational` from a term, allowing fractions. This method will return
     /// `Some` if the term is:
     ///

carcara/src/ast/pool/mod.rs

@@ -254,6 +254,7 @@ impl PrimitivePool {
                         "bv const should be handled by the parser and transfromed into a constant"
                     ),
                     IndexedOperator::BvBitOf => Sort::Bool,
+                    IndexedOperator::RePower | IndexedOperator::ReLoop => Sort::RegLan,
                 };
                 sort
             }

carcara/src/parser/error.rs

@@ -1,7 +1,7 @@
 //! The types for parser errors.
 
 use crate::{
-    ast::{Constant, Sort},
+    ast::{Constant, Rc, Sort, Term},
     parser::Token,
     utils::Range,
 };
@@ -57,9 +57,9 @@ pub enum ParserError {
     #[error("expected bitvector sort, got '{0}'")]
     ExpectedBvSort(Sort),
 
-    // Expected Constant::Integer, got other Constant
+    // Expected Constant::Integer, got other Term
     #[error("expected Constant of type Integer, got '{0}'")]
-    ExpectedIntegerConstant(Constant),
+    ExpectedIntegerConstant(Rc<Term>),
 
     /// A term that is not a function was used as a function.
     #[error("'{0}' is not a function sort")]
@@ -83,7 +83,7 @@ pub enum ParserError {
 
     /// The argument values are not in the expected range.
     #[error("expected argument value to be greater than {0}, got {1}")]
-    WrongValueOfArgs(Range, usize),
+    WrongValueOfArgs(Range<Integer>, Integer),
 
     #[error("extract arguments do not follow restrictions. Expected: {2} > {0} and {0} >= {1} and {1} >= 0")]
     InvalidExtractArgs(usize, usize, usize),
@@ -126,24 +126,17 @@ where
 /// Returns an error if the value of `sequence` is not in the `expected` range.
 pub fn assert_indexed_op_args_value<R>(sequence: &[Constant], range: R) -> Result<(), ParserError>
 where
-    R: Into<Range>,
+    R: Into<Range<Integer>>,
 {
     let range = range.into();
-    let mut wrong_value = usize::MAX;
     for x in sequence {
         if let Constant::Integer(i) = x {
-            let value = i.to_usize().unwrap();
-            if !range.contains(value) {
-                wrong_value = value;
-                break;
+            if !range.contains(i.clone()) {
+                return Err(ParserError::WrongValueOfArgs(range, i.clone()));
             }
         }
     }
-    if wrong_value == usize::MAX {
-        Ok(())
-    } else {
-        Err(ParserError::WrongValueOfArgs(range, wrong_value))
-    }
+    Ok(())
 }
 
 /// An error in sort checking.

carcara/src/parser/mod.rs

@@ -1340,15 +1340,39 @@ impl<'a, R: BufRead> Parser<'a, R> {
 
     fn parse_indexed_operator(&mut self) -> CarcaraResult<(IndexedOperator, Vec<Constant>)> {
         let bv_symbol = self.expect_symbol()?;
+
         if let Some(value) = bv_symbol.strip_prefix("bv") {
             let parsed_value = value.parse::<Integer>().unwrap();
-            let mut args = self.parse_sequence(Self::parse_constant, true)?;
-            args.insert(0, Constant::Integer(parsed_value));
-            return Ok((IndexedOperator::BvConst, args));
+            let args = self.parse_sequence(Self::parse_term, true)?;
+            let mut constant_args = Vec::new();
+            for arg in args {
+                if let Some(i) = arg.as_signed_integer() {
+                    constant_args.push(Constant::Integer(i));
+                } else {
+                    return Err(Error::Parser(
+                        ParserError::ExpectedIntegerConstant(arg.clone()),
+                        self.current_position,
+                    ));
+                }
+            }
+            constant_args.insert(0, Constant::Integer(parsed_value));
+            return Ok((IndexedOperator::BvConst, constant_args));
         }
+
         let op = IndexedOperator::from_str(bv_symbol.as_str()).unwrap();
-        let args = self.parse_sequence(Self::parse_constant, true)?;
-        Ok((op, args))
+        let args = self.parse_sequence(Self::parse_term, true)?;
+        let mut constant_args = Vec::new();
+        for arg in args {
+            if let Some(i) = arg.as_signed_integer() {
+                constant_args.push(Constant::Integer(i));
+            } else {
+                return Err(Error::Parser(
+                    ParserError::ExpectedIntegerConstant(arg.clone()),
+                    self.current_position,
+                ));
+            }
+        }
+        Ok((op, constant_args))
     }
 
     /// Constructs, check operation arguments and sort checks an indexed operation term.
@@ -1363,12 +1387,8 @@ impl<'a, R: BufRead> Parser<'a, R> {
             IndexedOperator::BvConst => {
                 assert_num_args(&op_args, 2)?;
                 assert_num_args(&args, 0)?;
-                let Constant::Integer(value) = op_args[0].clone() else {
-                    return Err(ParserError::ExpectedIntegerConstant(op_args[0].clone()));
-                };
-                let Constant::Integer(width) = op_args[1].clone() else {
-                    return Err(ParserError::ExpectedIntegerConstant(op_args[1].clone()));
-                };
+                let value = op_args[0].as_integer().unwrap();
+                let width = op_args[1].as_integer().unwrap();
                 assert_indexed_op_args_value(&[op_args[0].clone()], 0..)?;
                 assert_indexed_op_args_value(&[op_args[1].clone()], 1..)?;
                 return Ok(self.pool.add(Term::Const(Constant::BitVec(value, width))));
@@ -1417,6 +1437,22 @@ impl<'a, R: BufRead> Parser<'a, R> {
                 }
                 assert_indexed_op_args_value(&op_args, 0..)?;
             }
+            IndexedOperator::RePower => {
+                assert_num_args(&op_args, 1)?;
+                assert_num_args(&args, 1)?;
+                SortError::assert_eq(&Sort::Int, &op_args[0].sort())?;
+                SortError::assert_eq(&Sort::RegLan, &args[0].raw_sort())?;
+                assert_indexed_op_args_value(&[op_args[0].clone()], 0..)?;
+            }
+            IndexedOperator::ReLoop => {
+                assert_num_args(&op_args, 2)?;
+                assert_num_args(&args, 1)?;
+                for arg in &op_args {
+                    SortError::assert_eq(&Sort::Int, &arg.sort())?;
+                }
+                SortError::assert_eq(&Sort::RegLan, &args[0].raw_sort())?;
+                assert_indexed_op_args_value(&op_args, 0..)?;
+            }
         }
         Ok(self.pool.add(Term::IndexedOp { op, op_args, args }))
     }

carcara/src/utils.rs

@@ -1,5 +1,6 @@
 use crate::ast::{BindingList, Quantifier, Rc, Term};
 use indexmap::{IndexMap, IndexSet};
+use rug::Integer;
 use std::{
     borrow::Borrow,
     fmt,
@@ -166,15 +167,28 @@ impl<K, V> Default for HashMapStack<K, V> {
 
 // TODO: Document this struct
 #[derive(Debug)]
-pub struct Range(Option<usize>, Option<usize>);
+pub struct Range<T = usize>(Option<T>, Option<T>);
 
-impl Range {
-    pub fn contains(&self, n: usize) -> bool {
-        self.0.map_or(true, |bound| n >= bound) && self.1.map_or(true, |bound| n <= bound)
+impl<T: std::cmp::PartialOrd> Range<T> {
+    pub fn contains(&self, n: T) -> bool {
+        self.0.as_ref().map_or(true, |bound| n >= *bound)
+            && self.1.as_ref().map_or(true, |bound| n <= *bound)
     }
 }
 
-impl fmt::Display for Range {
+impl fmt::Display for Range<usize> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self {
+            Range(Some(a), Some(b)) if a == b => write!(f, "{}", a),
+            Range(Some(a), Some(b)) => write!(f, "between {} and {}", a, b),
+            Range(Some(a), None) => write!(f, "at least {}", a),
+            Range(None, Some(b)) => write!(f, "up to {}", b),
+            Range(None, None) => write!(f, "any number of"),
+        }
+    }
+}
+
+impl fmt::Display for Range<Integer> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
             Range(Some(a), Some(b)) if a == b => write!(f, "{}", a),
@@ -204,6 +218,12 @@ impl From<ops::RangeFrom<usize>> for Range {
     }
 }
 
+impl From<ops::RangeFrom<i32>> for Range<Integer> {
+    fn from(r: ops::RangeFrom<i32>) -> Self {
+        Self(Some(Integer::from(r.start)), None)
+    }
+}
+
 impl From<ops::RangeFull> for Range {
     fn from(_: ops::RangeFull) -> Self {
         Self(None, None)