From 0d0fdd708b6d7e3af5c5fc3fe40f8bca68cfd53e Mon Sep 17 00:00:00 2001 From: Vinicius Gomes Date: Tue, 30 Jul 2024 20:42:02 -0300 Subject: [PATCH] Add is_mod_string_concat option to the Polyeq comparator --- carcara/src/ast/polyeq.rs | 122 +++++++++++++++++-------------- carcara/src/ast/tests.rs | 6 +- carcara/src/elaborator/polyeq.rs | 2 +- 3 files changed, 71 insertions(+), 59 deletions(-) diff --git a/carcara/src/ast/polyeq.rs b/carcara/src/ast/polyeq.rs index acdc9125..1137a04f 100644 --- a/carcara/src/ast/polyeq.rs +++ b/carcara/src/ast/polyeq.rs @@ -22,6 +22,15 @@ enum Concat { Term(Rc), } +fn to_concat(args: &[Rc]) -> Vec { + args.iter() + .map(|arg| match arg.as_ref() { + Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), + _ => Concat::Term(arg.clone()), + }) + .collect() +} + /// A trait that represents objects that can be compared for equality modulo reordering of /// equalities or alpha equivalence. pub trait Polyeq { @@ -36,7 +45,7 @@ pub trait Polyeq { /// This function records how long it takes to run, and adds that duration to the `time` argument. pub fn polyeq(a: &Rc, b: &Rc, time: &mut Duration) -> bool { let start = Instant::now(); - let result = Polyeq::eq(&mut PolyeqComparator::new(true, false, false), a, b); + let result = Polyeq::eq(&mut PolyeqComparator::new(true, false, false, false), a, b); *time += start.elapsed(); result } @@ -48,7 +57,7 @@ pub fn polyeq(a: &Rc, b: &Rc, time: &mut Duration) -> bool { /// `(and (= a b) (= b c) (= c d))`. pub fn polyeq_mod_nary(a: &Rc, b: &Rc, time: &mut Duration) -> bool { let start = Instant::now(); - let result = Polyeq::eq(&mut PolyeqComparator::new(true, false, true), a, b); + let result = Polyeq::eq(&mut PolyeqComparator::new(true, false, true, false), a, b); *time += start.elapsed(); result } @@ -60,7 +69,7 @@ pub fn polyeq_mod_nary(a: &Rc, b: &Rc, time: &mut Duration) -> bool pub fn tracing_polyeq_mod_nary(a: &Rc, b: &Rc, time: &mut Duration) -> (bool, usize) { let start = Instant::now(); - let mut comp = PolyeqComparator::new(true, false, true); + let mut comp = PolyeqComparator::new(true, false, true, false); let result = Polyeq::eq(&mut comp, a, b); *time += start.elapsed(); @@ -77,7 +86,19 @@ pub fn tracing_polyeq_mod_nary(a: &Rc, b: &Rc, time: &mut Duration) /// This function records how long it takes to run, and adds that duration to the `time` argument. pub fn alpha_equiv(a: &Rc, b: &Rc, time: &mut Duration) -> bool { let start = Instant::now(); - let result = Polyeq::eq(&mut PolyeqComparator::new(true, true, false), a, b); + let result = Polyeq::eq(&mut PolyeqComparator::new(true, true, false, false), a, b); + *time += start.elapsed(); + result +} + +/// Similar to `polyeq`, but also compares modulo the equality of String constants and String concatenations. +/// +/// That is, for this function, String concatenations with constant arguments can be +/// considered equal to the String constant of those arguments collected. For example, the term +/// `(str.++ "a" "bd" "d")` is considered equal to the String constant `"abcd"`. +pub fn polyeq_mod_string_concat(a: &Rc, b: &Rc, time: &mut Duration) -> bool { + let start = Instant::now(); + let result = Polyeq::eq(&mut PolyeqComparator::new(true, false, false, true), a, b); *time += start.elapsed(); result } @@ -111,6 +132,7 @@ pub struct PolyeqComparator { is_mod_reordering: bool, de_bruijn_map: Option, is_mod_nary: bool, + is_mod_string_concat: bool, current_depth: usize, max_depth: usize, @@ -125,13 +147,21 @@ impl PolyeqComparator { // - If `is_alpha_equivalence` is `true`, the comparator will compare terms for alpha /// equivalence. /// - If `is_mod_nary` is `true`, the comparator will compare terms modulo the expansion of - /// n-ary operators - pub fn new(is_mod_reordering: bool, is_alpha_equivalence: bool, is_mod_nary: bool) -> Self { + /// n-ary operators. + /// - If `is_mod_string_concat` is `true`, the comparator will compare terms modulo the collection of + /// String constants arguments in the String concatenation. + pub fn new( + is_mod_reordering: bool, + is_alpha_equivalence: bool, + is_mod_nary: bool, + is_mod_string_concat: bool, + ) -> Self { Self { is_mod_reordering, cache: HashMapStack::new(), de_bruijn_map: is_alpha_equivalence.then(DeBruijnMap::new), is_mod_nary, + is_mod_string_concat, current_depth: 0, max_depth: 0, } @@ -183,6 +213,13 @@ impl PolyeqComparator { op_b: Operator, args_b: &[Rc], ) -> bool { + // Modulo string concatenation + if self.is_mod_string_concat { + let concat_args_a: Vec = to_concat(args_a); + let concat_args_b: Vec = to_concat(args_b); + return self.compare_strings(concat_args_a, concat_args_b); + } + // Modulo reordering of equalities if self.is_mod_reordering { if let (Operator::Equals, [a_1, a_2], Operator::Equals, [b_1, b_2]) = @@ -277,15 +314,6 @@ impl PolyeqComparator { } fn remainder(&mut self, a: Vec, b: Vec) -> (Vec, Vec) { - fn to_concat(args: &[Rc]) -> Vec { - args.iter() - .map(|arg| match arg.as_ref() { - Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), - _ => Concat::Term(arg.clone()), - }) - .collect() - } - match (a.first(), b.first()) { (None | Some(_), None) | (None, Some(_)) => (a, b), (Some(a_head), Some(b_head)) => match (a_head, b_head) { @@ -469,45 +497,6 @@ impl Polyeq for Term { args: args_b, }, ) => op_a == op_b && op_args_a == op_args_b && Polyeq::eq(comp, args_a, args_b), - (Term::Op(Operator::StrConcat, args_a), Term::Op(Operator::StrConcat, args_b)) => { - let concat_args_a: Vec = args_a - .iter() - .map(|arg| match arg.as_ref() { - Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), - _ => Concat::Term(arg.clone()), - }) - .collect(); - let concat_args_b: Vec = args_b - .iter() - .map(|arg| match arg.as_ref() { - Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), - _ => Concat::Term(arg.clone()), - }) - .collect(); - comp.compare_strings(concat_args_a, concat_args_b) - } - (Term::Op(Operator::StrConcat, args_a), Term::Const(Constant::String(b))) => { - let concat_args_a: Vec = args_a - .iter() - .map(|arg| match arg.as_ref() { - Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), - _ => Concat::Term(arg.clone()), - }) - .collect(); - let concat_args_b = vec![Concat::Constant(b.clone())]; - comp.compare_strings(concat_args_a, concat_args_b) - } - (Term::Const(Constant::String(a)), Term::Op(Operator::StrConcat, args_b)) => { - let concat_args_a = vec![Concat::Constant(a.clone())]; - let concat_args_b: Vec = args_b - .iter() - .map(|arg| match arg.as_ref() { - Term::Const(Constant::String(s)) => Concat::Constant(s.clone()), - _ => Concat::Term(arg.clone()), - }) - .collect(); - comp.compare_strings(concat_args_a, concat_args_b) - } (Term::Op(op_a, args_a), Term::Op(op_b, args_b)) => { comp.compare_op(*op_a, args_a, *op_b, args_b) @@ -572,7 +561,30 @@ impl Polyeq for Term { _ => false, } } - _ => false, + _ => { + if comp.is_mod_string_concat { + return match (a, b) { + ( + Term::Op(Operator::StrConcat, args_a), + Term::Const(Constant::String(b)), + ) => { + let concat_args_a: Vec = to_concat(args_a); + let concat_args_b = vec![Concat::Constant(b.clone())]; + comp.compare_strings(concat_args_a, concat_args_b) + } + ( + Term::Const(Constant::String(a)), + Term::Op(Operator::StrConcat, args_b), + ) => { + let concat_args_a = vec![Concat::Constant(a.clone())]; + let concat_args_b: Vec = to_concat(args_b); + comp.compare_strings(concat_args_a, concat_args_b) + } + _ => false, + }; + } + false + } } } } diff --git a/carcara/src/ast/tests.rs b/carcara/src/ast/tests.rs index bec7dbff..1317dde7 100644 --- a/carcara/src/ast/tests.rs +++ b/carcara/src/ast/tests.rs @@ -49,9 +49,9 @@ fn test_polyeq() { for (i, (a, b)) in cases.iter().enumerate() { let [a, b] = parse_terms(&mut pool, definitions, [a, b]); let mut comp = match test_type { - TestType::ModReordering => PolyeqComparator::new(true, false, false), - TestType::AlphaEquiv => PolyeqComparator::new(true, true, false), - TestType::ModNary => PolyeqComparator::new(false, false, true), + TestType::ModReordering => PolyeqComparator::new(true, false, false, false), + TestType::AlphaEquiv => PolyeqComparator::new(true, true, false, false), + TestType::ModNary => PolyeqComparator::new(false, false, true, false), }; assert!( Polyeq::eq(&mut comp, &a, &b), diff --git a/carcara/src/elaborator/polyeq.rs b/carcara/src/elaborator/polyeq.rs index adc7c447..ce89a23b 100644 --- a/carcara/src/elaborator/polyeq.rs +++ b/carcara/src/elaborator/polyeq.rs @@ -18,7 +18,7 @@ impl<'a> PolyeqElaborator<'a> { ids: id_helper, root_depth, cache: HashMapStack::new(), - checker: PolyeqComparator::new(true, is_alpha_equivalence, false), + checker: PolyeqComparator::new(true, is_alpha_equivalence, false, false), context: is_alpha_equivalence.then(ContextStack::new), } }