in z3tracer/src/parser.rs [97:317]
fn parse_line(&mut self) -> RawResult<bool> {
let lexer = &mut self.lexer;
let state = &mut self.state;
match lexer.read_string().unwrap().as_ref() {
"[mk-app]" => {
let id = lexer.read_fresh_ident()?;
let name = lexer.read_string()?;
let args = lexer.read_idents()?;
let term = Term::App {
name,
args,
meaning: None,
};
state.add_term(id, term)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[mk-var]" => {
let id = lexer.read_fresh_ident()?;
let index = lexer.read_integer()?;
let term = Term::Var { index };
state.add_term(id, term)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[mk-quant]" => {
let id = lexer.read_fresh_ident()?;
let name = lexer.read_string()?;
let params = lexer.read_integer()? as usize;
let mut triggers = lexer.read_idents()?;
let body = triggers.pop().ok_or(RawError::MissingIdentifier)?;
let term = Term::Quant {
name,
params,
triggers,
body,
var_names: None,
};
state.add_term(id, term)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[mk-lambda]" => {
let id = lexer.read_fresh_ident()?;
let name = lexer.read_string()?;
let params = lexer.read_integer()?;
let mut triggers = lexer.read_idents()?;
let body = triggers.pop().ok_or(RawError::MissingIdentifier)?;
let term = Term::Lambda {
name,
params,
triggers,
body,
};
state.add_term(id, term)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[mk-proof]" => {
let id = lexer.read_fresh_ident()?;
let name = lexer.read_string()?;
let mut args = lexer.read_idents()?;
let property = args.pop().ok_or(RawError::MissingIdentifier)?;
let term = Term::Proof {
name,
args,
property,
};
state.add_term(id, term)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[attach-meaning]" => {
let id = lexer.read_ident()?;
let theory = lexer.read_string()?;
let sexp = lexer.read_line()?;
let meaning = Meaning { theory, sexp };
state.attach_meaning(id, meaning)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[attach-var-names]" => {
let id = lexer.read_ident()?;
let names = lexer.read_var_names()?;
state.attach_var_names(id, names)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[inst-discovered]" => {
let method = lexer.read_string()?;
let key = lexer.read_fresh_key()?;
let quantifier = lexer.read_ident()?;
let terms = lexer.read_idents()?;
let blame = lexer.read_idents()?;
let frame = QiFrame::Discovered {
method,
quantifier,
terms,
blame,
};
state.add_instantiation(key, frame)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[new-match]" => {
let key = lexer.read_fresh_key()?;
let quantifier = lexer.read_ident()?;
let trigger = lexer.read_ident()?;
let terms = lexer.read_idents()?;
let used = lexer.read_matched_terms()?;
let frame = QiFrame::NewMatch {
quantifier,
trigger,
terms,
used,
};
state.add_instantiation(key, frame)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[eq-expl]" => {
let id = lexer.read_ident()?;
let eq = lexer.read_equality()?;
state.add_equality(id, eq)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[instance]" => {
let key = lexer.read_key()?;
let term = lexer.read_optional_ident()?;
let generation = lexer.read_optional_integer()?;
let instance = QiInstance {
generation,
term,
enodes: Vec::new(),
};
state.start_instance(key, instance)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[attach-enode]" => {
let id = lexer.read_ident()?;
let generation = lexer.read_integer()?;
state.attach_enode(id, generation)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[end-of-instance]" => {
state.end_instance()?;
lexer.read_end_of_line()?;
Ok(true)
}
"[tool-version]" => {
let s1 = lexer.read_string()?;
let s2 = lexer.read_string()?;
if !self.config.skip_z3_version_check {
RawError::check_that_tool_version_is_supported(&s1, &s2)?;
}
state.tool_version(s1, s2)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[begin-check]" => {
let i = lexer.read_integer()?;
state.begin_check(i)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[assign]" => {
let lit = lexer.read_literal()?;
let s = lexer.read_line()?;
state.assign(lit, s)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[conflict]" => {
let lits = lexer.read_literals()?;
let s = lexer.read_line()?;
state.conflict(lits, s)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[push]" => {
let i = lexer.read_integer()?;
state.push(i)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[pop]" => {
let i = lexer.read_integer()?;
let j = lexer.read_integer()?;
state.pop(i, j)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[resolve-lit]" => {
let i = lexer.read_integer()?;
let lit = lexer.read_literal()?;
state.resolve_lit(i, lit)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[resolve-process]" => {
let lit = lexer.read_literal()?;
state.resolve_process(lit)?;
lexer.read_end_of_line()?;
Ok(true)
}
"[eof]" => {
lexer.read_end_of_line()?;
Ok(false)
}
s if self.config.ignore_invalid_lines && !s.starts_with('[') => {
// Ignore lines not starting with '['
lexer.read_line()?;
lexer.read_end_of_line()?;
Ok(true)
}
s => Err(RawError::UnknownCommand(s.to_string())),
}
}