conjure_cp_core/ast/

declaration.rs

use super::categories::{Category, CategoryOf};
use super::name::Name;
use super::serde::{DefaultWithId, HasId, IdPtr, ObjId, PtrAsInner};
use super::{
    DecisionVariable, DomainPtr, Expression, GroundDomain, HasDomain, Moo, Reference, ReturnType,
    Typeable,
};
use crate::representation::{ReprRule, ReprStore};
use parking_lot::{
    MappedRwLockReadGuard, MappedRwLockWriteGuard, RwLock, RwLockReadGuard, RwLockWriteGuard,
};
use serde::{Deserialize, Serialize};
use serde_with::serde_as;
use std::any::TypeId;
use std::collections::BTreeSet;
use std::collections::VecDeque;
use std::fmt::{Debug, Display};
use std::hash::{DefaultHasher, Hash, Hasher};
use std::mem;
use std::ops::{Deref, DerefMut};
use std::sync::Arc;
use std::sync::atomic::{AtomicU32, AtomicU64, Ordering};
use uniplate::{Biplate, Tree, Uniplate};

/// Global counter of declarations.
/// Note that the counter is shared between all threads
/// Thus, when running multiple models in parallel, IDs may
/// be different with every run depending on scheduling order
static DECLARATION_PTR_ID_COUNTER: AtomicU32 = const { AtomicU32::new(0) };

/// Global generation of declaration contents.
///
/// Declaration pointers are shared across symbol tables, so an in-place update cannot cheaply
/// notify every table that contains the pointer. Symbol-table content caches compare against this
/// generation instead.
static DECLARATION_CONTENT_GENERATION: AtomicU64 = const { AtomicU64::new(1) };

/// Returns the generation shared by all mutable declaration contents.
pub(crate) fn declaration_content_generation() -> u64 {
    DECLARATION_CONTENT_GENERATION.load(Ordering::Acquire)
}

/// Records that a declaration's contents may have changed.
fn mark_declaration_content_changed() {
    DECLARATION_CONTENT_GENERATION.fetch_add(1, Ordering::AcqRel);
}

/// Mutable access to part of a declaration that records a semantic change when released.
pub struct DeclarationMutGuard<'a, T: ?Sized> {
    inner: Option<MappedRwLockWriteGuard<'a, T>>,
}

impl<'a, T: ?Sized> DeclarationMutGuard<'a, T> {
    /// Wraps a mapped write guard so dropping it records a content change.
    fn new(inner: MappedRwLockWriteGuard<'a, T>) -> Self {
        Self { inner: Some(inner) }
    }
}

impl<T: ?Sized> Deref for DeclarationMutGuard<'_, T> {
    type Target = T;

    fn deref(&self) -> &Self::Target {
        self.inner.as_deref().expect("declaration guard is live")
    }
}

impl<T: ?Sized> DerefMut for DeclarationMutGuard<'_, T> {
    fn deref_mut(&mut self) -> &mut Self::Target {
        self.inner
            .as_deref_mut()
            .expect("declaration guard is live")
    }
}

impl<T: ?Sized> Drop for DeclarationMutGuard<'_, T> {
    fn drop(&mut self) {
        drop(self.inner.take());
        mark_declaration_content_changed();
    }
}

#[doc(hidden)]
/// Resets the id counter of `DeclarationPtr` to 0.
///
/// This is probably always a bad idea.
pub fn reset_declaration_id_unchecked() {
    let _ = DECLARATION_PTR_ID_COUNTER.swap(0, Ordering::Relaxed);
}

/// A shared pointer to a [`Declaration`].
///
/// Two declaration pointers are equal if they point to the same underlying declaration.
///
/// # Id
///
///  The id of `DeclarationPtr` obeys the following invariants:
///
/// 1. Declaration pointers have the same id if they point to the same
///    underlying declaration.
///
/// 2. The id is immutable.
///
/// 3. Changing the declaration pointed to by the declaration pointer does not change the id. This
///    allows declarations to be updated by replacing them with a newer version of themselves.
///
/// `Ord`, `Hash`, and `Eq` use id for comparisons.
/// # Serde
///
/// Declaration pointers can be serialised using the following serializers:
///
/// + [`DeclarationPtrFull`](serde::DeclarationPtrFull)
/// + [`DeclarationPtrAsId`](serde::DeclarationPtrAsId)
///
/// See their documentation for more information.
#[derive(Clone, Debug)]
pub struct DeclarationPtr
where
    Self: Send + Sync,
{
    // the shared bits of the pointer
    inner: Arc<DeclarationPtrInner>,
}

// The bits of a declaration that are shared between all pointers.
#[derive(Debug)]
struct DeclarationPtrInner {
    // Identity hash/order key. Declaration content is mutable and is hashed separately by
    // `DeclarationPtr::content_hash`.
    // We don't want this to be mutable, as `HashMap` and `BTreeMap` rely on the hash or order of
    // keys to be unchanging.
    //
    // See:  https://rust-lang.github.io/rust-clippy/master/index.html#mutable_key_type
    id: ObjId,

    // The contents of the declaration itself should be mutable.
    value: RwLock<Declaration>,

    /// Representations initialised for this declaration.
    representations: RwLock<ReprStore>,

    /// The declaration from which this auxiliary declaration was created.
    source: RwLock<Option<DeclarationPtr>>,
}

impl DeclarationPtrInner {
    fn new(value: RwLock<Declaration>) -> Arc<DeclarationPtrInner> {
        Arc::new(DeclarationPtrInner {
            id: ObjId {
                type_name: ustr::ustr(DeclarationPtr::TYPE_NAME),
                object_id: DECLARATION_PTR_ID_COUNTER.fetch_add(1, Ordering::Relaxed),
            },
            value,
            representations: RwLock::new(ReprStore::new()),
            source: RwLock::new(None),
        })
    }

    // SAFETY: only use if you are really really sure you arn't going to break the id invariants of
    // DeclarationPtr and HasId!
    fn new_with_id_unchecked(value: RwLock<Declaration>, id: ObjId) -> Arc<DeclarationPtrInner> {
        Arc::new(DeclarationPtrInner {
            id,
            value,
            representations: RwLock::new(ReprStore::new()),
            source: RwLock::new(None),
        })
    }
}

#[allow(dead_code)]
impl DeclarationPtr {
    /******************************/
    /*        Constructors        */
    /******************************/

    /// Creates a `DeclarationPtr` for the given `Declaration`.
    fn from_declaration(declaration: Declaration) -> DeclarationPtr {
        DeclarationPtr {
            inner: DeclarationPtrInner::new(RwLock::new(declaration)),
        }
    }

    /// Gets the declaration from which this auxiliary declaration was created.
    pub fn source(&self) -> RwLockReadGuard<'_, Option<DeclarationPtr>> {
        self.inner.source.read()
    }

    /// Mutates the declaration from which this auxiliary declaration was created.
    pub fn source_mut(&mut self) -> RwLockWriteGuard<'_, Option<DeclarationPtr>> {
        self.inner.source.write()
    }

    /// Gets the representations initialised for this declaration.
    pub fn reprs(&self) -> RwLockReadGuard<'_, ReprStore> {
        self.inner.representations.read()
    }

    /// Mutates the representations initialised for this declaration.
    pub fn reprs_mut(&mut self) -> RwLockWriteGuard<'_, ReprStore> {
        self.inner.representations.write()
    }

    /// Gets a particular representation state, if it has been initialised.
    pub fn get_repr<T: ReprRule + ?Sized>(
        &self,
    ) -> Option<MappedRwLockReadGuard<'_, T::DeclLevel>> {
        RwLockReadGuard::try_map(self.inner.representations.read(), |reprs| reprs.get::<T>()).ok()
    }

    /// Creates a new declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
    ///
    /// // letting MyDomain be int(1..5)
    /// let declaration = DeclarationPtr::new(
    ///     Name::User("MyDomain".into()),
    ///     DeclarationKind::DomainLetting(Domain::int(vec![
    ///         Range::Bounded(1,5)])));
    /// ```
    pub fn new(name: Name, kind: DeclarationKind) -> DeclarationPtr {
        DeclarationPtr::from_declaration(Declaration::new(name, kind))
    }

    /// Creates a new find declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
    ///
    /// // find x: int(1..5)
    /// let declaration = DeclarationPtr::new_find(
    ///     Name::User("x".into()),
    ///     Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// ```
    pub fn new_find(name: Name, domain: DomainPtr) -> DeclarationPtr {
        let kind = DeclarationKind::Find(DecisionVariable::new(domain));
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new auxiliary find declaration.
    ///
    /// Auxiliary finds are introduced by rewriting (for example, turning a top-level `exists`
    /// into constraints), and can also be written in Essence as `findAux`.
    /// They are decision variables for solvers, but must not be branched on during search:
    /// different assignments to them must not produce distinct user-facing solutions.
    pub fn new_find_auxiliary(name: Name, domain: DomainPtr) -> DeclarationPtr {
        let kind = DeclarationKind::FindAuxiliary(DecisionVariable::new(domain));
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new given declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
    ///
    /// // given n: int(1..5)
    /// let declaration = DeclarationPtr::new_given(
    ///     Name::User("n".into()),
    ///     Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// ```
    pub fn new_given(name: Name, domain: DomainPtr) -> DeclarationPtr {
        let kind = DeclarationKind::Given(domain);
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new quantified declaration for local comprehension scopes.
    ///
    /// Used when creating the quantified variable in a generator.
    pub fn new_quantified(name: Name, domain: DomainPtr) -> DeclarationPtr {
        DeclarationPtr::new(
            name,
            DeclarationKind::Quantified(Quantified {
                domain,
                generator: None,
            }),
        )
    }

    /// Creates a quantified declaration backed by a generator declaration.
    ///
    /// This is used in comprehensions to refer to a quantified variable that is already defined using a generator.
    pub fn new_quantified_from_generator(decl: &DeclarationPtr) -> Option<DeclarationPtr> {
        let kind = DeclarationKind::Quantified(Quantified {
            domain: decl.domain()?,
            generator: Some(decl.clone()),
        });
        Some(DeclarationPtr::new(decl.name().clone(), kind))
    }

    pub fn new_quantified_expr(name: Name, expr: Expression) -> DeclarationPtr {
        let kind = DeclarationKind::QuantifiedExpr(expr);
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new value letting declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
    /// Literal,Atom,Moo};
    /// use conjure_cp_core::{matrix_expr,ast::Metadata};
    ///
    /// // letting n be 10 + 10
    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
    /// let declaration = DeclarationPtr::new_value_letting(
    ///     Name::User("n".into()),
    ///     expression);
    ///
    /// ```
    pub fn new_value_letting(name: Name, expression: Expression) -> DeclarationPtr {
        let kind = DeclarationKind::ValueLetting(expression, None);
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new value letting declaration with domain.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
    /// Literal,Atom,Moo,DomainPtr,Metadata};
    /// use conjure_cp_core::{matrix_expr};
    ///
    /// // letting n be 10 + 10
    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
    /// let domain = Domain::bool();
    /// let declaration = DeclarationPtr::new_value_letting_with_domain(
    ///     Name::User("n".into()),
    ///     expression,
    ///     domain,
    /// );
    /// ```
    pub fn new_value_letting_with_domain(
        name: Name,
        expression: Expression,
        domain: DomainPtr,
    ) -> DeclarationPtr {
        let kind = DeclarationKind::ValueLetting(expression, Some(domain));
        DeclarationPtr::new(name, kind)
    }

    /// Creates a new domain letting declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
    ///
    /// // letting MyDomain be int(1..5)
    /// let declaration = DeclarationPtr::new_domain_letting(
    ///     Name::User("MyDomain".into()),
    ///     Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// ```
    pub fn new_domain_letting(name: Name, domain: DomainPtr) -> DeclarationPtr {
        let kind = DeclarationKind::DomainLetting(domain);
        DeclarationPtr::new(name, kind)
    }

    /**********************************************/
    /*        Declaration accessor methods        */
    /**********************************************/

    /// Gets the domain of the declaration, if it has one.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};
    ///
    /// // find a: int(1..5)
    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)])))
    ///
    /// ```
    pub fn domain(&self) -> Option<DomainPtr> {
        // Expressions stored inside a declaration (as opposed to the constraint tree the rewrite
        // engine walks) can be mutated in place by substitution utilities that never touch
        // the constraint-tree metadata cache, so `domain_of`'s cache would go stale silently for
        // them. Use the uncached path here.
        match &self.kind() as &DeclarationKind {
            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => {
                Some(var.domain_of())
            }
            DeclarationKind::ValueLetting(e, domain) => {
                domain.clone().or_else(|| e.domain_of_uncached())
            }
            DeclarationKind::TemporaryValueLetting(e) => e.domain_of_uncached(),
            DeclarationKind::DomainLetting(domain) => Some(domain.clone()),
            DeclarationKind::Given(domain) => Some(domain.clone()),
            DeclarationKind::Quantified(inner) => Some(inner.domain.clone()),
            DeclarationKind::QuantifiedExpr(expr) => expr.domain_of_uncached()?.element_domain(),
        }
    }

    /// Returns true if this declaration is an auxiliary find.
    ///
    /// Auxiliary finds are solver variables that must not be included in the search/branching
    /// order (see [`DeclarationKind::FindAuxiliary`]).
    pub fn is_find_auxiliary(&self) -> bool {
        matches!(
            &self.kind() as &DeclarationKind,
            DeclarationKind::FindAuxiliary(_)
        )
    }

    /// Gets the domain of the declaration and fully resolve it
    pub fn resolved_domain(&self) -> Option<Moo<GroundDomain>> {
        self.domain()?.resolve().ok()
    }

    /// Gets the kind of the declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};
    ///
    /// // find a: int(1..5)
    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
    /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))
    /// ```
    pub fn kind(&self) -> MappedRwLockReadGuard<'_, DeclarationKind> {
        self.map(|x| &x.kind)
    }

    /// Gets the name of the declaration.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
    ///
    /// // find a: int(1..5)
    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))
    /// ```
    pub fn name(&self) -> MappedRwLockReadGuard<'_, Name> {
        self.map(|x| &x.name)
    }

    /// This declaration as a decision variable, if it is one.
    ///
    /// Both user [`DeclarationKind::Find`] and rewriter-introduced
    /// [`DeclarationKind::FindAuxiliary`] declarations are treated as decision variables.
    pub fn as_find(&self) -> Option<MappedRwLockReadGuard<'_, DecisionVariable>> {
        RwLockReadGuard::try_map(self.read(), |x| match &x.kind {
            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => Some(var),
            _ => None,
        })
        .ok()
    }

    /// This declaration as a mutable decision variable, if it is one.
    ///
    /// Both user [`DeclarationKind::Find`] and rewriter-introduced
    /// [`DeclarationKind::FindAuxiliary`] declarations are treated as decision variables.
    pub fn as_find_mut(&mut self) -> Option<DeclarationMutGuard<'_, DecisionVariable>> {
        RwLockWriteGuard::try_map(self.write(), |x| match &mut x.kind {
            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => Some(var),
            _ => None,
        })
        .ok()
        .map(DeclarationMutGuard::new)
    }

    /// This declaration as a domain letting, if it is one.
    pub fn as_domain_letting(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
        RwLockReadGuard::try_map(self.read(), |x| {
            if let DeclarationKind::DomainLetting(domain) = &x.kind {
                Some(domain)
            } else {
                None
            }
        })
        .ok()
    }

    /// This declaration as a mutable domain letting, if it is one.
    pub fn as_domain_letting_mut(&mut self) -> Option<DeclarationMutGuard<'_, DomainPtr>> {
        RwLockWriteGuard::try_map(self.write(), |x| {
            if let DeclarationKind::DomainLetting(domain) = &mut x.kind {
                Some(domain)
            } else {
                None
            }
        })
        .ok()
        .map(DeclarationMutGuard::new)
    }

    /// This declaration as a value letting, if it is one.
    pub fn as_value_letting(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
        RwLockReadGuard::try_map(self.read(), |x| {
            if let DeclarationKind::ValueLetting(expression, _)
            | DeclarationKind::TemporaryValueLetting(expression) = &x.kind
            {
                Some(expression)
            } else {
                None
            }
        })
        .ok()
    }

    /// This declaration as a mutable value letting, if it is one.
    pub fn as_value_letting_mut(&mut self) -> Option<DeclarationMutGuard<'_, Expression>> {
        RwLockWriteGuard::try_map(self.write(), |x| {
            if let DeclarationKind::ValueLetting(expression, _)
            | DeclarationKind::TemporaryValueLetting(expression) = &mut x.kind
            {
                Some(expression)
            } else {
                None
            }
        })
        .ok()
        .map(DeclarationMutGuard::new)
    }

    /// This declaration as a given statement, if it is one.
    pub fn as_given(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
        RwLockReadGuard::try_map(self.read(), |x| {
            if let DeclarationKind::Given(domain) = &x.kind {
                Some(domain)
            } else {
                None
            }
        })
        .ok()
    }

    /// This declaration as a mutable given statement, if it is one.
    pub fn as_given_mut(&mut self) -> Option<DeclarationMutGuard<'_, DomainPtr>> {
        RwLockWriteGuard::try_map(self.write(), |x| {
            if let DeclarationKind::Given(domain) = &mut x.kind {
                Some(domain)
            } else {
                None
            }
        })
        .ok()
        .map(DeclarationMutGuard::new)
    }

    /// This declaration as a quantified expression, if it is one.
    pub fn as_quantified_expr(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
        RwLockReadGuard::try_map(self.read(), |x| {
            if let DeclarationKind::QuantifiedExpr(expr) = &x.kind {
                Some(expr)
            } else {
                None
            }
        })
        .ok()
    }

    /// This declaration as a mutable quantified expression, if it is one.
    pub fn as_quantified_expr_mut(&mut self) -> Option<DeclarationMutGuard<'_, Expression>> {
        RwLockWriteGuard::try_map(self.write(), |x| {
            if let DeclarationKind::QuantifiedExpr(expr) = &mut x.kind {
                Some(expr)
            } else {
                None
            }
        })
        .ok()
        .map(DeclarationMutGuard::new)
    }

    /// Changes the name in this declaration, returning the old one.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};
    ///
    /// // find a: int(1..5)
    /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// let old_name = declaration.replace_name(Name::User("b".into()));
    /// assert_eq!(old_name,Name::User("a".into()));
    /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));
    /// ```
    pub fn replace_name(&mut self, name: Name) -> Name {
        let mut current_name = self.map_mut(|decl| &mut decl.name);
        std::mem::replace(&mut *current_name, name)
    }

    /// Replaces the underlying declaration kind and returns the previous kind.
    /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.
    pub fn replace_kind(&mut self, kind: DeclarationKind) -> DeclarationKind {
        let mut current_kind = self.map_mut(|decl| &mut decl.kind);
        std::mem::replace(&mut *current_kind, kind)
    }

    /*****************************************/
    /*        Pointer utility methods        */
    /*****************************************/

    // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for
    // convenience.

    /// Read the underlying [Declaration].
    ///
    /// Will block the current thread until no other thread has a write lock.
    /// Attempting to get a read lock if the current thread already has one
    /// **will** cause it to deadlock.
    /// The lock is released when the returned guard goes out of scope.
    fn read(&self) -> RwLockReadGuard<'_, Declaration> {
        self.inner.value.read()
    }

    /// Write the underlying [Declaration].
    ///
    /// Will block the current thread until no other thread has a read or write lock.
    /// The lock is released when the returned guard goes out of scope.
    fn write(&mut self) -> RwLockWriteGuard<'_, Declaration> {
        self.inner.value.write()
    }

    /// Creates a new declaration pointer with the same contents as `self` that is not shared with
    /// anyone else.
    ///
    /// As the resulting pointer is unshared, it will have a new id.
    ///
    /// # Examples
    ///
    /// ```
    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
    ///
    /// // find a: int(1..5)
    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
    ///
    /// let mut declaration2 = declaration.clone();
    ///
    /// declaration2.replace_name(Name::User("b".into()));
    ///
    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
    ///
    /// declaration2 = declaration2.detach();
    ///
    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
    ///
    /// declaration2.replace_name(Name::User("c".into()));
    ///
    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
    /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));
    /// ```
    pub fn detach(self) -> DeclarationPtr {
        // despite having the same contents, the new declaration pointer is unshared, so it should
        // get a new id.
        let value = self.inner.value.read().clone();
        let representations = self.inner.representations.read().clone();
        let source = self.inner.source.read().clone();
        let detached = DeclarationPtr {
            inner: DeclarationPtrInner::new(RwLock::new(value)),
        };
        *detached.inner.representations.write() = representations;
        *detached.inner.source.write() = source;
        detached
    }

    /// Applies `f` to the declaration, returning the result as a reference.
    fn map<U>(&self, f: impl FnOnce(&Declaration) -> &U) -> MappedRwLockReadGuard<'_, U> {
        RwLockReadGuard::map(self.read(), f)
    }

    /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.
    fn map_mut<U>(
        &mut self,
        f: impl FnOnce(&mut Declaration) -> &mut U,
    ) -> DeclarationMutGuard<'_, U> {
        DeclarationMutGuard::new(RwLockWriteGuard::map(self.write(), f))
    }

    /// Replaces the declaration with a new one, returning the old value, without deinitialising
    /// either one.
    pub fn replace(&mut self, declaration: Declaration) -> Declaration {
        let mut guard = self.write();
        let ans = mem::replace(&mut *guard, declaration);
        drop(guard);
        mark_declaration_content_changed();
        ans
    }

    /// Hashes the declaration contents rather than the stable declaration pointer id.
    ///
    /// Pointer hashing intentionally remains id-based for map/set invariants. This helper is for
    /// rewrite caches that need to be invalidated when the declaration value behind a reference
    /// changes.
    pub(crate) fn content_hash(&self) -> u64 {
        let mut hasher = DefaultHasher::new();
        let mut seen = BTreeSet::new();
        self.hash_content(&mut hasher, &mut seen);
        hasher.finish()
    }

    /// Compares current declaration contents without considering pointer identity.
    pub(crate) fn content_eq(&self, other: &Self) -> bool {
        if self.id() == other.id() {
            return true;
        }
        let this = self.read().clone();
        let other = other.read().clone();
        this == other
    }

    /// Hashes this declaration's value into `state`, guarding against declaration-reference cycles.
    fn hash_content<H: Hasher>(&self, state: &mut H, seen: &mut BTreeSet<ObjId>) {
        let id = self.id();
        if !seen.insert(id.clone()) {
            "recursive-declaration".hash(state);
            return;
        }

        let declaration = self.read();
        declaration.name.hash(state);
        declaration.kind.hash_content(state, seen);
        seen.remove(&id);
    }
}

impl CategoryOf for DeclarationPtr {
    fn category_of(&self) -> Category {
        match &self.kind() as &DeclarationKind {
            DeclarationKind::Find(decision_variable)
            | DeclarationKind::FindAuxiliary(decision_variable) => decision_variable.category_of(),
            DeclarationKind::ValueLetting(expression, _)
            | DeclarationKind::TemporaryValueLetting(expression) => expression.category_of(),
            DeclarationKind::DomainLetting(_) => Category::Constant,
            DeclarationKind::Given(_) => Category::Parameter,
            DeclarationKind::Quantified(..) => Category::Quantified,
            DeclarationKind::QuantifiedExpr(..) => Category::Quantified,
        }
    }
}
impl HasId for DeclarationPtr {
    const TYPE_NAME: &'static str = "DeclarationPtrInner";
    fn id(&self) -> ObjId {
        self.inner.id.clone()
    }
}

impl DefaultWithId for DeclarationPtr {
    fn default_with_id(id: ObjId) -> Self {
        DeclarationPtr {
            inner: DeclarationPtrInner::new_with_id_unchecked(
                RwLock::new(Declaration {
                    name: Name::User("_UNKNOWN".into()),
                    kind: DeclarationKind::ValueLetting(false.into(), None),
                }),
                id,
            ),
        }
    }
}

impl Typeable for DeclarationPtr {
    fn return_type(&self) -> ReturnType {
        match &self.kind() as &DeclarationKind {
            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => var.return_type(),
            DeclarationKind::ValueLetting(expression, _)
            | DeclarationKind::TemporaryValueLetting(expression) => expression.return_type(),
            DeclarationKind::DomainLetting(domain) => domain.return_type(),
            DeclarationKind::Given(domain) => domain.return_type(),
            DeclarationKind::Quantified(inner) => inner.domain.return_type(),
            DeclarationKind::QuantifiedExpr(expr) => expr.return_type(),
        }
    }
}

impl Uniplate for DeclarationPtr {
    fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
        let decl = self.read();
        let (tree, recons) = Biplate::<DeclarationPtr>::biplate(&decl as &Declaration);

        let self2 = self.clone();
        (
            tree,
            Box::new(move |x| {
                let mut self3 = self2.clone();
                let inner = recons(x);
                let _ = self3.replace(inner);
                self3
            }),
        )
    }
}

impl<To> Biplate<To> for DeclarationPtr
where
    Declaration: Biplate<To>,
    To: Uniplate,
{
    fn biplate(&self) -> (Tree<To>, Box<dyn Fn(Tree<To>) -> Self>) {
        if TypeId::of::<To>() == TypeId::of::<Self>() {
            unsafe {
                let self_as_to = std::mem::transmute::<&Self, &To>(self).clone();
                (
                    Tree::One(self_as_to),
                    Box::new(move |x| {
                        let Tree::One(x) = x else { panic!() };

                        let x_as_self = std::mem::transmute::<&To, &Self>(&x);
                        x_as_self.clone()
                    }),
                )
            }
        } else {
            // call biplate on the enclosed declaration
            let decl = self.read();
            let (tree, recons) = Biplate::<To>::biplate(&decl as &Declaration);

            let self2 = self.clone();
            (
                tree,
                Box::new(move |x| {
                    let mut self3 = self2.clone();
                    let inner = recons(x);
                    let _ = self3.replace(inner);
                    self3
                }),
            )
        }
    }
}

type ReferenceTree = Tree<Reference>;
type ReferenceReconstructor<T> = Box<dyn Fn(ReferenceTree) -> T>;

impl Biplate<Reference> for DeclarationPtr {
    fn biplate(&self) -> (ReferenceTree, ReferenceReconstructor<Self>) {
        let (tree, recons_kind) = biplate_declaration_kind_references(self.kind().clone());

        let self2 = self.clone();
        (
            tree,
            Box::new(move |x| {
                let mut self3 = self2.clone();
                let _ = self3.replace_kind(recons_kind(x));
                self3
            }),
        )
    }
}

fn biplate_domain_ptr_references(
    domain: DomainPtr,
) -> (ReferenceTree, ReferenceReconstructor<DomainPtr>) {
    let domain_inner = domain.as_ref().clone();
    let (tree, recons_domain) = Biplate::<Reference>::biplate(&domain_inner);
    (tree, Box::new(move |x| Moo::new(recons_domain(x))))
}

fn biplate_declaration_kind_references(
    kind: DeclarationKind,
) -> (ReferenceTree, ReferenceReconstructor<DeclarationKind>) {
    match kind {
        DeclarationKind::Find(var) => {
            let (tree, recons_domain) = biplate_domain_ptr_references(var.domain.clone());
            (
                tree,
                Box::new(move |x| {
                    let mut var2 = var.clone();
                    var2.domain = recons_domain(x);
                    DeclarationKind::Find(var2)
                }),
            )
        }
        DeclarationKind::FindAuxiliary(var) => {
            let (tree, recons_domain) = biplate_domain_ptr_references(var.domain.clone());
            (
                tree,
                Box::new(move |x| {
                    let mut var2 = var.clone();
                    var2.domain = recons_domain(x);
                    DeclarationKind::FindAuxiliary(var2)
                }),
            )
        }
        DeclarationKind::Given(domain) => {
            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
            (
                tree,
                Box::new(move |x| DeclarationKind::Given(recons_domain(x))),
            )
        }
        DeclarationKind::DomainLetting(domain) => {
            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
            (
                tree,
                Box::new(move |x| DeclarationKind::DomainLetting(recons_domain(x))),
            )
        }
        DeclarationKind::ValueLetting(expression, domain) => {
            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
            (
                tree,
                Box::new(move |x| DeclarationKind::ValueLetting(recons_expr(x), domain.clone())),
            )
        }
        DeclarationKind::TemporaryValueLetting(expression) => {
            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
            (
                tree,
                Box::new(move |x| DeclarationKind::TemporaryValueLetting(recons_expr(x))),
            )
        }
        DeclarationKind::Quantified(quantified) => {
            let (domain_tree, recons_domain) =
                biplate_domain_ptr_references(quantified.domain.clone());

            let (generator_tree, recons_generator) = if let Some(generator) = quantified.generator()
            {
                let generator = generator.clone();
                let (tree, recons_declaration) = Biplate::<Reference>::biplate(&generator);
                (
                    tree,
                    Box::new(move |x| Some(recons_declaration(x)))
                        as ReferenceReconstructor<Option<DeclarationPtr>>,
                )
            } else {
                (
                    Tree::Zero,
                    Box::new(|_| None) as ReferenceReconstructor<Option<DeclarationPtr>>,
                )
            };

            (
                Tree::Many(VecDeque::from([domain_tree, generator_tree])),
                Box::new(move |x| {
                    let Tree::Many(mut children) = x else {
                        panic!("unexpected biplate tree shape for quantified declaration")
                    };

                    let domain = children.pop_front().unwrap_or(Tree::Zero);
                    let generator = children.pop_front().unwrap_or(Tree::Zero);

                    let mut quantified2 = quantified.clone();
                    quantified2.domain = recons_domain(domain);
                    quantified2.generator = recons_generator(generator);
                    DeclarationKind::Quantified(quantified2)
                }),
            )
        }
        DeclarationKind::QuantifiedExpr(expr) => {
            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expr);
            (
                tree,
                Box::new(move |x| DeclarationKind::QuantifiedExpr(recons_expr(x))),
            )
        }
    }
}

impl IdPtr for DeclarationPtr {
    type Data = Declaration;

    fn get_data(&self) -> Self::Data {
        self.read().clone()
    }

    fn with_id_and_data(id: ObjId, data: Self::Data) -> Self {
        Self {
            inner: DeclarationPtrInner::new_with_id_unchecked(RwLock::new(data), id),
        }
    }
}

impl Ord for DeclarationPtr {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        self.inner.id.cmp(&other.inner.id)
    }
}

impl PartialOrd for DeclarationPtr {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}

impl PartialEq for DeclarationPtr {
    fn eq(&self, other: &Self) -> bool {
        self.inner.id == other.inner.id
    }
}

impl Eq for DeclarationPtr {}

impl std::hash::Hash for DeclarationPtr {
    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
        // invariant: x == y -> hash(x) == hash(y)
        self.inner.id.hash(state);
    }
}

impl Display for DeclarationPtr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let value: &Declaration = &self.read();
        value.fmt(f)
    }
}

#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]
#[biplate(to=Expression)]
#[biplate(to=DeclarationPtr)]
#[biplate(to=Name)]
/// The contents of a declaration
pub struct Declaration {
    /// The name of the declared symbol.
    name: Name,

    /// The kind of the declaration.
    kind: DeclarationKind,
}

impl Declaration {
    /// Creates a new declaration.
    pub fn new(name: Name, kind: DeclarationKind) -> Declaration {
        Declaration { name, kind }
    }
}

/// A specific kind of declaration.
#[non_exhaustive]
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
#[biplate(to=Expression)]
#[biplate(to=DeclarationPtr)]
#[biplate(to=Declaration)]
pub enum DeclarationKind {
    Find(DecisionVariable),

    /// A rewriter-introduced or `findAux`-declared decision variable that must not be branched on
    /// during search.
    ///
    /// Used for auxiliaries such as those created when rewriting `exists` into constraints.
    FindAuxiliary(DecisionVariable),

    Given(DomainPtr),
    Quantified(Quantified),
    QuantifiedExpr(Expression),

    /// Carries an optional domain so instantiated `given`s can retain their declared domain.
    ValueLetting(Expression, Option<DomainPtr>),
    DomainLetting(DomainPtr),

    /// A short-lived value binding used internally during rewrites (e.g. comprehension unrolling).
    ///
    /// Unlike `ValueLetting`, this is not intended to represent a user-visible top-level `letting`.
    TemporaryValueLetting(Expression),
}

impl DeclarationKind {
    /// Hashes declaration-kind contents without using declaration pointer identity.
    fn hash_content<H: Hasher>(&self, state: &mut H, seen: &mut BTreeSet<ObjId>) {
        mem::discriminant(self).hash(state);
        match self {
            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => {
                var.domain.hash(state);
                for representation in &var.representations {
                    for repr in representation {
                        repr.repr_name().hash(state);
                        if let Ok(declarations) = repr.declaration_down() {
                            for declaration in declarations {
                                declaration.hash_content(state, seen);
                            }
                        } else {
                            "unavailable-representation-declarations".hash(state);
                        }
                    }
                }
            }
            DeclarationKind::Given(domain) | DeclarationKind::DomainLetting(domain) => {
                domain.hash(state);
            }
            DeclarationKind::Quantified(quantified) => {
                quantified.domain.hash(state);
                if let Some(generator) = quantified.generator() {
                    generator.hash_content(state, seen);
                }
            }
            DeclarationKind::QuantifiedExpr(expr)
            | DeclarationKind::TemporaryValueLetting(expr) => {
                expr.cached_content_hash().hash(state);
                expr.to_string().hash(state);
            }
            DeclarationKind::ValueLetting(expr, domain) => {
                expr.cached_content_hash().hash(state);
                expr.to_string().hash(state);
                domain.hash(state);
            }
        }
    }
}

#[serde_as]
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
pub struct Quantified {
    domain: DomainPtr,

    #[serde_as(as = "Option<PtrAsInner>")]
    generator: Option<DeclarationPtr>,
}

impl Quantified {
    pub fn domain(&self) -> &DomainPtr {
        &self.domain
    }

    pub fn generator(&self) -> Option<&DeclarationPtr> {
        self.generator.as_ref()
    }
}