Add rare-list operator

carcara/src/ast/mod.rs

@@ -409,6 +409,10 @@ pub enum Operator {
     BvSGt,
     BvSGe,
     BvBbTerm,
+
+    // Misc.
+    /// The `rare-list` operator, used to represent RARE lists.
+    RareList,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -528,6 +532,8 @@ impl_str_conversion_traits!(Operator {
     BvSGt: "bvsgt",
     BvSGe: "bvsge",
     BvBbTerm: "bbterm",
+
+    RareList: "rare-list",
 });
 
 /// A variable and an associated sort.
@@ -571,6 +577,9 @@ pub enum Sort {
     ///
     /// The associated term is the BV width of this sort.
     BitVec(Integer),
+
+    /// The sort of RARE lists.
+    RareList,
 }
 
 /// A quantifier, either `forall` or `exists`.

carcara/src/ast/pool/mod.rs

@@ -217,6 +217,7 @@ impl PrimitivePool {
                 | Operator::ReKleeneCross
                 | Operator::ReOption
                 | Operator::ReRange => Sort::RegLan,
+                Operator::RareList => Sort::RareList,
             },
             Term::App(f, _) => {
                 match self.compute_sort(f).as_sort().unwrap() {

carcara/src/ast/printer.rs

@@ -429,6 +429,7 @@ impl fmt::Display for Sort {
             Sort::RegLan => write!(f, "RegLan"),
             Sort::Array(x, y) => write_s_expr(f, "Array", &[x, y]),
             Sort::BitVec(w) => write!(f, "(_ BitVec {})", w),
+            Sort::RareList => unreachable!("RARE list sort should never be displayed"),
         }
     }
 }

carcara/src/parser/mod.rs

@@ -463,6 +463,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
                 }
                 SortError::assert_all_eq(&sorts)?;
             }
+            Operator::RareList => SortError::assert_all_eq(&sorts)?,
         }
         Ok(self.pool.add(Term::Op(op, args)))
     }