chc.invariants.CFunInvDictionary module

Dictionary of indexed function invariants.

class chc.invariants.CFunInvDictionary.CFunInvDictionary(cfun: CFunction, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

Indexed function invariants.

property cfile: CFile

property cfun: CFunction

get_invariant_fact(ix: int) → chc.invariants.CInvariantFact.CInvariantFact[source]

get_invariant_fact_map() → Dict[int, chc.util.IndexedTable.IndexedTableValue][source]

get_non_relational_value(ix: int) → chc.invariants.CNonRelationalValue.CNonRelationalValue[source]

get_non_relational_value_map() → Dict[int, chc.util.IndexedTable.IndexedTableValue][source]

initialize(xnode: xml.etree.ElementTree.Element) → None[source]

objectmap_to_string(name: str) → str[source]

property vd: CFunVarDictionary

property xd: CFunXprDictionary