smt_lang/
combine.rs

1use super::problem::*;
2
3#[derive(Clone)]
4pub struct Combine<T: Clone> {
5    elements: Vec<Vec<T>>,
6    index: Vec<usize>,
7}
8
9impl<T: Clone> Combine<T> {
10    pub fn new(elements: Vec<Vec<T>>) -> Self {
11        let index = elements.iter().map(|_| 0).collect();
12        Self { elements, index }
13    }
14
15    pub fn index(&self) -> &Vec<usize> {
16        &self.index
17    }
18
19    pub fn values(&self) -> Vec<T> {
20        self.elements
21            .iter()
22            .zip(self.index.iter())
23            .map(|(v, i)| v[*i].clone())
24            .collect()
25    }
26
27    pub fn step(&mut self) -> bool {
28        for i in 0..self.index.len() {
29            let n = self.index[i];
30            if n < self.elements[i].len() - 1 {
31                self.index[i] += 1;
32                return true;
33            }
34            if i != self.index.len() - 1 {
35                for j in 0..=i {
36                    self.index[j] = 0;
37                }
38            }
39        }
40        false
41    }
42
43    pub fn next(&mut self) -> Option<Vec<T>> {
44        if self.step() {
45            Some(self.values())
46        } else {
47            None
48        }
49    }
50}
51
52pub fn combine_all(problem: &Problem, parameters: &Vec<Parameter>, expr: &Expr) -> Vec<Expr> {
53    let params_all = parameters.iter().map(|p| p.typ().all(problem)).collect();
54    let params_exp = parameters
55        .iter()
56        .map(|p| Expr::Parameter(p.clone()))
57        .collect::<Vec<_>>();
58    let mut combine = Combine::new(params_all);
59    let mut v = Vec::new();
60    loop {
61        let values = combine.values();
62        let all = params_exp.clone().into_iter().zip(values.clone()).collect();
63        let e = expr.substitute_all(all);
64        v.push(e);
65        if !combine.step() {
66            break;
67        }
68    }
69    v
70}
smt_lang/combine.rs

smt_lang/
combine.rs
