smt_lang/problem/
search.rs

1use super::*;
2use fraction::Fraction;
3
4#[derive(Clone)]
5pub enum Bound {
6    Int(isize),
7    Real(Fraction),
8}
9
10impl std::fmt::Display for Bound {
11    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
12        match self {
13            Bound::Int(v) => write!(f, "{}", v),
14            Bound::Real(v) => write!(f, "{}", v),
15        }
16    }
17}
18
19#[derive(Clone)]
20pub enum Search {
21    Solve,
22    Optimize(Box<Expr>, Bound, bool),
23}
24
25impl Search {
26    pub fn is_optimize(&self) -> bool {
27        match self {
28            Search::Solve => false,
29            Search::Optimize(_, _, _) => true,
30        }
31    }
32
33    pub fn resolve_type_expr(&self, entries: &TypeEntries) -> Result<Self, Error> {
34        match self {
35            Search::Solve => Ok(self.clone()),
36            Search::Optimize(e, bound, minimize) => {
37                let e = e.resolve_type(entries)?;
38                Ok(Search::Optimize(Box::new(e), bound.clone(), *minimize))
39            }
40        }
41    }
42
43    pub fn resolve_expr(&self, problem: &Problem, entries: &Entries) -> Result<Self, Error> {
44        match self {
45            Search::Solve => Ok(self.clone()),
46            Search::Optimize(e, bound, minimize) => {
47                let e = e.resolve(problem, entries)?;
48                Ok(Search::Optimize(Box::new(e), bound.clone(), *minimize))
49            }
50        }
51    }
52
53    pub fn check_parameter_size(&self, problem: &Problem) -> Result<(), Error> {
54        match self {
55            Search::Solve => Ok(()),
56            Search::Optimize(e, _, _) => e.check_parameter_size(problem),
57        }
58    }
59
60    pub fn check_type(&self, problem: &Problem) -> Result<(), Error> {
61        match self {
62            Search::Solve => Ok(()),
63            Search::Optimize(e, bound, _) => {
64                e.check_type(problem)?;
65                let et = e.typ(problem);
66                match bound {
67                    Bound::Int(_) => check_type_integer(e, &et),
68                    Bound::Real(_) => check_type_real(e, &et),
69                }
70            }
71        }
72    }
73}
74
75//------------------------- ToLang -------------------------
76
77impl ToLang for Search {
78    fn to_lang(&self, problem: &Problem) -> String {
79        match self {
80            Search::Solve => "solve\n".to_string(),
81            Search::Optimize(e, bound, minimize) => {
82                if *minimize {
83                    format!("minimize {} until {}", e.to_lang(problem), bound)
84                } else {
85                    format!("maximize {} until {}", e.to_lang(problem), bound)
86                }
87            }
88        }
89    }
90}
smt_lang/problem/search.rs

smt_lang/problem/
search.rs
