This commit is contained in:
Edward Chen
2022-04-27 21:14:45 -04:00
parent 47fbdb8de8
commit 3a065c021a
2 changed files with 83 additions and 21 deletions

View File

@@ -248,28 +248,32 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache<Term>) -> Term {
Op::Map(op) => match (get(0).as_array_opt(), get(1).as_array_opt()) {
(Some(a), Some(b)) => {
assert!(a.size == b.size);
let mut new_map: BTreeMap<Value, Value> = BTreeMap::new();
for (a_ind, a_val) in &a.map {
let b_val = &b.map[a_ind];
let res = fold_cache(
&term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))],
cache,
);
match res.as_value_opt() {
Some(r) => {
new_map.insert(a_ind.clone(), r.clone());
}
None => {
panic!("Unale to constant constant fold idx: {}", a_ind);
}
}
for t in a. {
}
let new_arr = Array::new(
a.key_sort.clone(),
Box::new(a.key_sort.default_value()),
new_map,
a.size,
);
// let mut new_map: BTreeMap<Value, Value> = BTreeMap::new();
// for (a_ind, a_val) in &a.map {
// let b_val = &b.map[a_ind];
// let res = &term![*op.clone(); leaf_term(Op::Const(a_val.clone())), leaf_term(Op::Const(b_val.clone()))];
// match res.as_value_opt() {
// Some(r) => {
// new_map.insert(a_ind.clone(), r.clone());
// }
// None => {
// panic!("Unale to constant constant fold idx: {}", a_ind);
// }
// }
// }
// let new_arr = Array::new(
// a.key_sort.clone(),
// Box::new(a.key_sort.default_value()),
// new_map,
// a.size,
// );
Some(leaf_term(Op::Const(Value::Array(new_arr))))
}
_ => None,

View File

@@ -31,6 +31,7 @@ use log::debug;
use rug::Integer;
use std::collections::BTreeMap;
use std::fmt::{self, Debug, Display, Formatter};
use std::iter::Peekable;
use std::sync::{Arc, RwLock};
pub mod bv;
@@ -721,6 +722,63 @@ impl Array {
self.check_idx(idx);
self.map.get(idx).unwrap_or(&*self.default).clone()
}
/// Iter
pub fn into_iter(&self) -> std::collections::btree_map::IntoIter<Value, Value> {
self.map.into_iter()
}
}
/// Merge two Array Iterators
struct ArrayMerge {
left: Peekable<std::collections::btree_map::IntoIter<Value, Value>>,
right: Peekable<std::collections::btree_map::IntoIter<Value, Value>>,
left_dfl: Value,
right_dfl: Value,
}
impl ArrayMerge {
pub fn new(a: Array, b: Array) -> Self {
if a.size != b.size {
panic!("IR Arrays have different lengths: {}, {}", a.size, b.size);
}
if a.key_sort != b.key_sort {
panic!(
"IR Arrays have different key sorts: {}, {}",
a.key_sort, b.key_sort
);
}
if a.default.sort() != b.default.sort() {
panic!(
"IR Arrays default values have different key sorts: {}, {}",
a.default.sort(),
b.default.sort()
);
}
Self {
left: a.into_iter().peekable(),
right: b.into_iter().peekable(),
left_dfl: *a.default,
right_dfl: *b.default,
}
}
pub fn peek(&self) -> (Option<&(Value, Value)>, Option<&(Value, Value)>) {
(self.left.peek(), self.right.peek())
}
pub fn left_next(&self) -> Option<(Value, Value)> {
self.left.next()
}
pub fn right_next(&self) -> Option<(Value, Value)> {
self.right.next()
}
pub fn next(&self) -> (Option<(Value, Value)>, Option<(Value, Value)>) {
(self.left.next(), self.right.next())
}
}
impl Display for Value {