fn extract_mem_vector(
        &self,
        model: &Model,
        domain: &ModelValue,
        domain_info_opt: &Option<(
            BTreeMap<ModelValue, BTreeMap<usize, bool>>,
            Option<ModelValue>,
            bool,
        )>,
    ) -> Option<ModelValueVector> {
        let mut size = 0;
        let domain_info = (*domain_info_opt).as_ref()?;
        let domain_idx_map = &domain_info.0;
        let default_domain_model_opt = &domain_info.1;
        let default_domain_flag = domain_info.2;

        let value_array_map = model
            .vars
            .get(&ModelValue::literal(&deduct_table_name(
                self.extract_literal()?,
            )?))?
            .extract_map()?;

        // In the model, the Store_ represents the update of that map
        let value_update_map_opt = model
            .vars
            .get(&ModelValue::literal(&deduct_update_table_name(
                self.extract_literal()?,
            )?))
            .and_then(|update_map| update_map.extract_map());

        let mut domain_exists_map_opt = domain_idx_map.get(domain);
        if domain_exists_map_opt == None {
            if let Some(default_domain_model) = default_domain_model_opt {
                domain_exists_map_opt = domain_idx_map.get(default_domain_model);
            }
        }

        let mut values = BTreeMap::new();
        let mut default = ModelValue::error();

        let mut insert_values = |elem_opt: &ModelValue, new_value: &ModelValue| {
            if let Some(idx) = elem_opt.extract_number() {
                if let Some(domain_exists_map) = domain_exists_map_opt {
                    let mut flag = default_domain_flag;
                    if let Some(domain_exists_value) = domain_exists_map.get(&idx) {
                        flag = *domain_exists_value;
                    }
                    if flag {
                        // Only print the memory locations in the domain
                        values.insert(idx, new_value.clone());
                        size += 1;
                    }
                }
            }
        };

        // Each entry in value_array_map takes the form:
        // key: |T@[Int]$1_Bug7_BallotCounter!val!0| 0
        // value: ($1_Bug7_BallotCounter 18446744073709522257)
        // elems[1] is index to represent the instance of the memory
        for (key, value) in value_array_map {
            if let ModelValue::List(elems) = key {
                if elems.len() == 2 && &elems[0] == self {
                    insert_values(&elems[1], value);
                }
            } else if key == &ModelValue::literal("else") {
                // Currently, we assume existence of default memory locations print out the value.
                if default_domain_flag {
                    default = value.clone();
                }
            }
        }

        // Travese the update map to obtain the updated value
        if let Some(value_update_map) = value_update_map_opt {
            for up_k in value_update_map.keys() {
                if let ModelValue::List(elems) = up_k {
                    // We only consider the case
                    // Where elems has three elements: Array symbol, position, updated value
                    if elems.len() == 3 && &elems[0] == self {
                        insert_values(&elems[1], &elems[2]);
                    }
                }
            }
        }

        Some(ModelValueVector {
            size,
            values,
            default,
        })
    }
/// Extract memory content from the model
Extract memory content from the model
Extract memory content from the model
fn extract_mem_vector(
        &self,
        model: &Model,
        domain: &ModelValue,
        domain_info_opt: &Option<(
            BTreeMap<ModelValue, BTreeMap<usize, bool>>,
            Option<ModelValue>,
            bool,
        )>,
    ) -> Option<ModelValueVector> {
        let mut size = 0;
        let domain_info = (*domain_info_opt).as_ref()?;
        let domain_idx_map = &domain_info.0;
        let default_domain_model_opt = &domain_info.1;
        let default_domain_flag = domain_info.2;
        let value_array_map = model
            .vars
            .get(&ModelValue::literal(&deduct_table_name(
                self.extract_literal()?,
            )?))?
            .extract_map()?;
        // In the model, the Store_ represents the update of that map
        let value_update_map_opt = model
            .vars
            .get(&ModelValue::literal(&deduct_update_table_name(
                self.extract_literal()?,
            )?))
            .and_then(|update_map| update_map.extract_map());
        let mut domain_exists_map_opt = domain_idx_map.get(domain);
        if domain_exists_map_opt == None {
            if let Some(default_domain_model) = default_domain_model_opt {
                domain_exists_map_opt = domain_idx_map.get(default_domain_model);
            }
        }
        let mut values = BTreeMap::new();
        let mut default = ModelValue::error();
        let mut insert_values = |elem_opt: &ModelValue, new_value: &ModelValue| {
            if let Some(idx) = elem_opt.extract_number() {
                if let Some(domain_exists_map) = domain_exists_map_opt {
                    let mut flag = default_domain_flag;
                    if let Some(domain_exists_value) = domain_exists_map.get(&idx) {
                        flag = *domain_exists_value;
                    }
                    if flag {
                        // Only print the memory locations in the domain
                        values.insert(idx, new_value.clone());
                        size += 1;
                    }
                }
            }
        };
        // Each entry in value_array_map takes the form:
        // key: |T@[Int]$1_Bug7_BallotCounter!val!0| 0
        // value: ($1_Bug7_BallotCounter 18446744073709522257)
        // elems[1] is index to represent the instance of the memory
        for (key, value) in value_array_map {
            if let ModelValue::List(elems) = key {
                if elems.len() == 2 && &elems[0] == self {
                    insert_values(&elems[1], value);
                }
            } else if key == &ModelValue::literal("else") {
                // Currently, we assume existence of default memory locations print out the value.
                if default_domain_flag {
                    default = value.clone();
                }
            }
        }
        // Travese the update map to obtain the updated value
        if let Some(value_update_map) = value_update_map_opt {
            for up_k in value_update_map.keys() {
                if let ModelValue::List(elems) = up_k {
                    // We only consider the case
                    // Where elems has three elements: Array symbol, position, updated value
                    if elems.len() == 3 && &elems[0] == self {
                        insert_values(&elems[1], &elems[2]);
                    }
                }
            }
        }
        Some(ModelValueVector {
            size,
            values,
            default,
        })
    }
fn extract_mem_vector ( & self , model : & Model , domain : & ModelValue , domain_info_opt : & Option < ( BTreeMap < ModelValue , BTreeMap < usize , bool > > , Option < ModelValue > , bool , ) > , ) -> Option < ModelValueVector > { let mut size = 0 ; let domain_info = ( * domain_info_opt ) . as_ref ( ) ? ; let domain_idx_map = & domain_info . 0 ; let default_domain_model_opt = & domain_info . 1 ; let default_domain_flag = domain_info . 2 ; let value_array_map = model . vars . get ( & ModelValue :: literal ( & deduct_table_name ( self . extract_literal ( ) ? , ) ? ) ) ? . extract_map ( ) ? ; // In the model, the Store_ represents the update of that map let value_update_map_opt = model . vars . get ( & ModelValue :: literal ( & deduct_update_table_name ( self . extract_literal ( ) ? , ) ? ) ) . and_then ( | update_map | update_map . extract_map ( ) ) ; let mut domain_exists_map_opt = domain_idx_map . get ( domain ) ; if domain_exists_map_opt == None { if let Some ( default_domain_model ) = default_domain_model_opt { domain_exists_map_opt = domain_idx_map . get ( default_domain_model ) ; } } let mut values = BTreeMap :: new ( ) ; let mut default = ModelValue :: error ( ) ; let mut insert_values = | elem_opt : & ModelValue , new_value : & ModelValue | { if let Some ( idx ) = elem_opt . extract_number ( ) { if let Some ( domain_exists_map ) = domain_exists_map_opt { let mut flag = default_domain_flag ; if let Some ( domain_exists_value ) = domain_exists_map . get ( & idx ) { flag = * domain_exists_value ; } if flag { // Only print the memory locations in the domain values . insert ( idx , new_value . clone ( ) ) ; size += 1 ; } } } } ; // Each entry in value_array_map takes the form: // key: |T@[Int]$1_Bug7_BallotCounter!val!0| 0 // value: ($1_Bug7_BallotCounter 18446744073709522257) // elems[1] is index to represent the instance of the memory for ( key , value ) in value_array_map { if let ModelValue :: List ( elems ) = key { if elems . len ( ) == 2 && & elems [ 0 ] == self { insert_values ( & elems [ 1 ] , value ) ; } } else if key == & ModelValue :: literal ( " " ) { // Currently, we assume existence of default memory locations print out the value. if default_domain_flag { default = value . clone ( ) ; } } } // Travese the update map to obtain the updated value if let Some ( value_update_map ) = value_update_map_opt { for up_k in value_update_map . keys ( ) { if let ModelValue :: List ( elems ) = up_k { // We only consider the case // Where elems has three elements: Array symbol, position, updated value if elems . len ( ) == 3 && & elems [ 0 ] == self { insert_values ( & elems [ 1 ] , & elems [ 2 ] ) ; } } } } Some ( ModelValueVector { size , values , default , } ) }
Extract memory content from the model
Extract memory content from the model
&self
model
&Model
domain
&ModelValue
domain_info_opt
&Option<(
            BTreeMap<ModelValue, BTreeMap<usize, bool>>,
            Option<ModelValue>,
            bool,
        )>