chc.invariants.CInvariantFact module

Base class and subclasses

chc.invariants.CInvariantFact.CInvariantFact(...)
chc.invariants.CInvariantFact.CInvariantNRVFact(...)	Non-relational-value fact (relation with symbolic constants).
chc.invariants.CInvariantFact.CParameterConstraint(...)
chc.invariants.CInvariantFact.CUnreachableFact(...)	Domain that signals unreachability.

Different types of invariants.

class chc.invariants.CInvariantFact.CInvariantFact(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)

Bases: chc.invariants.CFunDictionaryRecord.CFunInvDictionaryRecord

property is_nrv_fact: bool

property is_unreachable_fact: bool

class chc.invariants.CInvariantFact.CInvariantNRVFact(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)

Bases: chc.invariants.CInvariantFact.CInvariantFact

Non-relational-value fact (relation with symbolic constants).

property is_nrv_fact: bool

property non_relational_value: CNonRelationalValue

property variable: CXVariable

class chc.invariants.CInvariantFact.CParameterConstraint(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)

Bases: chc.invariants.CInvariantFact.CInvariantFact

property xpr: CXXpr

class chc.invariants.CInvariantFact.CUnreachableFact(invd: CFunInvDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)

Bases: chc.invariants.CInvariantFact.CInvariantFact

Domain that signals unreachability.

property domain: str

property is_unreachable_fact: bool