pub struct Model { /* private fields */ }Expand description
Everything the rules are allowed to say, and what each of it means.
Implementations§
Source§impl Model
impl Model
Sourcepub fn read(path: &str, text: &str) -> Result<Model, Vec<Error>>
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.
Sourcepub fn write(
&self,
path: &str,
term: &Term,
widths: &Widths,
) -> Result<(String, Sort), Error>
pub fn write( &self, path: &str, term: &Term, widths: &Widths, ) -> Result<(String, Sort), 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.
Sourcepub fn touches_memory(&self, term: &Term) -> bool
pub fn touches_memory(&self, term: &Term) -> bool
Whether reading this term reaches memory, following every head the model defines.
A rule that reads memory needs a solver told about arrays and a constant to stand for the
memory it starts from, and neither is worth putting in a query that does not. Nothing in a
rule says (mem) directly: a load says load.i32, and it is the model entry for that head
which reaches memory, so this expands what the model says rather than reading the surface.