chc.proof.CFilePredicateDictionary module

Dictionary for proof obligation predicates.

class chc.proof.CFilePredicateDictionary.CFilePredicateDictionary(cfile: CFile, xnode: Optional[xml.etree.ElementTree.Element])[source]

Bases: object

Dictionary that encodes proof obligation predicates.

property cfile: CFile

property dictionary: CFileDictionary

get_predicate(ix: int) → chc.proof.CPOPredicate.CPOPredicate[source]

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

index_predicate(p: chc.proof.CPOPredicate.CPOPredicate, subst: Dict[int, CExp] = {}) → int[source]

initialize(xnode: Optional[xml.etree.ElementTree.Element], force: bool = False) → None[source]

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

read_xml_predicate(xnode: xml.etree.ElementTree.Element, tag: str = 'ipr') → chc.proof.CPOPredicate.CPOPredicate[source]

write_xml(node: xml.etree.ElementTree.Element) → None[source]

write_xml_predicate(xnode: xml.etree.ElementTree.Element, pred: chc.proof.CPOPredicate.CPOPredicate, tag: str = 'ipr') → None[source]