Struct Const

pub struct Const<'st, T>(/* private fields */);

This struct wraps specific instances of other terms to indicate that they are constant. Constants are named terms whose value can be extracted from a model using Model::eval.

To construct a Const<'st, T> call T::new_const where T implements Sort.

Implementations

impl<T> Const<'_, T>

pub fn name(&self) -> &str

The name of the constant

Trait Implementations

impl<'st> Add<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the + operator.

fn add(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the + operation.

impl<'st> Add<Const<'st, Real<'st>>> for f64

type Output = Real<'st>

The resulting type after applying the + operator.

fn add(self, rhs: Const<'st, Real<'st>>) -> Self::Output

Performs the + operation.

impl<'st, const M: usize, R> Add<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the + operator.

fn add(self, rhs: R) -> Self::Output

Performs the + operation.

impl<'st, R> Add<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the + operator.

fn add(self, rhs: R) -> Self::Output

Performs the + operation.

impl<'st, R> Add<R> for Const<'st, Real<'st>>

where R: IntoWithStorage<'st, Real<'st>>,

type Output = Real<'st>

The resulting type after applying the + operator.

fn add(self, rhs: R) -> Self::Output

Performs the + operation.

impl<'st> BitAnd<Const<'st, Bool<'st>>> for bool

type Output = Bool<'st>

The resulting type after applying the & operator.

fn bitand(self, rhs: Const<'st, Bool<'st>>) -> Self::Output

Performs the & operation.

impl<'st, const M: usize, R> BitAnd<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the & operator.

fn bitand(self, rhs: R) -> Self::Output

Performs the & operation.

impl<'st, R> BitAnd<R> for Const<'st, Bool<'st>>

where R: IntoWithStorage<'st, Bool<'st>>,

type Output = Bool<'st>

The resulting type after applying the & operator.

fn bitand(self, rhs: R) -> Self::Output

Performs the & operation.

impl<'st> BitOr<Const<'st, Bool<'st>>> for bool

type Output = Bool<'st>

The resulting type after applying the | operator.

fn bitor(self, rhs: Const<'st, Bool<'st>>) -> Self::Output

Performs the | operation.

impl<'st, const M: usize, R> BitOr<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the | operator.

fn bitor(self, rhs: R) -> Self::Output

Performs the | operation.

impl<'st, R> BitOr<R> for Const<'st, Bool<'st>>

where R: IntoWithStorage<'st, Bool<'st>>,

type Output = Bool<'st>

The resulting type after applying the | operator.

fn bitor(self, rhs: R) -> Self::Output

Performs the | operation.

impl<'st> BitXor<Const<'st, Bool<'st>>> for bool

type Output = Bool<'st>

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: Const<'st, Bool<'st>>) -> Self::Output

Performs the ^ operation.

impl<'st, const M: usize, R> BitXor<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: R) -> Self::Output

Performs the ^ operation.

impl<'st, R> BitXor<R> for Const<'st, Bool<'st>>

where R: IntoWithStorage<'st, Bool<'st>>,

type Output = Bool<'st>

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: R) -> Self::Output

Performs the ^ operation.

impl<'st, T: Clone> Clone for Const<'st, T>

fn clone(&self) -> Const<'st, T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'st, T: Debug> Debug for Const<'st, T>

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

Formats the value using the given formatter.

impl<T> Deref for Const<'_, T>

type Target = T

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl<'st> Div<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the / operator.

fn div(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the / operation.

impl<'st> Div<Const<'st, Real<'st>>> for f64

type Output = Real<'st>

The resulting type after applying the / operator.

fn div(self, rhs: Const<'st, Real<'st>>) -> Self::Output

Performs the / operation.

impl<'st, const M: usize, R> Div<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the / operator.

fn div(self, rhs: R) -> Self::Output

Performs the / operation.

impl<'st, R> Div<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the / operator.

fn div(self, rhs: R) -> Self::Output

Performs the / operation.

impl<'st, R> Div<R> for Const<'st, Real<'st>>

where R: IntoWithStorage<'st, Real<'st>>,

type Output = Real<'st>

The resulting type after applying the / operator.

fn div(self, rhs: R) -> Self::Output

Performs the / operation.

impl<'st, const M: usize> From<Const<'st, BitVec<'st, M>>> for BitVec<'st, M>

fn from(c: Const<'st, BitVec<'st, M>>) -> Self

Converts to this type from the input type.

impl<'st> From<Const<'st, Bool<'st>>> for Bool<'st>

fn from(c: Const<'st, Bool<'st>>) -> Self

Converts to this type from the input type.

impl<'st> From<Const<'st, Int<'st>>> for Int<'st>

fn from(c: Const<'st, Int<'st>>) -> Self

Converts to this type from the input type.

impl<'st> From<Const<'st, Real<'st>>> for Real<'st>

fn from(c: Const<'st, Real<'st>>) -> Self

Converts to this type from the input type.

impl<'st, T> From<Const<'st, T>> for Dynamic<'st>

where T: Into<Dynamic<'st>>,

fn from(c: Const<'st, T>) -> Self

Converts to this type from the input type.

impl<'st, T: Into<STerm<'st>>> From<Const<'st, T>> for STerm<'st>

fn from(c: Const<'st, T>) -> Self

Converts to this type from the input type.

impl<'st, X: Sorted<'st>, Y: Sorted<'st>> IntoWithStorage<'st, Array<'st, X, Y>> for Const<'st, Array<'st, X, Y>>

fn into_with_storage(self, _st: &'st Storage) -> Array<'st, X, Y>

Construct a STerm with the presence of Storage

impl<'st> IntoWithStorage<'st, Bool<'st>> for Const<'st, Bool<'st>>

fn into_with_storage(self, _st: &'st Storage) -> Bool<'st>

Construct a STerm with the presence of Storage

impl<'st> IntoWithStorage<'st, Int<'st>> for Const<'st, Int<'st>>

fn into_with_storage(self, _st: &'st Storage) -> Int<'st>

Construct a STerm with the presence of Storage

impl<'st> IntoWithStorage<'st, Real<'st>> for Const<'st, Real<'st>>

fn into_with_storage(self, _st: &'st Storage) -> Real<'st>

Construct a STerm with the presence of Storage

impl<'st> Mul<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the * operator.

fn mul(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the * operation.

impl<'st> Mul<Const<'st, Real<'st>>> for f64

type Output = Real<'st>

The resulting type after applying the * operator.

fn mul(self, rhs: Const<'st, Real<'st>>) -> Self::Output

Performs the * operation.

impl<'st, const M: usize, R> Mul<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the * operator.

fn mul(self, rhs: R) -> Self::Output

Performs the * operation.

impl<'st, R> Mul<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the * operator.

fn mul(self, rhs: R) -> Self::Output

Performs the * operation.

impl<'st, R> Mul<R> for Const<'st, Real<'st>>

where R: IntoWithStorage<'st, Real<'st>>,

type Output = Real<'st>

The resulting type after applying the * operator.

fn mul(self, rhs: R) -> Self::Output

Performs the * operation.

impl<'st, A> QuantifierVars<'st> for Const<'st, A>

where A: StaticSorted<'st>,

fn into_vars(self, _st: &'st Storage) -> &'st [SortedVar<'st>]

The concrete sequence of variable declaration which should be quantified over.

impl<'st> Rem<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the % operator.

fn rem(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the % operation.

impl<'st, const M: usize, R> Rem<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the % operator.

fn rem(self, rhs: R) -> Self::Output

Performs the % operation.

impl<'st, R> Rem<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the % operator.

fn rem(self, rhs: R) -> Self::Output

Performs the % operation.

impl<'st> Shl<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the << operator.

fn shl(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the << operation.

impl<'st, const M: usize, R> Shl<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the << operator.

fn shl(self, rhs: R) -> Self::Output

Performs the << operation.

impl<'st, R> Shl<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the << operator.

fn shl(self, rhs: R) -> Self::Output

Performs the << operation.

impl<'st> Shr<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the >> operator.

fn shr(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the >> operation.

impl<'st, const M: usize, R> Shr<R> for Const<'st, BitVec<'st, M>>

where R: Into<BitVec<'st, M>>,

type Output = BitVec<'st, M>

The resulting type after applying the >> operator.

fn shr(self, rhs: R) -> Self::Output

Performs the >> operation.

impl<'st, R> Shr<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the >> operator.

fn shr(self, rhs: R) -> Self::Output

Performs the >> operation.

impl<'st, T: Sorted<'st>> Sorted<'st> for Const<'st, T>

type Inner = T

The inner type of the term. This is used for Const<'st, T> where the inner type is T.

fn sort(&self) -> Sort<'st>

The sort of the term.

fn is_sort(sort: Sort<'st>) -> bool

Check if a sort is of this type.

fn st(&self) -> &'st Storage

The storage associated with any term of this sort.

fn sterm(self) -> STerm<'st>

Constructy the smtlib AST representation of the term with associated storage.

fn term(self) -> &'st Term<'st>

Construct the smtlib AST representation of term.

fn into_dynamic(self) -> Dynamic<'st>

Casts the term into a dynamic term which looses static types and stores the sort dynamically.

fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>

Construct the term representing (= self other)

fn _neq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>

Construct the term representing (distinct self other)

fn labeled(self) -> (Label<Self>, Self::Inner)

where Self::Inner: From<STerm<'st>>,

Wraps the term in a a label, which can be used to extract information from models at a later point.

impl<'st> Sub<Const<'st, Int<'st>>> for i64

type Output = Int<'st>

The resulting type after applying the - operator.

fn sub(self, rhs: Const<'st, Int<'st>>) -> Self::Output

Performs the - operation.

impl<'st> Sub<Const<'st, Real<'st>>> for f64

type Output = Real<'st>

The resulting type after applying the - operator.

fn sub(self, rhs: Const<'st, Real<'st>>) -> Self::Output

Performs the - operation.

impl<'st, R> Sub<R> for Const<'st, Int<'st>>

where R: IntoWithStorage<'st, Int<'st>>,

type Output = Int<'st>

The resulting type after applying the - operator.

fn sub(self, rhs: R) -> Self::Output

Performs the - operation.

impl<'st, R> Sub<R> for Const<'st, Real<'st>>

where R: IntoWithStorage<'st, Real<'st>>,

type Output = Real<'st>

The resulting type after applying the - operator.

fn sub(self, rhs: R) -> Self::Output

Performs the - operation.

impl<'st, T: Copy> Copy for Const<'st, T>