Skip to content

Normalize all n-ary operators in the RARE rewrite engine #125

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
caotic123 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Normalize all n-ary operators in the RARE rewrite engine #125

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
25c6de0
Fix rare-list checking: parameterize RareList sort by element type
Jun 9, 2026
58b36e3
Normalize all n-ary operators in the RARE rewrite engine
Jun 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion carcara/src/ast/polyeq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -653,8 +653,8 @@ impl PolyeqComparable for Sort {
| (Sort::Real, Sort::Real)
| (Sort::String, Sort::String)
| (Sort::RegLan, Sort::RegLan)
| (Sort::RareList, Sort::RareList)
| (Sort::Type, Sort::Type) => true,
(Sort::RareList(a), Sort::RareList(b)) => comp.eq(a, b),
(Sort::Array(x_a, y_a), Sort::Array(x_b, y_b)) => {
comp.eq(x_a, x_b) && comp.eq(y_a, y_b)
}
Expand Down
97 changes: 74 additions & 23 deletions carcara/src/ast/pool/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,11 @@ impl PrimitivePool {
| Operator::BvSRem
| Operator::BvSMod
| Operator::BvAShr => {
match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
let sort = match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
};
match sort {
Sort::BitVec(width) => Sort::BitVec(width),
Sort::ParamSort(v, head) => {
if let Some(Sort::Var(_)) = head.as_sort() {
Expand Down Expand Up @@ -167,7 +171,11 @@ impl PrimitivePool {
}
let mut total_width: Vec<TotalWidth> = vec![];
for arg in args {
match self.compute_sort(arg).as_sort().unwrap().clone() {
let sort = match self.compute_sort(arg).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
};
match sort {
Sort::BitVec(arg_width) => {
total_width.push(TotalWidth::Width(arg_width));
}
Expand Down Expand Up @@ -218,18 +226,27 @@ impl PrimitivePool {
}
Operator::RealDiv | Operator::ToReal => Sort::Real,
Operator::IntDiv | Operator::Mod | Operator::Abs | Operator::ToInt => Sort::Int,
Operator::Select => match self.compute_sort(&args[0]).as_sort().unwrap() {
Sort::Array(_, y) => y.as_sort().unwrap().clone(),
Sort::ParamSort(v, head) => {
if let Some(Sort::Var(_)) = head.as_sort() {
v[1].as_sort().unwrap().clone()
} else {
unreachable!()
Operator::Select => {
let sort = match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
};
match sort {
Sort::Array(_, y) => y.as_sort().unwrap().clone(),
Sort::ParamSort(v, head) => {
if let Some(Sort::Var(_)) = head.as_sort() {
v[1].as_sort().unwrap().clone()
} else {
unreachable!()
}
}
_ => unreachable!(),
}
_ => unreachable!(),
}
Operator::Store => match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
},
Operator::Store => self.compute_sort(&args[0]).as_sort().unwrap().clone(),
Operator::StrLen | Operator::IndexOf | Operator::StrToCode | Operator::StrToInt => {
Sort::Int
}
Expand All @@ -255,7 +272,14 @@ impl PrimitivePool {
| Operator::ReKleeneCross
| Operator::ReOption
| Operator::ReRange => Sort::RegLan,
Operator::RareList => Sort::RareList,
Operator::RareList => {
let element_sort = if let Some(arg) = args.first() {
self.compute_sort(arg)
} else {
self.add(Term::Sort(Sort::Var("T".to_owned())))
};
Sort::RareList(element_sort)
}
},
Term::App(f, args) => {
match self.compute_sort(f).as_sort().unwrap() {
Expand Down Expand Up @@ -313,26 +337,53 @@ impl PrimitivePool {
}
ParamOperator::ZeroExtend | ParamOperator::SignExtend => {
let extension_width = op_args[0].as_integer().unwrap().to_usize().unwrap();
let Sort::BitVec(bv_width) =
self.compute_sort(&args[0]).as_sort().unwrap().clone()
else {
unreachable!()
let sort = match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
};
Sort::BitVec(extension_width + bv_width)
match sort {
Sort::BitVec(bv_width) => Sort::BitVec(extension_width + bv_width),
Sort::ParamSort(v, head) => {
let width = v.first().cloned().unwrap_or_else(|| {
unreachable!(
"bitvector parametric sort missing width in zero/sign extend"
)
});
let ext = self
.add(Term::Const(Constant::Integer(extension_width.into())));
let add = self.add(Term::Op(Operator::Add, vec![ext, width]));
Sort::ParamSort(vec![add], head)
}
_ => unreachable!(),
}
}
ParamOperator::RotateLeft | ParamOperator::RotateRight => {
self.compute_sort(&args[0]).as_sort().unwrap().clone()
}
ParamOperator::Repeat => {
let repetitions = op_args[0].as_integer().unwrap();
let Sort::BitVec(bv_width) =
self.compute_sort(&args[0]).as_sort().unwrap().clone()
else {
unreachable!()
let sort = match self.compute_sort(&args[0]).as_sort().unwrap().clone() {
Sort::RareList(inner) => inner.as_sort().unwrap().clone(),
sort => sort,
};
Sort::BitVec((repetitions * bv_width).to_usize().unwrap())
match sort {
Sort::BitVec(bv_width) => {
Sort::BitVec((repetitions * bv_width).to_usize().unwrap())
}
Sort::ParamSort(v, head) => {
let width = v.first().cloned().unwrap_or_else(|| {
unreachable!(
"bitvector parametric sort missing width in repeat"
)
});
let reps =
self.add(Term::Const(Constant::Integer(repetitions.clone())));
let mul = self.add(Term::Op(Operator::Mult, vec![reps, width]));
Sort::ParamSort(vec![mul], head)
}
_ => unreachable!(),
}
}

ParamOperator::BvConst => unreachable!(
"bv const should be handled by the parser and transformed into a constant"
),
Expand Down
2 changes: 1 addition & 1 deletion carcara/src/ast/printer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -559,7 +559,7 @@ impl fmt::Display for Sort {
Sort::ParamSort(args, s) => write!(f, "(par {:?} {})", args, s),
Sort::Array(x, y) => write_s_expr(f, "Array", &[x, y]),
Sort::BitVec(w) => write!(f, "(_ BitVec {})", w),
Sort::RareList => write!(f, "rare-list"),
Sort::RareList(elem) => write_s_expr(f, "rare-list", &[elem]),
Sort::Type => write!(f, "Type"),
}
}
Expand Down
25 changes: 22 additions & 3 deletions carcara/src/ast/substitution.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,14 @@ pub struct Substitution {
}

impl Substitution {
fn compare_sort_rare_list(lhs: &Sort, rhs: &Sort) -> bool {
match (lhs, rhs) {
(Sort::RareList(inner), other) => inner.as_sort().is_some_and(|s| s == other),
(other, Sort::RareList(inner)) => inner.as_sort().is_some_and(|s| s == other),
_ => false,
}
}

/// Constructs an empty substitution.
pub fn empty() -> Self {
Self {
Expand Down Expand Up @@ -74,8 +82,13 @@ impl Substitution {
if !k.is_var() && !k.is_sort_var() {
return Err(SubstitutionError::NotAVariable(k.clone()));
}
if pool.sort(k) != pool.sort(v)
&& !pool.sort(k).as_sort().is_some_and(Sort::is_polymorphic)

let k_sort = pool.sort(k).as_sort().unwrap().clone();
let v_sort = pool.sort(v).as_sort().unwrap().clone();
if k_sort != v_sort
&& !k_sort.is_polymorphic()
&& !v_sort.is_polymorphic()
&& !Self::compare_sort_rare_list(&k_sort, &v_sort)
{
return Err(SubstitutionError::DifferentSorts(k.clone(), v.clone()));
}
Expand Down Expand Up @@ -104,7 +117,13 @@ impl Substitution {
if !x.is_var() && !x.is_sort_var() {
return Err(SubstitutionError::NotAVariable(x));
}
if pool.sort(&x) != pool.sort(&t) {
let x_sort = pool.sort(&x).as_sort().unwrap().clone();
let t_sort = pool.sort(&t).as_sort().unwrap().clone();
if x_sort != t_sort
&& !x_sort.is_polymorphic()
&& !t_sort.is_polymorphic()
&& !Self::compare_sort_rare_list(&x_sort, &t_sort)
{
return Err(SubstitutionError::DifferentSorts(x, t));
}

Expand Down
9 changes: 6 additions & 3 deletions carcara/src/ast/term.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,8 +92,8 @@ pub enum Sort {
/// A parametric sort, with a set of sort variables that can appear in the second argument.
ParamSort(Vec<Rc<Term>>, Rc<Term>),

/// The sort of RARE lists.
RareList,
/// The sort of RARE lists, parameterized by their element sort.
RareList(Rc<Term>),

/// The sort of sorts.
Type,
Expand Down Expand Up @@ -736,8 +736,10 @@ impl Sort {
| (Sort::Real, Sort::Real)
| (Sort::String, Sort::String)
| (Sort::RegLan, Sort::RegLan)
| (Sort::RareList, Sort::RareList)
| (Sort::Type, Sort::Type) => true,
(Sort::RareList(a), Sort::RareList(b)) => {
a.as_sort().unwrap().match_with(b.as_sort().unwrap(), map)
}
(Sort::Array(x_a, y_a), Sort::Array(x_b, y_b)) => {
let s_x_a = x_a.as_sort().unwrap();
let s_y_a = y_a.as_sort().unwrap();
Expand Down Expand Up @@ -1118,6 +1120,7 @@ impl Sort {
match self {
Sort::Var(_) => true,
Sort::ParamSort(_, sort) if matches!(&**sort, Term::Sort(Sort::Var(_))) => true,
Sort::RareList(inner) => inner.as_sort().is_some_and(Sort::is_polymorphic),
_ => false,
}
}
Expand Down
18 changes: 13 additions & 5 deletions carcara/src/checker/rules/rare.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use indexmap::IndexMap;

use crate::{
ast::{Constant, Substitution, Term},
ast::{Constant, Sort, Substitution, Term},
checker::{error::CheckerError, rules::get_premise_term},
rare::{get_rules, rewrite_meta_terms},
};
Expand Down Expand Up @@ -41,10 +41,18 @@ pub fn check_rare(

for arg in rare_term.arguments.iter().rev() {
let arg_sort = rare_term.parameters.get(arg).unwrap();
map.insert(
pool.add(Term::Var(arg.clone(), arg_sort.term.clone())),
arguments.next().unwrap().clone(),
);
let value = arguments.next().unwrap().clone();
let var_sort =
if arg_sort.attribute == crate::ast::rare_rules::AttributeParameters::List {
match arg_sort.term.as_sort().unwrap() {
Sort::RareList(elem_sort) => elem_sort.clone(),
_ => arg_sort.term.clone(),
}
} else {
arg_sort.term.clone()
};
let variable = pool.add(Term::Var(arg.clone(), var_sort));
map.insert(variable, value);
}

if rare_term.premises.len() != premises.len() {
Expand Down
4 changes: 4 additions & 0 deletions carcara/src/parser/error.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -250,6 +250,10 @@ impl SortError {
) -> Result<(), Self> {
let any = Sort::Atom("?".into(), Box::new([]));

if let Sort::RareList(inner) = got {
return Self::assert_array_sort(pool, key, value, inner.as_sort().unwrap());
}

if let Sort::ParamSort(v, head) = got {
if let Some(Sort::Var(name)) = head.as_sort() {
if name == "Array" {
Expand Down
39 changes: 31 additions & 8 deletions carcara/src/parser/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -240,6 +240,15 @@ impl<'a, R: BufRead> Parser<'a, R> {
self.is_real_only_logic && self.problem.is_some()
}

fn is_bv_sort(sort: &Sort) -> bool {
match sort {
Sort::BitVec(_) => true,
Sort::ParamSort(_, head) => matches!(head.as_sort(), Some(Sort::Var(_))),
Sort::RareList(inner) => inner.as_sort().is_some_and(Self::is_bv_sort),
_ => false,
}
}

/// Constructs and sort checks an operation term.
fn make_op(&mut self, op: Operator, args: Vec<Rc<Term>>) -> Result<Rc<Term>, ParserError> {
let sorts: Vec<_> = args.iter().map(|t| self.pool.sort(t)).collect();
Expand Down Expand Up @@ -438,14 +447,14 @@ impl<'a, R: BufRead> Parser<'a, R> {
Operator::BvNot | Operator::BvNeg => {
assert_num_args(&args, 1)?;
for s in sorts {
if !matches!(s, Sort::BitVec(_)) && !s.is_polymorphic() {
if !Self::is_bv_sort(s) {
return Err(ParserError::ExpectedBvSort(s.clone()));
}
}
}
Operator::BvSize | Operator::UBvToInt | Operator::SBvToInt => {
assert_num_args(&args, 1)?;
if !matches!(sorts[0], Sort::BitVec(_)) && !sorts[0].is_polymorphic() {
if !Self::is_bv_sort(sorts[0]) {
return Err(ParserError::ExpectedBvSort(sorts[0].clone()));
}
}
Expand All @@ -467,7 +476,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
Operator::BvConcat => {
assert_num_args(&args, 2..)?;
for s in sorts {
if !matches!(s, Sort::BitVec(_)) && !s.is_polymorphic() {
if !Self::is_bv_sort(s) {
return Err(ParserError::ExpectedBvSort(s.clone()));
}
}
Expand All @@ -483,7 +492,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
| Operator::BvOr
| Operator::BvXor => {
assert_num_args(&args, 2..)?;
if !matches!(sorts[0], Sort::BitVec(_)) && !sorts[0].is_polymorphic() {
if !Self::is_bv_sort(sorts[0]) {
return Err(ParserError::ExpectedBvSort(sorts[0].clone()));
}
SortError::assert_all_eq(&sorts)?;
Expand All @@ -510,12 +519,12 @@ impl<'a, R: BufRead> Parser<'a, R> {
| Operator::BvSGt
| Operator::BvSGe => {
assert_num_args(&args, 2)?;
if !matches!(sorts[0], Sort::BitVec(_)) && !sorts[0].is_polymorphic() {
if !Self::is_bv_sort(sorts[0]) {
return Err(ParserError::ExpectedBvSort(sorts[0].clone()));
}
SortError::assert_all_eq(&sorts)?;
}
Operator::RareList => SortError::assert_all_eq(&sorts)?,
Operator::RareList => (),
}
Ok(self.pool.add(Term::Op(op, args)))
}
Expand Down Expand Up @@ -1583,7 +1592,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
*/
assert_num_args(&op_args, 2)?;
assert_num_args(&args, 1)?;
if !matches!(sorts[0], Sort::BitVec(_)) {
if !Self::is_bv_sort(sorts[0]) {
return Err(ParserError::ExpectedBvSort(sorts[0].clone()));
}
for arg in &op_args {
Expand Down Expand Up @@ -1628,7 +1637,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
} else {
return Err(ParserError::ExpectedIntegerConstant(op_args[0].clone()));
}
if !matches!(sorts[0], Sort::BitVec(_)) {
if !Self::is_bv_sort(sorts[0]) {
return Err(ParserError::ExpectedBvSort(sorts[0].clone()));
}
assert_indexed_op_args_value(&op_args, 0..)?;
Expand Down Expand Up @@ -1839,6 +1848,13 @@ impl<'a, R: BufRead> Parser<'a, R> {
[x, y] => Ok(Sort::Array(x.clone(), y.clone())),
_ => Err(ParserError::WrongNumberOfArgs(2.into(), args.len())),
},
"rare-list" | "RareList" => match args.as_slice() {
[elem] => Ok(Sort::RareList(elem.clone())),
[] => Ok(Sort::RareList(
self.pool.add(Term::Sort(Sort::Var("T".to_owned()))),
)),
_ => Err(ParserError::WrongNumberOfArgs(1.into(), args.len())),
},
other
if polymorphic
&& other.starts_with('@')
Expand Down Expand Up @@ -1921,6 +1937,13 @@ impl<'a, R: BufRead> Parser<'a, R> {
}
Token::OpenParen if polymorphic => {
let name = self.expect_symbol()?;
if matches!(name.as_str(), "rare-list" | "RareList") {
let args = self
.parse_sequence(|parser| Parser::parse_sort(parser, polymorphic), true)?;
return self
.make_sort(name, args, polymorphic)
.map_err(|e| Error::Parser(e, pos));
}
let args = self.parse_sequence(Self::parse_term, true)?;
let args = args
.into_iter()
Expand Down
Loading