Struct varisat::variables::Variables

pub struct Variables {
    global_from_user: VarBiMap,
    solver_from_global: VarBiMap,
    user_freelist: HashSet<Var>,
    global_freelist: HashSet<Var>,
    solver_freelist: HashSet<Var>,
    var_data: Vec<VarData>,
}

Variable mapping and metadata.

Fields

global_from_user: VarBiMap

Bidirectional mapping from user variables to global variables.

Initially this is the identity mapping. This ensures that in the non-assumptions setting the map from used user variables to global variables is the identity. This is a requirement for generating proofs in non-native formats. Those proofs are not aware of variable renaming, but are restricted to the non-incremental setting, so this works out.

This is also requried for native proofs, as they assume that the mapping during the initial load is the identity.

solver_from_global: VarBiMap

Bidirectional mapping from global variables to user variables.

This starts with the empty mapping, so only used variables are allocated.

user_freelist: HashSet<Var>

User variables that were explicitly hidden by the user.

global_freelist: HashSet<Var>

Global variables that can be recycled without increasing the global_watermark.

solver_freelist: HashSet<Var>

Solver variables that are unused and can be recycled.

var_data: Vec<VarData>

Variable metadata.

Indexed by global variable indices.

Methods

impl Variables

pub fn solver_watermark(&self) -> usize

Number of allocated solver variables.

pub fn global_watermark(&self) -> usize

Number of allocated global variables.

pub fn user_watermark(&self) -> usize

Number of allocated global variables.

pub fn user_var_iter<'a>(&'a self) -> impl Iterator<Item = Var> + 'a

Iterator over all user variables that are in use.

pub fn global_var_iter<'a>(&'a self) -> impl Iterator<Item = Var> + 'a

Iterator over all global variables that are in use.

pub fn global_from_user(&self) -> &VarMap

The user to global mapping.

pub fn global_from_user_mut(&mut self) -> VarBiMapMut

Mutable user to global mapping.

pub fn solver_from_global(&self) -> &VarMap

The global to solver mapping.

pub fn solver_from_global_mut(&mut self) -> VarBiMapMut

Mutable global to solver mapping.

pub fn user_from_global(&self) -> &VarMap

The global to user mapping.

pub fn user_from_global_mut(&mut self) -> VarBiMapMut

Mutable global to user mapping.

pub fn global_from_solver(&self) -> &VarMap

The solver to global mapping.

pub fn global_from_solver_mut(&mut self) -> VarBiMapMut

Mutable solver to global mapping.

pub fn existing_solver_from_user(&self, user: Var) -> Var

Get an existing solver var for a user var.

pub fn existing_user_from_solver(&self, solver: Var) -> Var

Get an existing user var from a solver var.

pub fn var_data_global_mut(&mut self, global: Var) -> &mut VarData

Mutable reference to the var data for a global variable.

pub fn var_data_solver_mut(&mut self, solver: Var) -> &mut VarData

Mutable reference to the var data for a solver variable.

pub fn var_data_global(&self, global: Var) -> &VarData

Var data for a global variable.

pub fn solver_var_present(&self, solver: Var) -> bool

Check if a solver var is mapped to a global var

pub fn next_unmapped_global(&self) -> Var

Get an unmapped global variable.

pub fn next_unmapped_solver(&self) -> Var

Get an unmapped global variable.

pub fn next_unmapped_user(&self) -> Var

Get an unmapped user variable.

Trait Implementations

impl Default for Variables

fn default() -> Variables

Returns the "default value" for a type.