Skip to main content

Environment

litex::environment

Struct Environment 

Source 
pub struct Environment {
Show 24 fields
    pub defined_identifiers: HashMap<IdentifierName, ()>,
    pub defined_def_props: HashMap<PropName, DefPropStmt>,
    pub defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
    pub defined_structs: HashMap<StructName, DefStructStmt>,
    pub defined_families: HashMap<FamilyName, DefFamilyStmt>,
    pub defined_algorithms: HashMap<AlgoName, DefAlgoStmt>,
    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<ExistFact>>,
    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<(ExistFact, 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_identifier_satisfy_struct: HashMap<FieldAccessName, StructObj>,
    pub known_objs_in_fn_sets: HashMap<ObjString, FnSet>,
    pub cache_well_defined_obj: HashMap<ObjString, ()>,
    pub cache_known_fact: HashMap<FactString, LineFile>,

}

Fields§

§defined_identifiers: HashMap<IdentifierName, ()>§defined_def_props: HashMap<PropName, DefPropStmt>§defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>§defined_structs: HashMap<StructName, DefStructStmt>§defined_families: HashMap<FamilyName, DefFamilyStmt>§defined_algorithms: HashMap<AlgoName, DefAlgoStmt>§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<ExistFact>>§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<(ExistFact, 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_identifier_satisfy_struct: HashMap<FieldAccessName, StructObj>§known_objs_in_fn_sets: HashMap<ObjString, FnSet>§cache_well_defined_obj: HashMap<ObjString, ()>§cache_known_fact: HashMap<FactString, LineFile>

Implementations§

Source§

impl Environment

Source

pub fn new( objs: HashMap<IdentifierName, ()>, def_props: HashMap<PropName, DefPropStmt>, struct_defs: HashMap<StructName, DefStructStmt>, families: HashMap<FamilyName, DefFamilyStmt>, abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>, algorithms: HashMap<AlgoName, DefAlgoStmt>, field_access_name: HashMap<FieldAccessName, StructObj>, known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>, known_fn_in_fn_set: HashMap<ObjString, FnSet>, 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<ExistFact>>, known_atomic_facts_in_forall_facts: HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>, known_exist_facts_in_forall_facts: HashMap<ExistFactKey, Vec<(ExistFact, 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>, cache_known_valid_obj: HashMap<ObjString, ()>, cache_known_fact: HashMap<FactString, LineFile>, ) -> Self

Source§

impl Environment

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source§

impl Environment

Source

pub fn new_empty_env() -> Self

Source§

impl Environment

Source

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

Trait Implementations§

Source§

impl Display for Environment

Source§

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

Formats the value using the given formatter. Read more

Auto Trait Implementations§

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToString for T
where T: Display + ?Sized,

Source§

fn to_string(&self) -> String

Converts the given value to a String. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.