smt_lang/problem/
constraint.rs

1use super::*;
2use crate::parser::Position;
3
4//------------------------- Id -------------------------
5
6#[derive(Clone, Copy, PartialEq, Eq, Debug, Hash)]
7pub struct ConstraintId(pub usize);
8
9impl Id for ConstraintId {
10    fn empty() -> Self {
11        Self(0)
12    }
13}
14
15//------------------------- Constraint -------------------------
16
17#[derive(Clone)]
18pub struct Constraint {
19    id: ConstraintId,
20    name: String,
21    expr: Expr,
22    position: Option<Position>,
23}
24
25impl Constraint {
26    pub fn new<S: Into<String>>(name: S, expr: Expr, position: Option<Position>) -> Self {
27        let id = ConstraintId::empty();
28        let name = name.into();
29        Self {
30            id,
31            name,
32            expr,
33            position,
34        }
35    }
36
37    pub fn expr(&self) -> &Expr {
38        &self.expr
39    }
40
41    //---------- Resolve ----------
42
43    pub fn resolve_type_expr(&mut self, entries: &TypeEntries) -> Result<(), Error> {
44        let e = self.expr.resolve_type(entries)?;
45        self.expr = e;
46        Ok(())
47    }
48
49    pub fn resolve_expr(&self, problem: &Problem, entries: &Entries) -> Result<Constraint, Error> {
50        let expr = self.expr.resolve(problem, entries)?;
51        Ok(Constraint {
52            id: self.id,
53            name: self.name.clone(),
54            expr,
55            position: self.position.clone(),
56        })
57    }
58
59    //---------- Parameter Size ----------
60
61    pub fn check_parameter_size(&self, problem: &Problem) -> Result<(), Error> {
62        self.expr.check_parameter_size(problem)
63    }
64
65    //---------- Typing ----------
66
67    pub fn check_type(&self, problem: &Problem) -> Result<(), Error> {
68        self.expr.check_type(problem)?;
69        check_type_bool(&self.expr, &self.expr.typ(problem))?;
70        Ok(())
71    }
72}
73
74//------------------------- Postion -------------------------
75
76impl WithPosition for Constraint {
77    fn position(&self) -> &Option<Position> {
78        &self.position
79    }
80}
81
82//------------------------- Named -------------------------
83
84impl Named<ConstraintId> for Constraint {
85    fn id(&self) -> ConstraintId {
86        self.id
87    }
88
89    fn set_id(&mut self, id: ConstraintId) {
90        self.id = id;
91    }
92
93    fn name(&self) -> &str {
94        &self.name
95    }
96}
97
98//------------------------- ToLang -------------------------
99
100impl ToLang for Constraint {
101    fn to_lang(&self, problem: &Problem) -> String {
102        format!(
103            "constraint {} = {}",
104            self.name(),
105            self.expr.to_lang(problem)
106        )
107    }
108}
smt_lang/problem/constraint.rs

smt_lang/problem/
constraint.rs
