smt-lang 0.7.5

Sat Modulo Theory Language
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90

use super::*;
use fraction::Fraction;

#[derive(Clone)]
pub enum Bound {
    Int(isize),
    Real(Fraction),
}

impl std::fmt::Display for Bound {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Bound::Int(v) => write!(f, "{}", v),
            Bound::Real(v) => write!(f, "{}", v),
        }
    }
}

#[derive(Clone)]
pub enum Search {
    Solve,
    Optimize(Box<Expr>, Bound, bool),
}

impl Search {
    pub fn is_optimize(&self) -> bool {
        match self {
            Search::Solve => false,
            Search::Optimize(_, _, _) => true,
        }
    }

    pub fn resolve_type_expr(&self, entries: &TypeEntries) -> Result<Self, Error> {
        match self {
            Search::Solve => Ok(self.clone()),
            Search::Optimize(e, bound, minimize) => {
                let e = e.resolve_type(entries)?;
                Ok(Search::Optimize(Box::new(e), bound.clone(), *minimize))
            }
        }
    }

    pub fn resolve_expr(&self, problem: &Problem, entries: &Entries) -> Result<Self, Error> {
        match self {
            Search::Solve => Ok(self.clone()),
            Search::Optimize(e, bound, minimize) => {
                let e = e.resolve(problem, entries)?;
                Ok(Search::Optimize(Box::new(e), bound.clone(), *minimize))
            }
        }
    }

    pub fn check_parameter_size(&self, problem: &Problem) -> Result<(), Error> {
        match self {
            Search::Solve => Ok(()),
            Search::Optimize(e, _, _) => e.check_parameter_size(problem),
        }
    }

    pub fn check_type(&self, problem: &Problem) -> Result<(), Error> {
        match self {
            Search::Solve => Ok(()),
            Search::Optimize(e, bound, _) => {
                e.check_type(problem)?;
                let et = e.typ(problem);
                match bound {
                    Bound::Int(_) => check_type_integer(e, &et),
                    Bound::Real(_) => check_type_real(e, &et),
                }
            }
        }
    }
}

//------------------------- ToLang -------------------------

impl ToLang for Search {
    fn to_lang(&self, problem: &Problem) -> String {
        match self {
            Search::Solve => "solve\n".to_string(),
            Search::Optimize(e, bound, minimize) => {
                if *minimize {
                    format!("minimize {} until {}", e.to_lang(problem), bound)
                } else {
                    format!("maximize {} until {}", e.to_lang(problem), bound)
                }
            }
        }
    }
}