Struct GlobalArgs 

pub struct GlobalArgs {

    pub help: (),
    pub extra_rule_sets: Vec<String>,
    pub verbose: u8,
    pub quiet: bool,
    pub rule_trace: Option<PathBuf>,
    pub rule_trace_aggregates: Option<PathBuf>,
    pub rule_trace_cdp: bool,
    pub rule_attempt_trace: Option<PathBuf>,
    pub parser: Parser,
    pub rewriter: Rewriter,
    pub comprehension_expander: QuantifiedExpander,
    pub heuristic: Heuristic,
    pub responses: Vec<usize>,
    pub seed: u64,
    pub solver_seed: u32,
    pub channelling: Channelling,
    pub solver: SolverFamily,
    pub minion_discrete_threshold: usize,
    pub minion_varorder: Option<MinionVariableOrder>,
    pub minion_valorder: Option<MinionValueOrder>,
    pub save_solver_input_file: Option<PathBuf>,
    pub solver_timeout: Option<Duration>,
    pub log_file: Option<PathBuf>,
    pub log_format: Option<LogFormat>,
    pub log_detail: Option<LogDetail>,
}

Fields

help: ()

Print help

extra_rule_sets: Vec<String>

Extra rule sets to enable

verbose: u8

Increase stderr logging detail (-v: stages, -vv: rule applications, -vvv: rule attempts).

Rule-attempt logging can be expensive and produce a very large amount of output.

quiet: bool

Disable warning and progress logs on stderr

rule_trace: Option<PathBuf>

Output file for the default rule trace.

rule_trace_aggregates: Option<PathBuf>

Output file for aggregated rule-application counts.

The file is updated incrementally in the format: total_rule_applications: N, followed by one line per rule.

rule_trace_cdp: bool

Continue rule trace generation during solver-time CDP rewrites.

This is off by default, so follow-up dominance-blocking rewrites do not contribute to the trace.

rule_attempt_trace: Option<PathBuf>

Output file for the rule-attempt trace in CSV format.

Each row includes: elapsed_s, rule_level, rule_name, rule_set, status, expression.

parser: Parser

Which parser to use.

Possible values: tree-sitter, via-conjure.

rewriter: Rewriter

Which rewriter to use.

Possible values: baseline, optimised, baseline+prefilter, or baseline+worklist.

Option meanings:

• prefilter: skip rules whose declared expression kinds cannot match; strong win vs baseline and part of optimised.
• worklist: drive rewriting from persistent dirty queues instead of repeated full scans; strong win vs baseline and part of optimised.

comprehension_expander: QuantifiedExpander

Which strategy to use for expanding quantified variables in comprehensions.

Possible values: auto, native, via-solver, via-solver-ac. auto chooses between native and solver-backed expansion from the comprehension’s estimated size and available pruning constraints.

heuristic: Heuristic

Heuristic for selecting an answer when multiple modelling choices are applicable.

Possible values: f (first), r (random), c (compact), i (interactive). Compact minimises the representation-domain size for representation choices and the resulting AST depth for equally-applicable rewrite rules. Interactive prompts on stderr, or uses --responses when provided. x (all) is reserved for model generation and is not supported by the CLI yet.

responses: Vec<usize>

Comma-separated 1-based answers for the interactive heuristic (-h i).

If provided, these are used as the answers during interactive model generation instead of prompting the user.

seed: u64

Seed used by the random heuristic.

solver_seed: u32

Seed used by the backend solver’s random search behaviour.

channelling: Channelling

Whether multiple representations of the same declaration may be channelled together.

Possible values: no, yes. Channelling is disabled by default. Enable yes to allow different representations of the same variable at different call sites, e.g. 1 in (x :: set (representation packed) of int) /\ 2 in (x :: set (representation occurrence) of int).

solver: SolverFamily

Solver to use.

Possible values: minion, sat, z3.

How a model is expressed for the chosen solver – which SAT encoding an integer gets, or which Z3 theory – is a modelling choice made per declaration, not part of the solver name. Use --heuristic to steer those choices and --channelling to allow more than one per declaration.

minion_discrete_threshold: usize

Int-domain size threshold for using Minion DISCRETE variables.

If an int domain has size <= this value, Conjure Oxide emits DISCRETE; otherwise BOUND.

minion_varorder: Option<MinionVariableOrder>

Override Minion variable ordering.

Possible values: static, sdf, srf, ldf, random, conflict, wdeg, domoverwdeg.

minion_valorder: Option<MinionValueOrder>

Override Minion value ordering.

Possible values: ascend, descend, random.

save_solver_input_file: Option<PathBuf>

Save a solver input file to .

This input file will be in a format compatible by the command-line interface of the selected solver. For example, when the solver is Minion, a valid .minion file will be output.

This file is for informational purposes only; the results of running this file cannot be used by Conjure Oxide in any way.

solver_timeout: Option<Duration>

Stop the solver after the given cumulative wall-clock timeout.

Minion has one-second timeout resolution, so finer durations are rounded up.

log_file: Option<PathBuf>

Write general logs to this file

log_format: Option<LogFormat>

Format used by –log-file [default: text]

log_detail: Option<LogDetail>

Detail written by –log-file [default: stages]

Trait Implementations

impl Args for GlobalArgs

fn group_id() -> Option<Id>

Report the [ArgGroup::id][crate::ArgGroup::id] for this set of arguments

fn augment_args<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate Self via [FromArgMatches::from_arg_matches_mut]

fn augment_args_for_update<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate self via [FromArgMatches::update_from_arg_matches_mut]

impl Clone for GlobalArgs

fn clone(&self) -> GlobalArgs

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for GlobalArgs

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

Formats the value using the given formatter.

impl FromArgMatches for GlobalArgs

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

Layout

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 224 bytes