conjure_cp_core/ast/declaration.rs
1use super::categories::{Category, CategoryOf};
2use super::name::Name;
3use super::serde::{DefaultWithId, HasId, IdPtr, ObjId, PtrAsInner};
4use super::{
5 DecisionVariable, DomainPtr, Expression, GroundDomain, HasDomain, Moo, RecordEntry, ReturnType,
6 Typeable,
7};
8use parking_lot::{
9 MappedRwLockReadGuard, MappedRwLockWriteGuard, RwLock, RwLockReadGuard, RwLockWriteGuard,
10};
11use serde::{Deserialize, Serialize};
12use serde_with::serde_as;
13use std::any::TypeId;
14use std::fmt::{Debug, Display};
15use std::mem;
16use std::sync::Arc;
17use std::sync::atomic::{AtomicU32, Ordering};
18use uniplate::{Biplate, Tree, Uniplate};
19
20/// Global counter of declarations.
21/// Note that the counter is shared between all threads
22/// Thus, when running multiple models in parallel, IDs may
23/// be different with every run depending on scheduling order
24static DECLARATION_PTR_ID_COUNTER: AtomicU32 = const { AtomicU32::new(0) };
25
26#[doc(hidden)]
27/// Resets the id counter of `DeclarationPtr` to 0.
28///
29/// This is probably always a bad idea.
30pub fn reset_declaration_id_unchecked() {
31 let _ = DECLARATION_PTR_ID_COUNTER.swap(0, Ordering::Relaxed);
32}
33
34/// A shared pointer to a [`Declaration`].
35///
36/// Two declaration pointers are equal if they point to the same underlying declaration.
37///
38/// # Id
39///
40/// The id of `DeclarationPtr` obeys the following invariants:
41///
42/// 1. Declaration pointers have the same id if they point to the same
43/// underlying declaration.
44///
45/// 2. The id is immutable.
46///
47/// 3. Changing the declaration pointed to by the declaration pointer does not change the id. This
48/// allows declarations to be updated by replacing them with a newer version of themselves.
49///
50/// `Ord`, `Hash`, and `Eq` use id for comparisons.
51/// # Serde
52///
53/// Declaration pointers can be serialised using the following serializers:
54///
55/// + [`DeclarationPtrFull`](serde::DeclarationPtrFull)
56/// + [`DeclarationPtrAsId`](serde::DeclarationPtrAsId)
57///
58/// See their documentation for more information.
59#[derive(Clone, Debug)]
60pub struct DeclarationPtr
61where
62 Self: Send + Sync,
63{
64 // the shared bits of the pointer
65 inner: Arc<DeclarationPtrInner>,
66}
67
68// The bits of a declaration that are shared between all pointers.
69#[derive(Debug)]
70struct DeclarationPtrInner {
71 // We don't want this to be mutable, as `HashMap` and `BTreeMap` rely on the hash or order of
72 // keys to be unchanging.
73 //
74 // See: https://rust-lang.github.io/rust-clippy/master/index.html#mutable_key_type
75 id: ObjId,
76
77 // The contents of the declaration itself should be mutable.
78 value: RwLock<Declaration>,
79}
80
81impl DeclarationPtrInner {
82 fn new(value: RwLock<Declaration>) -> Arc<DeclarationPtrInner> {
83 Arc::new(DeclarationPtrInner {
84 id: ObjId {
85 type_name: ustr::ustr(DeclarationPtr::TYPE_NAME),
86 object_id: DECLARATION_PTR_ID_COUNTER.fetch_add(1, Ordering::Relaxed),
87 },
88 value,
89 })
90 }
91
92 // SAFETY: only use if you are really really sure you arn't going to break the id invariants of
93 // DeclarationPtr and HasId!
94 fn new_with_id_unchecked(value: RwLock<Declaration>, id: ObjId) -> Arc<DeclarationPtrInner> {
95 Arc::new(DeclarationPtrInner { id, value })
96 }
97}
98
99#[allow(dead_code)]
100impl DeclarationPtr {
101 /******************************/
102 /* Constructors */
103 /******************************/
104
105 /// Creates a `DeclarationPtr` for the given `Declaration`.
106 fn from_declaration(declaration: Declaration) -> DeclarationPtr {
107 DeclarationPtr {
108 inner: DeclarationPtrInner::new(RwLock::new(declaration)),
109 }
110 }
111
112 /// Creates a new declaration.
113 ///
114 /// # Examples
115 ///
116 /// ```
117 /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
118 ///
119 /// // letting MyDomain be int(1..5)
120 /// let declaration = DeclarationPtr::new(
121 /// Name::User("MyDomain".into()),
122 /// DeclarationKind::DomainLetting(Domain::int(vec![
123 /// Range::Bounded(1,5)])));
124 /// ```
125 pub fn new(name: Name, kind: DeclarationKind) -> DeclarationPtr {
126 DeclarationPtr::from_declaration(Declaration::new(name, kind))
127 }
128
129 /// Creates a new find declaration.
130 ///
131 /// # Examples
132 ///
133 /// ```
134 /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
135 ///
136 /// // find x: int(1..5)
137 /// let declaration = DeclarationPtr::new_find(
138 /// Name::User("x".into()),
139 /// Domain::int(vec![Range::Bounded(1,5)]));
140 ///
141 /// ```
142 pub fn new_find(name: Name, domain: DomainPtr) -> DeclarationPtr {
143 let kind = DeclarationKind::Find(DecisionVariable::new(domain));
144 DeclarationPtr::new(name, kind)
145 }
146
147 /// Creates a new given declaration.
148 ///
149 /// # Examples
150 ///
151 /// ```
152 /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
153 ///
154 /// // given n: int(1..5)
155 /// let declaration = DeclarationPtr::new_given(
156 /// Name::User("n".into()),
157 /// Domain::int(vec![Range::Bounded(1,5)]));
158 ///
159 /// ```
160 pub fn new_given(name: Name, domain: DomainPtr) -> DeclarationPtr {
161 let kind = DeclarationKind::Given(domain);
162 DeclarationPtr::new(name, kind)
163 }
164
165 /// Creates a new quantified declaration for local comprehension scopes.
166 ///
167 /// Used when creating the quantified variable in a generator.
168 pub fn new_quantified(name: Name, domain: DomainPtr) -> DeclarationPtr {
169 DeclarationPtr::new(
170 name,
171 DeclarationKind::Quantified(Quantified {
172 domain,
173 generator: None,
174 }),
175 )
176 }
177
178 /// Creates a quantified declaration backed by a generator declaration.
179 ///
180 /// This is used in comprehensions to refer to a quantified variable that is already defined using a generator.
181 pub fn new_quantified_from_generator(decl: &DeclarationPtr) -> Option<DeclarationPtr> {
182 let kind = DeclarationKind::Quantified(Quantified {
183 domain: decl.domain()?,
184 generator: Some(decl.clone()),
185 });
186 Some(DeclarationPtr::new(decl.name().clone(), kind))
187 }
188
189 /// Creates a new value letting declaration.
190 ///
191 /// # Examples
192 ///
193 /// ```
194 /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
195 /// Literal,Atom,Moo};
196 /// use conjure_cp_core::{matrix_expr,ast::Metadata};
197 ///
198 /// // letting n be 10 + 10
199 /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
200 /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
201 /// let declaration = DeclarationPtr::new_value_letting(
202 /// Name::User("n".into()),
203 /// expression);
204 ///
205 /// ```
206 pub fn new_value_letting(name: Name, expression: Expression) -> DeclarationPtr {
207 let kind = DeclarationKind::ValueLetting(expression);
208 DeclarationPtr::new(name, kind)
209 }
210
211 /// Creates a new domain letting declaration.
212 ///
213 /// # Examples
214 ///
215 /// ```
216 /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
217 ///
218 /// // letting MyDomain be int(1..5)
219 /// let declaration = DeclarationPtr::new_domain_letting(
220 /// Name::User("MyDomain".into()),
221 /// Domain::int(vec![Range::Bounded(1,5)]));
222 ///
223 /// ```
224 pub fn new_domain_letting(name: Name, domain: DomainPtr) -> DeclarationPtr {
225 let kind = DeclarationKind::DomainLetting(domain);
226 DeclarationPtr::new(name, kind)
227 }
228
229 /// Creates a new record field declaration.
230 ///
231 /// # Examples
232 ///
233 /// ```
234 /// use conjure_cp_core::ast::{DeclarationPtr,Name,RecordEntry,Domain,Range};
235 ///
236 /// // create declaration for field A in `find rec: record {A: int(0..1), B: int(0..2)}`
237 ///
238 /// let field = RecordEntry {
239 /// name: Name::User("n".into()),
240 /// domain: Domain::int(vec![Range::Bounded(1,5)])
241 /// };
242 ///
243 /// let declaration = DeclarationPtr::new_record_field(field);
244 /// ```
245 pub fn new_record_field(entry: RecordEntry) -> DeclarationPtr {
246 let kind = DeclarationKind::RecordField(entry.domain);
247 DeclarationPtr::new(entry.name, kind)
248 }
249
250 /**********************************************/
251 /* Declaration accessor methods */
252 /**********************************************/
253
254 /// Gets the domain of the declaration, if it has one.
255 ///
256 /// # Examples
257 ///
258 /// ```
259 /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};
260 ///
261 /// // find a: int(1..5)
262 /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
263 ///
264 /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)])))
265 ///
266 /// ```
267 pub fn domain(&self) -> Option<DomainPtr> {
268 match &self.kind() as &DeclarationKind {
269 DeclarationKind::Find(var) => Some(var.domain_of()),
270 DeclarationKind::ValueLetting(e) => e.domain_of(),
271 DeclarationKind::DomainLetting(domain) => Some(domain.clone()),
272 DeclarationKind::Given(domain) => Some(domain.clone()),
273 DeclarationKind::Quantified(inner) => Some(inner.domain.clone()),
274 DeclarationKind::RecordField(domain) => Some(domain.clone()),
275 }
276 }
277
278 /// Gets the domain of the declaration and fully resolve it
279 pub fn resolved_domain(&self) -> Option<Moo<GroundDomain>> {
280 self.domain()?.resolve()
281 }
282
283 /// Gets the kind of the declaration.
284 ///
285 /// # Examples
286 ///
287 /// ```
288 /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};
289 ///
290 /// // find a: int(1..5)
291 /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
292 /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))
293 /// ```
294 pub fn kind(&self) -> MappedRwLockReadGuard<'_, DeclarationKind> {
295 self.map(|x| &x.kind)
296 }
297
298 /// Gets the name of the declaration.
299 ///
300 /// # Examples
301 ///
302 /// ```
303 /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
304 ///
305 /// // find a: int(1..5)
306 /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
307 ///
308 /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))
309 /// ```
310 pub fn name(&self) -> MappedRwLockReadGuard<'_, Name> {
311 self.map(|x| &x.name)
312 }
313
314 /// This declaration as a decision variable, if it is one.
315 pub fn as_var(&self) -> Option<MappedRwLockReadGuard<'_, DecisionVariable>> {
316 RwLockReadGuard::try_map(self.read(), |x| {
317 if let DeclarationKind::Find(var) = &x.kind {
318 Some(var)
319 } else {
320 None
321 }
322 })
323 .ok()
324 }
325
326 /// This declaration as a mutable decision variable, if it is one.
327 pub fn as_var_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DecisionVariable>> {
328 RwLockWriteGuard::try_map(self.write(), |x| {
329 if let DeclarationKind::Find(var) = &mut x.kind {
330 Some(var)
331 } else {
332 None
333 }
334 })
335 .ok()
336 }
337
338 /// This declaration as a domain letting, if it is one.
339 pub fn as_domain_letting(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
340 RwLockReadGuard::try_map(self.read(), |x| {
341 if let DeclarationKind::DomainLetting(domain) = &x.kind {
342 Some(domain)
343 } else {
344 None
345 }
346 })
347 .ok()
348 }
349
350 /// This declaration as a mutable domain letting, if it is one.
351 pub fn as_domain_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
352 RwLockWriteGuard::try_map(self.write(), |x| {
353 if let DeclarationKind::DomainLetting(domain) = &mut x.kind {
354 Some(domain)
355 } else {
356 None
357 }
358 })
359 .ok()
360 }
361
362 /// This declaration as a value letting, if it is one.
363 pub fn as_value_letting(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
364 RwLockReadGuard::try_map(self.read(), |x| {
365 if let DeclarationKind::ValueLetting(expression) = &x.kind {
366 Some(expression)
367 } else {
368 None
369 }
370 })
371 .ok()
372 }
373
374 /// This declaration as a mutable value letting, if it is one.
375 pub fn as_value_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, Expression>> {
376 RwLockWriteGuard::try_map(self.write(), |x| {
377 if let DeclarationKind::ValueLetting(expression) = &mut x.kind {
378 Some(expression)
379 } else {
380 None
381 }
382 })
383 .ok()
384 }
385
386 /// Changes the name in this declaration, returning the old one.
387 ///
388 /// # Examples
389 ///
390 /// ```
391 /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};
392 ///
393 /// // find a: int(1..5)
394 /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
395 ///
396 /// let old_name = declaration.replace_name(Name::User("b".into()));
397 /// assert_eq!(old_name,Name::User("a".into()));
398 /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));
399 /// ```
400 pub fn replace_name(&mut self, name: Name) -> Name {
401 let mut decl = self.write();
402 std::mem::replace(&mut decl.name, name)
403 }
404
405 /// Replaces the underlying declaration kind and returns the previous kind.
406 /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.
407 pub fn replace_kind(&mut self, kind: DeclarationKind) -> DeclarationKind {
408 let mut decl = self.write();
409 std::mem::replace(&mut decl.kind, kind)
410 }
411
412 /*****************************************/
413 /* Pointer utility methods */
414 /*****************************************/
415
416 // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for
417 // convenience.
418
419 /// Read the underlying [Declaration].
420 ///
421 /// Will block the current thread until no other thread has a write lock.
422 /// Attempting to get a read lock if the current thread already has one
423 /// **will** cause it to deadlock.
424 /// The lock is released when the returned guard goes out of scope.
425 fn read(&self) -> RwLockReadGuard<'_, Declaration> {
426 self.inner.value.read()
427 }
428
429 /// Write the underlying [Declaration].
430 ///
431 /// Will block the current thread until no other thread has a read or write lock.
432 /// The lock is released when the returned guard goes out of scope.
433 fn write(&mut self) -> RwLockWriteGuard<'_, Declaration> {
434 self.inner.value.write()
435 }
436
437 /// Creates a new declaration pointer with the same contents as `self` that is not shared with
438 /// anyone else.
439 ///
440 /// As the resulting pointer is unshared, it will have a new id.
441 ///
442 /// # Examples
443 ///
444 /// ```
445 /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
446 ///
447 /// // find a: int(1..5)
448 /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
449 ///
450 /// let mut declaration2 = declaration.clone();
451 ///
452 /// declaration2.replace_name(Name::User("b".into()));
453 ///
454 /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
455 /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
456 ///
457 /// declaration2 = declaration2.detach();
458 ///
459 /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
460 ///
461 /// declaration2.replace_name(Name::User("c".into()));
462 ///
463 /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
464 /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));
465 /// ```
466 pub fn detach(self) -> DeclarationPtr {
467 // despite having the same contents, the new declaration pointer is unshared, so it should
468 // get a new id.
469 let value = self.inner.value.read().clone();
470 DeclarationPtr {
471 inner: DeclarationPtrInner::new(RwLock::new(value)),
472 }
473 }
474
475 /// Applies `f` to the declaration, returning the result as a reference.
476 fn map<U>(&self, f: impl FnOnce(&Declaration) -> &U) -> MappedRwLockReadGuard<'_, U> {
477 RwLockReadGuard::map(self.read(), f)
478 }
479
480 /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.
481 fn map_mut<U>(
482 &mut self,
483 f: impl FnOnce(&mut Declaration) -> &mut U,
484 ) -> MappedRwLockWriteGuard<'_, U> {
485 RwLockWriteGuard::map(self.write(), f)
486 }
487
488 /// Replaces the declaration with a new one, returning the old value, without deinitialising
489 /// either one.
490 fn replace(&mut self, declaration: Declaration) -> Declaration {
491 let mut guard = self.write();
492 let ans = mem::replace(&mut *guard, declaration);
493 drop(guard);
494 ans
495 }
496}
497
498impl CategoryOf for DeclarationPtr {
499 fn category_of(&self) -> Category {
500 match &self.kind() as &DeclarationKind {
501 DeclarationKind::Find(decision_variable) => decision_variable.category_of(),
502 DeclarationKind::ValueLetting(expression) => expression.category_of(),
503 DeclarationKind::DomainLetting(_) => Category::Constant,
504 DeclarationKind::Given(_) => Category::Parameter,
505 DeclarationKind::Quantified(..) => Category::Quantified,
506 DeclarationKind::RecordField(_) => Category::Bottom,
507 }
508 }
509}
510impl HasId for DeclarationPtr {
511 const TYPE_NAME: &'static str = "DeclarationPtrInner";
512 fn id(&self) -> ObjId {
513 self.inner.id.clone()
514 }
515}
516
517impl DefaultWithId for DeclarationPtr {
518 fn default_with_id(id: ObjId) -> Self {
519 DeclarationPtr {
520 inner: DeclarationPtrInner::new_with_id_unchecked(
521 RwLock::new(Declaration {
522 name: Name::User("_UNKNOWN".into()),
523 kind: DeclarationKind::ValueLetting(false.into()),
524 }),
525 id,
526 ),
527 }
528 }
529}
530
531impl Typeable for DeclarationPtr {
532 fn return_type(&self) -> ReturnType {
533 match &self.kind() as &DeclarationKind {
534 DeclarationKind::Find(var) => var.return_type(),
535 DeclarationKind::ValueLetting(expression) => expression.return_type(),
536 DeclarationKind::DomainLetting(domain) => domain.return_type(),
537 DeclarationKind::Given(domain) => domain.return_type(),
538 DeclarationKind::Quantified(inner) => inner.domain.return_type(),
539 DeclarationKind::RecordField(domain) => domain.return_type(),
540 }
541 }
542}
543
544impl Uniplate for DeclarationPtr {
545 fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
546 let decl = self.read();
547 let (tree, recons) = Biplate::<DeclarationPtr>::biplate(&decl as &Declaration);
548
549 let self2 = self.clone();
550 (
551 tree,
552 Box::new(move |x| {
553 let mut self3 = self2.clone();
554 let inner = recons(x);
555 *(&mut self3.write() as &mut Declaration) = inner;
556 self3
557 }),
558 )
559 }
560}
561
562impl<To> Biplate<To> for DeclarationPtr
563where
564 Declaration: Biplate<To>,
565 To: Uniplate,
566{
567 fn biplate(&self) -> (Tree<To>, Box<dyn Fn(Tree<To>) -> Self>) {
568 if TypeId::of::<To>() == TypeId::of::<Self>() {
569 unsafe {
570 let self_as_to = std::mem::transmute::<&Self, &To>(self).clone();
571 (
572 Tree::One(self_as_to),
573 Box::new(move |x| {
574 let Tree::One(x) = x else { panic!() };
575
576 let x_as_self = std::mem::transmute::<&To, &Self>(&x);
577 x_as_self.clone()
578 }),
579 )
580 }
581 } else {
582 // call biplate on the enclosed declaration
583 let decl = self.read();
584 let (tree, recons) = Biplate::<To>::biplate(&decl as &Declaration);
585
586 let self2 = self.clone();
587 (
588 tree,
589 Box::new(move |x| {
590 let mut self3 = self2.clone();
591 let inner = recons(x);
592 *(&mut self3.write() as &mut Declaration) = inner;
593 self3
594 }),
595 )
596 }
597 }
598}
599
600impl IdPtr for DeclarationPtr {
601 type Data = Declaration;
602
603 fn get_data(&self) -> Self::Data {
604 self.read().clone()
605 }
606
607 fn with_id_and_data(id: ObjId, data: Self::Data) -> Self {
608 Self {
609 inner: DeclarationPtrInner::new_with_id_unchecked(RwLock::new(data), id),
610 }
611 }
612}
613
614impl Ord for DeclarationPtr {
615 fn cmp(&self, other: &Self) -> std::cmp::Ordering {
616 self.inner.id.cmp(&other.inner.id)
617 }
618}
619
620impl PartialOrd for DeclarationPtr {
621 fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
622 Some(self.cmp(other))
623 }
624}
625
626impl PartialEq for DeclarationPtr {
627 fn eq(&self, other: &Self) -> bool {
628 self.inner.id == other.inner.id
629 }
630}
631
632impl Eq for DeclarationPtr {}
633
634impl std::hash::Hash for DeclarationPtr {
635 fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
636 // invariant: x == y -> hash(x) == hash(y)
637 self.inner.id.hash(state);
638 }
639}
640
641impl Display for DeclarationPtr {
642 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
643 let value: &Declaration = &self.read();
644 value.fmt(f)
645 }
646}
647
648#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]
649#[biplate(to=Expression)]
650#[biplate(to=DeclarationPtr)]
651#[biplate(to=Name)]
652/// The contents of a declaration
653pub(super) struct Declaration {
654 /// The name of the declared symbol.
655 name: Name,
656
657 /// The kind of the declaration.
658 kind: DeclarationKind,
659}
660
661impl Declaration {
662 /// Creates a new declaration.
663 fn new(name: Name, kind: DeclarationKind) -> Declaration {
664 Declaration { name, kind }
665 }
666}
667
668/// A specific kind of declaration.
669#[non_exhaustive]
670#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
671#[biplate(to=Expression)]
672#[biplate(to=DeclarationPtr)]
673#[biplate(to=Declaration)]
674pub enum DeclarationKind {
675 Find(DecisionVariable),
676 Given(DomainPtr),
677 Quantified(Quantified),
678 ValueLetting(Expression),
679 DomainLetting(DomainPtr),
680
681 /// A named field inside a record type.
682 /// e.g. A, B in record{A: int(0..1), B: int(0..2)}
683 RecordField(DomainPtr),
684}
685
686#[serde_as]
687#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
688pub struct Quantified {
689 domain: DomainPtr,
690
691 #[serde_as(as = "Option<PtrAsInner>")]
692 generator: Option<DeclarationPtr>,
693}
694
695impl Quantified {
696 pub fn domain(&self) -> &DomainPtr {
697 &self.domain
698 }
699
700 pub fn generator(&self) -> Option<&DeclarationPtr> {
701 self.generator.as_ref()
702 }
703}