Skip to content

Commit

Permalink
Add is_mod_string_concat option to the Polyeq comparator
Browse files Browse the repository at this point in the history
  • Loading branch information
@vinisilvag
vinisilvag committed Aug 19, 2024
1 parent bacc028 commit 0d0fdd7
Show file tree
Hide file tree
Showing 3 changed files with 71 additions and 59 deletions.
122 changes: 67 additions & 55 deletions carcara/src/ast/polyeq.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,15 @@ enum Concat {
Term(Rc<Term>),
}

fn to_concat(args: &[Rc<Term>]) -> Vec<Concat> {
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 {
Expand All @@ -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<Term>, b: &Rc<Term>, 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
}
Expand All @@ -48,7 +57,7 @@ pub fn polyeq(a: &Rc<Term>, b: &Rc<Term>, time: &mut Duration) -> bool {
/// `(and (= a b) (= b c) (= c d))`.
pub fn polyeq_mod_nary(a: &Rc<Term>, b: &Rc<Term>, 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
}
Expand All @@ -60,7 +69,7 @@ pub fn polyeq_mod_nary(a: &Rc<Term>, b: &Rc<Term>, time: &mut Duration) -> bool
pub fn tracing_polyeq_mod_nary(a: &Rc<Term>, b: &Rc<Term>, 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();
Expand All @@ -77,7 +86,19 @@ pub fn tracing_polyeq_mod_nary(a: &Rc<Term>, b: &Rc<Term>, 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<Term>, b: &Rc<Term>, 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<Term>, b: &Rc<Term>, 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
}
Expand Down Expand Up @@ -111,6 +132,7 @@ pub struct PolyeqComparator {
is_mod_reordering: bool,
de_bruijn_map: Option<DeBruijnMap>,
is_mod_nary: bool,
is_mod_string_concat: bool,

current_depth: usize,
max_depth: usize,
Expand All @@ -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,
}
Expand Down Expand Up @@ -183,6 +213,13 @@ impl PolyeqComparator {
op_b: Operator,
args_b: &[Rc<Term>],
) -> bool {
// Modulo string concatenation
if self.is_mod_string_concat {
let concat_args_a: Vec<Concat> = to_concat(args_a);
let concat_args_b: Vec<Concat> = 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]) =
Expand Down Expand Up @@ -277,15 +314,6 @@ impl PolyeqComparator {
}

fn remainder(&mut self, a: Vec<Concat>, b: Vec<Concat>) -> (Vec<Concat>, Vec<Concat>) {
fn to_concat(args: &[Rc<Term>]) -> Vec<Concat> {
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) {
Expand Down Expand Up @@ -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<Concat> = 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> = 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<Concat> = 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<Concat> = 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)
Expand Down Expand Up @@ -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<Concat> = 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<Concat> = to_concat(args_b);
comp.compare_strings(concat_args_a, concat_args_b)
}
_ => false,
};
}
false
}
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions carcara/src/ast/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
2 changes: 1 addition & 1 deletion carcara/src/elaborator/polyeq.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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),
}
}
Expand Down

0 comments on commit 0d0fdd7

Please sign in to comment.