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 open(path: &Path) -> Result<Model, Vec<Error>>
pub fn open(path: &Path) -> Result<Model, Vec<Error>>
Read a model from a file, and every model it is written on top of.
An include names a file from the root of the repository, which is the first directory
above the including one whose Cargo.toml says it is a workspace. Naming it that way
rather than relative to whoever wrote the include is what makes the path in an include
read the same as the path in the prose beside it, since everything else in this
repository names a file from the root.
A file included twice is read once. That is the normal case rather than a mistake, since two rule sets over the same IR are two models including one file, and it is also what stops a cycle.
§Errors
Everything Model::read refuses, plus a file that is not there, a repository root that
cannot be found, and a head that two of the files give a meaning to.
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.
What the text includes is remembered rather than followed, because following it means
reading files and this takes text. Model::open is the one that reads files.
§Errors
Anything that is not a well formed (semantics (head params) body) form or a well formed
(include path) form, and any head given a meaning twice.
Sourcepub fn knows(&self, head: &str) -> bool
pub fn knows(&self, head: &str) -> bool
Whether this model gives a head a meaning.
What a rule needs is Model::write, which expands a whole term. This is for anything
asking about one head on its own, which is a test and a message about a head with no
entry anywhere.
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.
Sourcepub fn touches_floats(&self, term: &Term) -> bool
pub fn touches_floats(&self, term: &Term) -> bool
Whether reading this term reaches a float, following every head the model defines.
A rule that does needs a solver told about floats, and a solver told about floats is
slower at every rule that has none, so the question is worth asking rather than answering
yes for the whole file. A head is a float either by its own suffix, as fadd.f32 is, or
by what the model says it means.