Struct BddVarManager 

pub struct BddVarManager {
    manager: BDDManager,
    loc_vars: HashMap<Location, BDD>,
    loc_vars_primed: HashMap<Location, BDD>,
    variable_vars: HashMap<Variable, Vec<BDD>>,
    variable_vars_primed: HashMap<Variable, Vec<BDD>>,
    shared_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>,
    shared_primed_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>,
    rule_vars: Vec<BDD>,
    rule_to_bdd: HashMap<IntervalTARule, BDD>,
    unprimed_vars_vec: Vec<BDD>,
    primed_vars_vec: Vec<BDD>,
}

Manager for BDD variables for an underlying IntervalThresholdAutomaton

Fields

manager: BDDManager

The BDD manager

loc_vars: HashMap<Location, BDD>

BDD variables for each location

loc_vars_primed: HashMap<Location, BDD>

Location successor BDD variables

variable_vars: HashMap<Variable, Vec<BDD>>

BDD variables for each variable

variable_vars_primed: HashMap<Variable, Vec<BDD>>

Variable successor BDD variables

shared_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>

Mapping for each variable from unprimed interval to the corresponding BDD

shared_primed_interval_to_bdd: HashMap<Variable, HashMap<Interval, BDD>>

Mapping for each variable from primed interval to the correspond BDD

rule_vars: Vec<BDD>

BDD variables to represent the rule_id

rule_to_bdd: HashMap<IntervalTARule, BDD>

Mapping from abstract rule to the corresponding BDD

unprimed_vars_vec: Vec<BDD>

All unprimed bdd variables for locations and shared variables

primed_vars_vec: Vec<BDD>

All primed bdd variables for locations and shared variables

Implementations

impl BddVarManager

pub fn new(mgr: BDDManager, automaton: &IntervalThresholdAutomaton) -> Self

creates a new BDDVarManager

fn initialize(&mut self, aut: &IntervalThresholdAutomaton)

initializes the bdd_var_manager

1. create unprimed and primed location vars
2. create unprimed and primed shared variable intervals
3. create bdd_variables to represent rules
4. create ordered vectors for all unprimed and primed bdd variables

fn initialize_loc_vars(&mut self, aut: &IntervalThresholdAutomaton)

initializes all unprimed and primed bdd variables for locations

fn initialize_shared_vars(&mut self, aut: &IntervalThresholdAutomaton)

initializes all unprimed and primed bdd variables for shared variables

fn initialize_rule_vars(&mut self, aut: &IntervalThresholdAutomaton)

pub fn get_location_var( &self, loc: &Location, ) -> Result<&BDD, BDDVarManagerError>

get the BDD variable for a location

pub fn get_primed_location_var( &self, loc: &Location, ) -> Result<&BDD, BDDVarManagerError>

get the primed BDD variable for a location

pub fn get_shared_interval_bdd( &self, shared: &Variable, interval: &Interval, ) -> Result<&BDD, BDDVarManagerError>

get the BDD variables for a shared variable

pub fn get_primed_shared_interval_bdd( &self, shared: &Variable, interval: &Interval, ) -> Result<&BDD, BDDVarManagerError>

get the primed BDD variables for a shared variable

pub fn get_rule_bdd( &self, rule: &IntervalTARule, ) -> Result<&BDD, BDDVarManagerError>

get the BDD for an abstract rule

pub fn get_bdd_true(&self) -> BDD

get the constant true BDD

pub fn get_bdd_false(&self) -> BDD

get the constant false BDD

fn new_location_var(&mut self, loc: &Location)

creates and stores a new bdd variable to represent a given location

fn new_primed_location_var(&mut self, loc: &Location)

creates and stores a new primed bdd variable to represent a given location

fn new_shared_var(&mut self, shared: &Variable)

creates and stores a new bdd variable to represent the interval of a shared variable

fn new_primed_shared_var(&mut self, shared: &Variable)

creates and stores a new primed bdd variable to represent the interval of a shared variable

fn new_rule_var(&mut self)

creates and stores a new bdd variable to represent a rule

fn encode_bitwise_bdd(&self, index: u32, bdd_vars: &[BDD]) -> BDD

Given index and a vector of bdd variables, Returns the bitwise encoded bdd for index if enough bdd variables are provided

pub fn get_unchanged_interval_bdd( &self, shared: &Variable, ) -> Result<BDD, BDDVarManagerError>

Constructs a constraint which checks that the bdd variables for an unprimed and primed shared variable are unchanged

fn create_unprimed_primed_vecs(&mut self)

Creates an ordered vector for all unprimed and primed bdd variables

pub fn swap_unprimed_primed_bdd_vars(&self, cur: &BDD) -> BDD

Swaps all unprimed and primed bdd variables for cur

pub fn exists_unprimed(&self, cur: &BDD) -> BDD

abstracts all bdd variables for unprimed locations and unprimed shared variables for a given bdd

pub fn exists_primed(&self, cur: &BDD) -> BDD

abstracts all primed bdd variables for primed locations and primed shared variables for a given bdd cur

pub fn exists_rule_vars(&self, cur: &BDD) -> BDD

abstracts all bdd variables for rule_ids for a given bdd cur

Trait Implementations

impl Clone for BddVarManager

fn clone(&self) -> BddVarManager

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BddVarManager

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

Formats the value using the given formatter.