Struct Variable 

pub struct Variable<S: ToSort = Sort>(/* private fields */);

A free variable.

Variable represents a free variable in a term that can be bound by let expressions, quantified by forall or exists quantifiers, or bound to function parameters.

Variable objects can be created using the Variable::new() constructor or with the var! or vars! macros.

For example:

let config = Config::default();
let mut solver = Solver::new(&config)?;

solver.define(Definition::function("f", [var!(x Int)], sort!(Int), term!(* x 2)));

solver.require(term!(not (= (f 21) 42)))?;

assert_eq!(solver.check()?, Answer::No);

The Variable type is parametric in a ToSort type S used to represent the sort of the variable, such as Sort itself or the result of the sort! macro. See the documentation of ToSort for details.

Comparison of Variable objects is nominal, that is, equality and hashing operate on the identity of the objects, not on their values. In other words, two Variable objects with exactly the same fields (and in particular the same name) created by two different calls to Variable::new() will compare different and have a possibly different hash. Moreover, cloning a Variable object is a cheap operation and produces a second object which compares equal to the first. Under the hood, this is the behavior of Nominal<Arc<T>> for some inner type T, so we also refer to the Nominal type for details.

Implementations

impl<S: ToSort> Variable<S>

pub fn new<'a>(name: impl Into<Identifier<'a>>, sort: S) -> Variable<S>

Create a new Variable.

pub fn name(&self) -> &Identifier<'static>

Get the variable’s name.

pub fn sort(&self) -> &S

Get the variable’s sort.

Trait Implementations

impl<S: Clone + ToSort> Clone for Variable<S>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<S: Debug + ToSort> Debug for Variable<S>

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

Formats the value using the given formatter.

impl<S: Eq + ToSort> Eq for Variable<S>

impl From<Variable> for Function

fn from(value: Variable) -> Self

Converts to this type from the input type.

impl From<Variable> for SortedVar

fn from(var: Variable) -> Self

Converts to this type from the input type.

impl From<Variable> for SortHead

fn from(val: Variable) -> Self

Converts to this type from the input type.

impl From<Variable> for FunctionRef

fn from(val: Variable) -> Self

Converts to this type from the input type.

impl From<Variable> for Atom

fn from(val: Variable) -> Self

Converts to this type from the input type.

impl<S: Hash + ToSort> Hash for Variable<S>

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<S: Clone + ToSort> Locatable for Variable<S>

type Located = Variable<S>

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

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

impl<S: ToSort> Located for Variable<S>

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

Gets the Span tracked by the type.

impl<S: PartialEq + ToSort> PartialEq for Variable<S>

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

Equality operator ==.

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

Inequality operator !=.

impl Resolve for Variable

fn resolve(&self, env: &Env, pool: &dyn TermPool, _role: Role) -> Result<Self>

Perform name resolution on self.

impl<S: PartialEq + ToSort> StructuralPartialEq for Variable<S>

impl ToTerm for Variable

fn into_term_in(self, pool: &dyn TermPool) -> Term

Convert the object into a Term by uniquing in the given TermPool.

fn to_term_in(&self, pool: &dyn TermPool) -> Term

Convert the object (by reference) into a Term by uniquing in the given TermPool.