Struct Model 

pub struct Model { /* private fields */ }

Everything the rules are allowed to say, and what each of it means.

Implementations

impl Model

pub fn read(path: &str, text: &str) -> Result<Model, Vec<Error>>

Read a model from text.

Errors

Anything that is not a well formed (semantics (head params) body) form, and any head given a meaning twice.

pub fn write( &self, path: &str, term: &Term, widths: &Widths, ) -> Result<(String, u32), Error>

Write one term out as SMT-LIB, expanding everything the model defines, and say how wide what it computes is.

Errors

A head that is neither a builtin nor in the model, since that is a term nobody has said the meaning of, an application of the wrong number of arguments, and anything whose widths do not fit together.

Trait Implementations

impl Debug for Model

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

Formats the value using the given formatter.

impl Default for Model

fn default() -> Model

Returns the “default value” for a type.