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 element_encoding: Option<ElementEncoding>,
    pub table_encoding: Option<TableEncoding>,
    pub alldifferent_encoding: Option<AllDifferentEncoding>,
    pub amo_encoding: Option<AmoEncoding>,
    pub cardinality_encoding: Option<CardinalityEncoding>,
    pub pb_encoding: Option<PbEncoding>,
    pub solver: SolverFamily,
    pub sat_backend: SatBackend,
    pub minion_discrete_threshold: Option<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.

Counts are kept in memory and written when the program exits, 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 estimates structural work for supported Minion representation choices, falling back to representation-domain size elsewhere, and minimises resulting AST depth for equally-applicable rewrite rules. Use -v to inspect representation costs. 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, uniform. Channelling is disabled by default. uniform uses one representation kind per type family throughout the model. Enable yes for 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).

element_encoding: Option<ElementEncoding>

Pin the SAT element composition: implication or support.

table_encoding: Option<TableEncoding>

Pin the SAT table composition: tuple, mdd or binary-support (constant two-column relations).

alldifferent_encoding: Option<AllDifferentEncoding>

Pin allDifferent: pairwise, or value-amo (requires Direct or Boolean value indicators).

amo_encoding: Option<AmoEncoding>

Pin the SAT AMO encoder: pairwise, ladder, bitwise, commander, bimander, two-product, pindakaas-pairwise, pindakaas-ladder or pindakaas-bitwise. If omitted, compact chooses per constraint; portfolio heuristics share one family choice.

cardinality_encoding: Option<CardinalityEncoding>

Pin the SAT cardinality encoder: rustsat-totalizer or pindakaas-sorting-network.

pb_encoding: Option<PbEncoding>

Pin the SAT weighted encoder: rustsat-generalized-totalizer, rustsat-binary-adder, pindakaas-bdd, rustsat-dynamic-poly-watchdog, or pindakaas-swc.

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.

sat_backend: SatBackend

SAT backend to use with –solver sat (only compiled backends are available).

minion_discrete_threshold: Option<usize>

Pin the int-domain span threshold for using Minion DISCRETE variables.

If maximum - minimum + 1 <= this value, emit DISCRETE; otherwise BOUND. Constraints requiring DISCRETE override this choice. If omitted, the heuristic chooses between 10, zero (all BOUND), and unlimited (all DISCRETE). Compact chooses 10.

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) -> Self

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: 240 bytes