Struct Model 

pub struct Model {
    pub theory: String,
    pub sort_interp: FxHashMap<String, Vec<ModelValue>>,
    pub op_interp: FxHashMap<String, Arc<dyn Fn(&[ModelValue]) -> Result<ModelValue, GatError> + Send + Sync>>,
}

A model (interpretation) of a theory in Set.

Maps each sort to a carrier set of values and each operation to a function on those values. Models are the semantic counterpart of theories: a theory describes structure abstractly, while a model provides a concrete instantiation.

Model does not derive Serialize/Deserialize because op_interp contains function pointers (Arc<dyn Fn(...)>) which cannot be serialized.

Fields

theory: String

The name of the theory this model interprets.

sort_interp: FxHashMap<String, Vec<ModelValue>>

Sort interpretations: each sort name maps to its carrier set.

op_interp: FxHashMap<String, Arc<dyn Fn(&[ModelValue]) -> Result<ModelValue, GatError> + Send + Sync>>

Operation interpretations: each operation name maps to a function.

Implementations

impl Model

pub fn new(theory: impl Into<String>) -> Self

Create a new model for a given theory.

pub fn add_sort(&mut self, name: impl Into<String>, values: Vec<ModelValue>)

Add a sort interpretation (carrier set).

pub fn add_op<F>(&mut self, name: impl Into<String>, f: F)

where F: Fn(&[ModelValue]) -> Result<ModelValue, GatError> + Send + Sync + 'static,

Add an operation interpretation.

pub fn eval( &self, op_name: &str, args: &[ModelValue], ) -> Result<ModelValue, GatError>

Evaluate an operation by name on the given arguments.

Errors

Returns GatError::OpNotFound if the operation is not in this model, or GatError::ModelError if the operation function itself fails.

Trait Implementations

impl Debug for Model

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

Formats the value using the given formatter.