pub struct Z3Parser {
pub lits: Literals,
pub strings: StringTable,
pub events: EventLog,
/* private fields */
}Expand description
A parser for Z3 log files. Use one of the various Z3Parser::from_* methods
to construct this parser.
Fields§
§lits: Literals§strings: StringTable§events: EventLogImplementations§
Source§impl Z3Parser
impl Z3Parser
pub fn errors(&self) -> ParseErrors
pub fn meaning(&self, tidx: TermIdx) -> Option<&Meaning>
pub fn from_to(&self, eq: EqTransIdx) -> (ENodeIdx, ENodeIdx)
pub fn quant_count_incl_theory_solving(&self) -> (usize, bool)
pub fn quantifiers(&self) -> &TiSlice<QuantIdx, Quantifier>
pub fn instantiations(&self) -> &TiSlice<InstIdx, Instantiation>
pub fn instantiations_data(&self) -> impl Iterator<Item = InstData<'_>> + '_
pub fn terms(&self) -> &TiSlice<TermIdx, Term>
pub fn proofs(&self) -> &TiSlice<ProofIdx, ProofStep>
pub fn cdcls(&self) -> &TiSlice<CdclIdx, Cdcl>
pub fn quantifier_body(&self, qidx: QuantIdx) -> Option<TermIdx>
pub fn patterns(&self, q: QuantIdx) -> Option<&TiSlice<PatternIdx, TermIdx>>
pub fn get_inst(&self, iidx: InstIdx) -> InstData<'_>
pub fn get_instantiation_body(&self, iidx: InstIdx) -> Option<TermIdx>
pub fn as_tidx(&self, sidx: SynthIdx) -> Option<TermIdx>
pub fn get_pattern(&self, qpat: QuantPat) -> Option<TermIdx>
pub fn get_pattern_term(&self, qpat: QuantPat) -> Option<&Term>
pub fn get_frame(&self, idx: impl HasFrame) -> &StackFrame
Sourcepub fn proves_false(&self, pidx: ProofIdx) -> bool
pub fn proves_false(&self, pidx: ProofIdx) -> bool
Does the proof step pidx prove false? This can may be under a
hypothesis so might not necessarily imply unsat.
Sourcepub fn ast_size(
&self,
tidx: TermIdx,
cached: &mut FxHashMap<TermIdx, AstSize>,
) -> AstSize
pub fn ast_size( &self, tidx: TermIdx, cached: &mut FxHashMap<TermIdx, AstSize>, ) -> AstSize
Returns the size in AST nodes of the term tidx. Note that z3 eagerly
reduces terms such as 1 + 1 to 2 meaning that a matching loop can be
constant in this size metric!
pub fn inst_ast_size( &self, iidx: InstIdx, cached: &mut FxHashMap<TermIdx, AstSize>, ) -> Option<NonMaxU64>
pub fn new_quant_pat_vec<T>(&self, f: impl Fn(QuantPat) -> T) -> QuantPatVec<T>
Trait Implementations§
Source§impl Index<EqGivenIdx> for Z3Parser
impl Index<EqGivenIdx> for Z3Parser
Source§type Output = EqualityExpl
type Output = EqualityExpl
The returned type after indexing.
Source§impl Index<EqTransIdx> for Z3Parser
impl Index<EqTransIdx> for Z3Parser
Source§type Output = TransitiveExpl
type Output = TransitiveExpl
The returned type after indexing.
Source§impl Z3LogParser for Z3Parser
impl Z3LogParser for Z3Parser
fn newline(&mut self)
fn version_info<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_quant<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_lambda<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_var<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_app<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_proof<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn attach_meaning<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn attach_var_names<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn attach_enode<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn eq_expl<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn new_match<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn inst_discovered<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn end_of_instance<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn eof(&mut self)
fn assign<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn decide_and_or<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn conflict<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn push<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn pop<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn begin_check<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn decide<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn query_done<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn resolve_process<'a>( &mut self, _l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn resolve_lit<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
Auto Trait Implementations§
impl Freeze for Z3Parser
impl RefUnwindSafe for Z3Parser
impl Send for Z3Parser
impl Sync for Z3Parser
impl Unpin for Z3Parser
impl UnwindSafe for Z3Parser
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§impl<T> LogParser for Twhere
T: Z3LogParser + LogParserHelper,
impl<T> LogParser for Twhere
T: Z3LogParser + LogParserHelper,
Source§fn is_line_start(&mut self, first_byte: u8) -> bool
fn is_line_start(&mut self, first_byte: u8) -> bool
Can be used to allow for parsing entries across multiple lines.
Source§fn process_line(
&mut self,
line: &str,
line_no: usize,
) -> Result<bool, FatalError>
fn process_line( &mut self, line: &str, line_no: usize, ) -> Result<bool, FatalError>
Process a single line of the log file. Return
true if parsing should
continue, or false if parsing should stop.fn end_of_file(&mut self)
Source§fn from<'r, R: BufRead + 'r>(reader: R) -> StreamParser<'r, Self>
fn from<'r, R: BufRead + 'r>(reader: R) -> StreamParser<'r, Self>
Creates a new parser. Only use this if you cannot use the following
convenience methods: Read more
Source§fn from_async<'r, R: AsyncBufRead + Unpin + 'r>(
reader: R,
) -> AsyncParser<'r, Self>
fn from_async<'r, R: AsyncBufRead + Unpin + 'r>( reader: R, ) -> AsyncParser<'r, Self>
Creates a new async parser from an async buffered reader. The parser
will read rom the reader line-by-line.
Source§fn from_str(s: &str) -> StreamParser<'_, Self>
fn from_str(s: &str) -> StreamParser<'_, Self>
Creates a new parser from the contents of a log file. The string
argument must live as long as parsing is ongoing. Release this
constraint by using
take_parser to end
parsing. If you want the parser to take ownership of the string instead
(i.e. you are running into lifetime issues), use
from_string instead.Source§fn from_str_all(s: &str) -> Result<Self, FatalError>
fn from_str_all(s: &str) -> Result<Self, FatalError>
See
from_str and process_all.Source§fn from_string(s: String) -> StreamParser<'static, Self>
fn from_string(s: String) -> StreamParser<'static, Self>
Creates a new parser from the contents of a log file. The parser takes
ownership over the string.
Source§fn from_string_all(s: String) -> Result<Self, FatalError>
fn from_string_all(s: String) -> Result<Self, FatalError>
See
from_string and process_all.Source§fn from_file<P: AsRef<Path>>(
p: P,
) -> Result<(Metadata, StreamParser<'static, Self>)>
fn from_file<P: AsRef<Path>>( p: P, ) -> Result<(Metadata, StreamParser<'static, Self>)>
Creates a new streaming parser from a file. Additionally returns the
file metadata so that the progress can be calculated from the file size. Read more
Source§fn from_file_all<P: AsRef<Path>>(p: P) -> Result<Self, FatalError>
fn from_file_all<P: AsRef<Path>>(p: P) -> Result<Self, FatalError>
See
from_file and process_all.