pub fn query(path: &str, rule: &Rule, model: &Model) -> Result<String, Error>Expand description
The SMT-LIB question one rule asks, at the width the rule works in.
This is separate from asking it so that the query can be read, kept in a test, and handed to a solver by hand when one is arguing with it.
ยงErrors
Anything the model cannot write out, which is any term nobody has said the meaning of.