smt_lang/solution/
attribute.rs

1use super::*;
2use crate::problem::*;
3use crate::solve::Smt;
4
5//-------------------------------------------------- Attribute Value --------------------------------------------------
6
7pub struct AttributeValue<T: Id> {
8    id: AttributeId<T>,
9    value: Value,
10}
11
12pub trait NewAttribute<T: Id> {
13    fn new(smt: &Smt, model: &z3::Model, instance: InstanceId, attribute: AttributeId<T>) -> Self;
14}
15
16impl NewAttribute<StructureId> for AttributeValue<StructureId> {
17    fn new(
18        smt: &Smt,
19        model: &z3::Model,
20        instance: InstanceId,
21        attribute: AttributeId<StructureId>,
22    ) -> Self {
23        let e = Expr::Instance(instance, None);
24        let expr = Expr::StrucAttribute(Box::new(e), attribute, None);
25        let value = Value::new(smt, model, &expr);
26        Self {
27            id: attribute,
28            value,
29        }
30    }
31}
32
33impl ToLang for AttributeValue<StructureId> {
34    fn to_lang(&self, problem: &Problem) -> String {
35        let attribute = problem.get(self.id).unwrap();
36        format!(
37            "{}: {} = {}",
38            attribute.name(),
39            attribute.typ().to_lang(problem),
40            self.value.to_lang(problem)
41        )
42    }
43}
44
45impl NewAttribute<ClassId> for AttributeValue<ClassId> {
46    fn new(
47        smt: &Smt,
48        model: &z3::Model,
49        instance: InstanceId,
50        attribute: AttributeId<ClassId>,
51    ) -> Self {
52        let e = Expr::Instance(instance, None);
53        let expr = Expr::ClassAttribute(Box::new(e), attribute, None);
54        let value = Value::new(smt, model, &expr);
55        Self {
56            id: attribute,
57            value,
58        }
59    }
60}
61
62impl ToLang for AttributeValue<ClassId> {
63    fn to_lang(&self, problem: &Problem) -> String {
64        let attribute = problem.get(self.id).unwrap();
65        format!(
66            "{}: {} = {}",
67            attribute.name(),
68            attribute.typ().to_lang(problem),
69            self.value.to_lang(problem)
70        )
71    }
72}
smt_lang/solution/attribute.rs

smt_lang/solution/
attribute.rs
