Module settings 

Structs

HeuristicChoice

RewriteConfig

SolverArgs

SolverFamilyIter

An iterator over the variants of SolverFamily

Enums

Channelling

Whether a declaration may have more than one channelled representation.

Heuristic

Strategy used when a modelling decision has more than one applicable answer.

Parser

QuantifiedExpander

Rewriter

SolverFamily

Constants

DEFAULT_HEURISTIC_SEED

DEFAULT_MINION_DISCRETE_THRESHOLD

Functions

begin_heuristic_all_choices

Starts one replay of the x heuristic using the requested branch indices.

channelling

clear_heuristic_responses

Clears any remaining interactive responses.

comprehension_expander

configured_rule_trace_enabled

current_parser

current_rewriter

current_solver_family

default_rule_trace_enabled

heuristic

heuristic_all_choices

ints_need_representation

Whether integers carry a representation choice for the solver being targeted.

minion_discrete_threshold

next_heuristic_all_index

Selects the requested branch at the next x decision and records all available options.

next_heuristic_interactive_index

Selects an option for the interactive heuristic (i).

next_heuristic_random_index

Returns a deterministic pseudo-random index and advances the per-thread heuristic RNG.

rule_attempt_trace_enabled

rule_trace_aggregates_enabled

rule_trace_enabled

set_channelling

set_comprehension_expander

set_current_parser

set_current_rewriter

set_current_solver_family

set_default_rule_trace_enabled

set_heuristic

set_heuristic_responses

Sets the 1-based answers consumed by the interactive heuristic (i).

set_heuristic_seed

set_minion_discrete_threshold

set_rule_attempt_trace_enabled

set_rule_trace_aggregates_enabled

set_rule_trace_enabled

try_current_solver_family

The active solver family, or None if this thread has not set one.

with_compact_heuristic

Runs f with the compact heuristic in force, whatever the configured one is.

with_solver_family

Runs f as a rewrite for solver_family, then restores the surrounding solver context.