Struct Declaration 

pub struct Declaration<D: ToSort, R: ToSort> {
    pub name: Identifier<'static>,
    pub domain: Vec<D>,
    pub range: R,
    pub span: Option<Span>,
}

Specification for declarations of functions (and constants, and sorts).

Declaration objects are passed to the Solver::declare() method to declare entities in a solver, by specifying all the attributes of such declarations. Then, the method returns a Declared object which is an opaque shared reference to a specific Declaration object which represents the actual entity the solver is keeping track of.

The Declaration<D, R> type is parametric in two ToSort types D and R used to represent the sort of the domain and of the range of the function, respectively. These can be e.g., Sort itself or the result of the sort! macro. See the documentation of ToSort for details.

The fields are public and the type can be constructed freely, but some constructors are also provided (function(), constant(), and sort()), for common cases.

Fields

name: Identifier<'static>

The name of the declared function.

domain: Vec<D>

The domain of the declared function, i.e. the sorts of its arguments.

range: R

The range of the declared function, i.e. its return type.

span: Option<Span>

The optional source span the declaration comes from.

Implementations

impl<D: ToSort, R: ToSort> Declaration<D, R>

pub fn function<'a>( name: impl Into<Identifier<'a>>, domain: impl IntoIterator<Item = D>, range: R, ) -> Declaration<D, R>

Declare a function (or a constant, or a sort).

This is the most general constructor. It is more convenient than directly constructing the Declaration struct because of implicit conversions of the arguments and the absence of the span argument which is put to None by default, since most of the time when using the API directly, declarations do not have a source span.

If the declaration do have a span it can be set using over().

In the following example we declare a function taking a integer argument and returning a real and we set it to a given span.

solver.declare(Declaration::function("f", [sort!(Int)], sort!(Real)))?;

impl<D: ToSort> Declaration<D, Sort>

pub fn predicate<'a>( name: impl Into<Identifier<'a>>, domain: impl IntoIterator<Item = D>, ) -> Declaration<D, Sort>

Declare a predicate (i.e. a function returning Core::Bool().

This is equivalent to Declaration::function(name, domain, theories::Core::Bool()).

impl<R: ToSort> Declaration<Sort, R>

pub fn constant<'a>( name: impl Into<Identifier<'a>>, sort: R, ) -> Declaration<Sort, R>

Declare a constant (i.e. a function with no arguments).

This is equivalent to Declaration::function(name, Vec::<Sort>::new(), sort).

impl Declaration<Sort, Sort>

pub fn sort<'a>(name: impl Into<Identifier<'a>>) -> Declaration<Sort, Sort>

Declare a sort (i.e. a constant of the special sort Sort::sort()).

This is equivalent to Declaration::constant(name, Sort::sort()).

pub fn boolean<'a>(name: impl Into<Identifier<'a>>) -> Declaration<Sort, Sort>

Declare a Boolean constant (i.e. a constant of sort Core::Bool().

This is equivalent to Declaration::constant(name, theories::Core::Bool()).

pub fn integer<'a>(name: impl Into<Identifier<'a>>) -> Declaration<Sort, Sort>

Declare an integer constant (i.e. a constant of sort Ints::Int().

This is equivalent to Declaration::constant(name, theories::Ints::Int()).

pub fn real<'a>(name: impl Into<Identifier<'a>>) -> Declaration<Sort, Sort>

Declare a real constant (i.e. a constant of sort Reals::Real().

This is equivalent to Declaration::constant(name, theories::Reals::Real()).

Trait Implementations

impl<D: Clone + ToSort, R: Clone + ToSort> Clone for Declaration<D, R>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<D: Debug + ToSort, R: Debug + ToSort> Debug for Declaration<D, R>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<D: Eq + ToSort, R: Eq + ToSort> Eq for Declaration<D, R>

impl<D: Hash + ToSort, R: Hash + ToSort> Hash for Declaration<D, R>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<D: ToSort, R: ToSort> Locatable for Declaration<D, R>

type Located = Declaration<D, R>

fn over(self, span: impl Into<Option<Span>>) -> Self

Turns self into an object of type Self::Located tracking the new span.

impl<D: ToSort, R: ToSort> Located for Declaration<D, R>

fn span(&self) -> Option<Span>

Gets the Span tracked by the type.

impl<D: PartialEq + ToSort, R: PartialEq + ToSort> PartialEq for Declaration<D, R>

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl<D: PartialEq + ToSort, R: PartialEq + ToSort> StructuralPartialEq for Declaration<D, R>