Struct z3tracer::model::ModelConfig

pub struct ModelConfig {
    pub parser_config: ParserConfig,
    pub display_qi_logs: bool,
    pub with_qi_variables: bool,
    pub with_qi_triggers: bool,
    pub with_qi_produced_terms: bool,
    pub with_qi_used_terms: bool,
    pub log_term_equalities: bool,
    pub log_internal_term_equalities: bool,
    pub skip_log_consistency_checks: bool,
}

Configuration for the analysis of Z3 traces.

Fields

parser_config: ParserConfig

display_qi_logs: bool

Whether to log quantifier instantiations (QIs).

with_qi_variables: bool

Whether to display variable instantiations in QIs

with_qi_triggers: bool

Whether to display triggers in QIs.

with_qi_produced_terms: bool

Whether to display terms produced by QIs.

with_qi_used_terms: bool

Whether to display terms used by QIs.

log_term_equalities: bool

Whether to log term equalities.

log_internal_term_equalities: bool

Whether to log term equalities (internal loop).

skip_log_consistency_checks: bool

Whether to run consistency checks for identifiers, equations, etc.

Trait Implementations

impl Clone for ModelConfig

fn clone(&self) -> ModelConfig

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ModelConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ModelConfig

fn default() -> ModelConfig

Returns the “default value” for a type.

impl StructOpt for ModelConfig

fn clap<'a, 'b>() -> App<'a, 'b>

Returns clap::App corresponding to the struct.

fn from_clap(matches: &ArgMatches<'_>) -> Self

Builds the struct from clap::ArgMatches. It’s guaranteed to succeed if matches originates from an App generated by StructOpt::clap called on the same type, otherwise it must panic.

fn from_args() -> Self

Builds the struct from the command line arguments (std::env::args_os). Calls clap::Error::exit on failure, printing the error message and aborting the program.

fn from_args_safe() -> Result<Self, Error>

Builds the struct from the command line arguments (std::env::args_os). Unlike StructOpt::from_args, returns clap::Error on failure instead of aborting the program, so calling .exit is up to you.

fn from_iter<I>(iter: I) -> Self where
    I: IntoIterator,
    <I as IntoIterator>::Item: Into<OsString>,
    <I as IntoIterator>::Item: Clone, 

Gets the struct from any iterator such as a Vec of your making. Print the error message and quit the program in case of failure.

fn from_iter_safe<I>(iter: I) -> Result<Self, Error> where
    I: IntoIterator,
    <I as IntoIterator>::Item: Into<OsString>,
    <I as IntoIterator>::Item: Clone, 

Gets the struct from any iterator such as a Vec of your making.

impl StructOptInternal for ModelConfig

fn augment_clap<'a, 'b>(app: App<'a, 'b>) -> App<'a, 'b>

fn is_subcommand() -> bool

fn from_subcommand(_sub: (&'b str, Option<&'b ArgMatches<'a>>)) -> Option<Self>