Struct Environment 

pub struct Environment {

    pub defined_identifiers: HashMap<IdentifierName, ParamObjType>,
    pub defined_def_props: HashMap<PropName, DefPropStmt>,
    pub defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
    pub defined_families: HashMap<FamilyName, DefFamilyStmt>,
    pub defined_algorithms: HashMap<AlgoName, DefAlgoStmt>,
    pub defined_structs: HashMap<StructName, DefStructStmt>,
    pub known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
    pub known_atomic_facts_with_0_or_more_than_2_args: HashMap<(AtomicFactKey, bool), Vec<AtomicFact>>,
    pub known_atomic_facts_with_1_arg: HashMap<(AtomicFactKey, bool), HashMap<ObjString, AtomicFact>>,
    pub known_atomic_facts_with_2_args: HashMap<(AtomicFactKey, bool), HashMap<(ObjString, ObjString), AtomicFact>>,
    pub known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>,
    pub known_or_facts: HashMap<OrFactKey, Vec<OrFact>>,
    pub known_atomic_facts_in_forall_facts: HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>,
    pub known_exist_facts_in_forall_facts: HashMap<ExistFactKey, Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>>,
    pub known_or_facts_in_forall_facts: HashMap<OrFactKey, Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>>,
    pub known_objs_equal_to_tuple: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>,
    pub known_objs_equal_to_cart: HashMap<ObjString, (Cart, LineFile)>,
    pub known_objs_equal_to_finite_seq_list: HashMap<ObjString, (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile)>,
    pub known_objs_equal_to_matrix_list: HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>,
    pub known_objs_equal_to_normalized_decimal_number: HashMap<ObjString, Number>,
    pub known_objs_in_fn_sets: HashMap<ObjString, KnownFnInfo>,
    pub known_name_belong_to_struct: HashMap<String, StructName>,
    pub known_transitive_props: HashMap<String, ()>,
    pub known_commutative_props: HashMap<String, CommutativePropValue>,
    pub cache_well_defined_obj: HashMap<ObjString, ()>,
    pub cache_known_fact: HashMap<FactString, LineFile>,
}

Fields

defined_identifiers: HashMap<IdentifierName, ParamObjType>

defined_def_props: HashMap<PropName, DefPropStmt>

defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>

defined_families: HashMap<FamilyName, DefFamilyStmt>

defined_algorithms: HashMap<AlgoName, DefAlgoStmt>

defined_structs: HashMap<StructName, DefStructStmt>

known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>

known_atomic_facts_with_0_or_more_than_2_args: HashMap<(AtomicFactKey, bool), Vec<AtomicFact>>

known_atomic_facts_with_1_arg: HashMap<(AtomicFactKey, bool), HashMap<ObjString, AtomicFact>>

known_atomic_facts_with_2_args: HashMap<(AtomicFactKey, bool), HashMap<(ObjString, ObjString), AtomicFact>>

known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>

known_or_facts: HashMap<OrFactKey, Vec<OrFact>>

known_atomic_facts_in_forall_facts: HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>

known_exist_facts_in_forall_facts: HashMap<ExistFactKey, Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>>

known_or_facts_in_forall_facts: HashMap<OrFactKey, Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>>

known_objs_equal_to_tuple: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>

known_objs_equal_to_cart: HashMap<ObjString, (Cart, LineFile)>

known_objs_equal_to_finite_seq_list: HashMap<ObjString, (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile)>

known_objs_equal_to_matrix_list: HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>

known_objs_equal_to_normalized_decimal_number: HashMap<ObjString, Number>

known_objs_in_fn_sets: HashMap<ObjString, KnownFnInfo>

known_name_belong_to_struct: HashMap<String, StructName>

known_transitive_props: HashMap<String, ()>

known_commutative_props: HashMap<String, CommutativePropValue>

cache_well_defined_obj: HashMap<ObjString, ()>

cache_known_fact: HashMap<FactString, LineFile>

Implementations

impl Environment

pub fn new( objs: HashMap<IdentifierName, ParamObjType>, def_props: HashMap<PropName, DefPropStmt>, families: HashMap<FamilyName, DefFamilyStmt>, abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>, algorithms: HashMap<AlgoName, DefAlgoStmt>, structs: HashMap<StructName, DefStructStmt>, known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>, known_fn_in_fn_set: HashMap<ObjString, KnownFnInfo>, known_atomic_facts_with_0_or_more_than_2_args: HashMap<(AtomicFactKey, bool), Vec<AtomicFact>>, known_atomic_facts_with_1_arg: HashMap<(AtomicFactKey, bool), HashMap<ObjString, AtomicFact>>, known_atomic_facts_with_2_args: HashMap<(AtomicFactKey, bool), HashMap<(ObjString, ObjString), AtomicFact>>, known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>, known_atomic_facts_in_forall_facts: HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>, known_exist_facts_in_forall_facts: HashMap<ExistFactKey, Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>>, known_or_facts: HashMap<OrFactKey, Vec<OrFact>>, known_or_facts_in_forall_facts: HashMap<OrFactKey, Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>>, known_tuple_objs: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>, known_cart_objs: HashMap<ObjString, (Cart, LineFile)>, known_finite_seq_list_objs: HashMap<ObjString, (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile)>, known_matrix_list_objs: HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>, known_calculated_value_of_obj: HashMap<ObjString, Number>, known_name_belong_to_struct: HashMap<String, StructName>, cache_known_valid_obj: HashMap<ObjString, ()>, cache_known_fact: HashMap<FactString, LineFile>, ) -> Self

impl Environment

pub fn store_atomic_fact_by_ref( &mut self, atomic_fact: &AtomicFact, ) -> Result<(), RuntimeError>

pub fn store_atomic_fact( &mut self, atomic_fact: AtomicFact, ) -> Result<(), RuntimeError>

pub fn store_fact(&mut self, fact: Fact) -> Result<(), RuntimeError>

pub fn store_exist_fact_by_ref( &mut self, exist_fact: &ExistFactEnum, ) -> Result<(), RuntimeError>

pub fn store_exist_or_and_chain_atomic_fact( &mut self, fact: ExistOrAndChainAtomicFact, ) -> Result<(), RuntimeError>

pub fn store_and_chain_atomic_fact( &mut self, and_chain_atomic_fact: AndChainAtomicFact, ) -> Result<(), RuntimeError>

pub fn store_or_and_chain_atomic_fact( &mut self, fact: OrAndChainAtomicFact, ) -> Result<(), RuntimeError>

pub fn store_chain_fact_by_ref( &mut self, chain_fact: &ChainFact, ) -> Result<(), RuntimeError>

pub fn store_equality( &mut self, equality: &EqualFact, ) -> Result<(), RuntimeError>

impl Environment

pub fn new_empty_env() -> Self

impl Environment

pub fn store_transitive_prop_name(&mut self, prop_name: String)

pub fn store_commutative_prop_permutation( &mut self, prop_name: String, gather: Vec<usize>, line_file: LineFile, ) -> Result<(), RuntimeError>

impl Environment

pub fn store_fact_to_cache_known_fact( &mut self, fact_key: FactString, fact_line_file: LineFile, ) -> Result<(), RuntimeError>

Trait Implementations

impl Display for Environment

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

Formats the value using the given formatter.