| abs | ilasynth::AbstractionWrapper | |
| AbstractionWrapper(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| AbstractionWrapper(Abstraction *parent, const std::string &name) | ilasynth::AbstractionWrapper | inline |
| AbstractionWrapper(const abstraction_ptr_t &a) | ilasynth::AbstractionWrapper | inline |
| addAssumption(NodeRef *expr) | ilasynth::AbstractionWrapper | inline |
| addBit(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| addFun(const std::string &name, int retW, const py::list &l) | ilasynth::AbstractionWrapper | inline |
| addHornChild(const std::string &c, const std::string &i, NodeRef *d) | ilasynth::AbstractionWrapper | inline |
| addHornInstr(const std::string &i, NodeRef *d) | ilasynth::AbstractionWrapper | inline |
| addHornNext(const std::string &i, const std::string &s, NodeRef *n) | ilasynth::AbstractionWrapper | inline |
| addInp(const std::string &name, int width) | ilasynth::AbstractionWrapper | inline |
| addMem(const std::string &name, int addrW, int dataW) | ilasynth::AbstractionWrapper | inline |
| addReg(const std::string &name, int width) | ilasynth::AbstractionWrapper | inline |
| addUAbs(const std::string &name, NodeRef *valid) | ilasynth::AbstractionWrapper | inline |
| areEqual(NodeRef *left, NodeRef *right) const | ilasynth::AbstractionWrapper | inline |
| areEqualAssump(NodeRef *assump, NodeRef *left, NodeRef *right) | ilasynth::AbstractionWrapper | inline |
| areEqualUnrolled(unsigned n, NodeRef *reg, NodeRef *exp) | ilasynth::AbstractionWrapper | inline |
| bmc(unsigned n1, AbstractionWrapper *a1, NodeRef *r1, unsigned n2, AbstractionWrapper *a2, NodeRef *r2) | ilasynth::AbstractionWrapper | inlinestatic |
| bmcCond(NodeRef *assertion, unsigned n, NodeRef *assumpt) | ilasynth::AbstractionWrapper | inline |
| bmcInit(NodeRef *assertion, unsigned n, bool init) | ilasynth::AbstractionWrapper | inline |
| boolConstB(bool b) | ilasynth::AbstractionWrapper | inline |
| boolConstBStatic(bool b) | ilasynth::AbstractionWrapper | inlinestatic |
| boolConstI(int b) | ilasynth::AbstractionWrapper | inline |
| boolConstIStatic(int b) | ilasynth::AbstractionWrapper | inlinestatic |
| boolConstL(py::long_ b) | ilasynth::AbstractionWrapper | inline |
| boolConstLStatic(py::long_ b) | ilasynth::AbstractionWrapper | inlinestatic |
| bvConstInt(unsigned int l, int width) | ilasynth::AbstractionWrapper | inline |
| bvConstIntStatic(unsigned int l, int width) | ilasynth::AbstractionWrapper | inlinestatic |
| bvConstLong(py::long_ l, int width) | ilasynth::AbstractionWrapper | inline |
| bvConstLongStatic(py::long_ l, int width) | ilasynth::AbstractionWrapper | inlinestatic |
| connectUInst(const std::string &name, const AbstractionWrapper *uabs) | ilasynth::AbstractionWrapper | inline |
| EQcheck(MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2) | ilasynth::AbstractionWrapper | inlinestatic |
| EQcheckExport(const std::string &fn, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2) | ilasynth::AbstractionWrapper | inlinestatic |
| EQcheckSimple(AbstractionWrapper *a1, AbstractionWrapper *a2) | ilasynth::AbstractionWrapper | inlinestatic |
| EQcheckWithAssump(MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps) | ilasynth::AbstractionWrapper | inlinestatic |
| EQcheckWithAssumpExport(const std::string &fn, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps) | ilasynth::AbstractionWrapper | inlinestatic |
| exportAllToFile(const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| exportHornToFile(const std::string &fileName) | ilasynth::AbstractionWrapper | inline |
| exportListToFile(const py::list &l, const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| exportOneToFile(NodeRef *node, const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| generateCbmcCtoDir(const std::string &dirName) const | ilasynth::AbstractionWrapper | inline |
| generateCbmcCtoFile(const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| generateHornMapping(const std::string &type) | ilasynth::AbstractionWrapper | inline |
| generateSimToDir(const std::string &dirName) const | ilasynth::AbstractionWrapper | inline |
| generateSimToFile(const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| generateVerilogModule(const std::string &fileName, const std::string &modName) const | ilasynth::AbstractionWrapper | inline |
| generateVerilogToFile(const std::string &fileName) const | ilasynth::AbstractionWrapper | inline |
| getAllAssumptions() const | ilasynth::AbstractionWrapper | inline |
| getBit(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| getBits() const | ilasynth::AbstractionWrapper | inline |
| getDecodeExpressions() const | ilasynth::AbstractionWrapper | inline |
| getEnParamSyn() const | ilasynth::AbstractionWrapper | inline |
| getFetchExpr() const | ilasynth::AbstractionWrapper | inline |
| getFetchValid() const | ilasynth::AbstractionWrapper | inline |
| getFun(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| getFuns() const | ilasynth::AbstractionWrapper | inline |
| getInit(const std::string &name) const | ilasynth::AbstractionWrapper | inline |
| getInp(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| getInps() const | ilasynth::AbstractionWrapper | inline |
| getIpred(const std::string &name) const | ilasynth::AbstractionWrapper | inline |
| getMem(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| getMems() const | ilasynth::AbstractionWrapper | inline |
| getName() const | ilasynth::AbstractionWrapper | inline |
| getNext(const std::string &name) const | ilasynth::AbstractionWrapper | inline |
| getNextI(const std::string &name, int i) const | ilasynth::AbstractionWrapper | inline |
| getReduceWhenImport() const | ilasynth::AbstractionWrapper | inline |
| getReg(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| getRegs() const | ilasynth::AbstractionWrapper | inline |
| getUAbs(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| hornifyAll(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| hornifyBvAsInt(bool bvAsInt) | ilasynth::AbstractionWrapper | inline |
| hornifyIteAsNode(bool iteAsNode) | ilasynth::AbstractionWrapper | inline |
| hornifyNode(NodeRef *node, const std::string &rule) | ilasynth::AbstractionWrapper | inline |
| importAllFromFile(const std::string &fileName) | ilasynth::AbstractionWrapper | inline |
| importListFromFile(const std::string &fileName) | ilasynth::AbstractionWrapper | inline |
| importOneFromFile(const std::string &fileName) | ilasynth::AbstractionWrapper | inline |
| memConst(const MemValues &mv) | ilasynth::AbstractionWrapper | inline |
| memConstStatic(const MemValues &mv) | ilasynth::AbstractionWrapper | inlinestatic |
| newUnroller(AbstractionWrapper *uILA, bool initCondition) | ilasynth::AbstractionWrapper | inline |
| setDecodeExpressions(const py::list &l) | ilasynth::AbstractionWrapper | inline |
| setEnParamSyn(int en) | ilasynth::AbstractionWrapper | inline |
| setFetchExpr(NodeRef *expr) | ilasynth::AbstractionWrapper | inline |
| setFetchValid(NodeRef *expr) | ilasynth::AbstractionWrapper | inline |
| setInit(const std::string &name, NodeRef *n) | ilasynth::AbstractionWrapper | inline |
| setIpred(const std::string &name, NodeRef *n) | ilasynth::AbstractionWrapper | inline |
| setNext(const std::string &name, NodeRef *n) | ilasynth::AbstractionWrapper | inline |
| setReduceWhenImport(int en) | ilasynth::AbstractionWrapper | inline |
| setVlgExpConfig(bool extMem, bool fAsM) | ilasynth::AbstractionWrapper | inline |
| synthesizeAll(PyObject *fun) | ilasynth::AbstractionWrapper | inline |
| synthesizeElement(const std::string &name, NodeRef *expr, PyObject *fun) | ilasynth::AbstractionWrapper | inline |
| synthesizeReg(const std::string &name, PyObject *fun) | ilasynth::AbstractionWrapper | inline |
| toBoogie(const std::string &name) | ilasynth::AbstractionWrapper | inline |
| ~AbstractionWrapper() | ilasynth::AbstractionWrapper | inline |
