| _initVar(Z3ExprAdapter &z3expr, const npair_t &p, bool allowInit) | ilasynth::MicroUnroller | private |
| addAllStatesToLaterFrame() | ilasynth::MicroUnroller | private |
| addAllStatesToSecondFrame(bool initCondSet) | ilasynth::MicroUnroller | private |
| addArchStatesToFirstFrame() | ilasynth::MicroUnroller | private |
| addAssump(z3::expr &a) | ilasynth::MicroUnroller | inline |
| addAssumption(NodeRef *assumption) | ilasynth::MicroUnroller | |
| addInputNodes() | ilasynth::MicroUnroller | private |
| addOutput(z3::expr out) | ilasynth::MicroUnroller | inline |
| addPrimaryInput(z3::expr in) | ilasynth::MicroUnroller | inline |
| checkAssertion(NodeRef *assertion) | ilasynth::MicroUnroller | |
| checkMiter(z3::solver &S, z3::expr &e1, z3::expr &e2, MicroUnroller *u1, MicroUnroller *u2) | ilasynth::MicroUnroller | privatestatic |
| debug | ilasynth::MicroUnroller | |
| debugFrame() | ilasynth::MicroUnroller | private |
| dumpAssertion(NodeRef *assertion, const std::string &fileName) | ilasynth::MicroUnroller | |
| EqCheck(MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2) | ilasynth::MicroUnroller | static |
| EqCheck(MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps) | ilasynth::MicroUnroller | static |
| EqOffline(const std::string &fileName, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2) | ilasynth::MicroUnroller | static |
| EqOffline(const std::string &fileName, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps) | ilasynth::MicroUnroller | static |
| EvalEachFrame(z3::model &m, MicroUnroller *u, std::ostream &cexf) | ilasynth::MicroUnroller | privatestatic |
| frame() | ilasynth::MicroUnroller | inline |
| frame2suffix(unsigned fr, bool init=false) | ilasynth::MicroUnroller | privatestatic |
| frames() | ilasynth::MicroUnroller | inline |
| getAllOutputs() | ilasynth::MicroUnroller | inline |
| getAssumps() | ilasynth::MicroUnroller | inline |
| getNodeOnFrame(unsigned nframe, nptr_t &node) | ilasynth::MicroUnroller | |
| getOutput(Node *var) | ilasynth::MicroUnroller | inline |
| getOutput(unsigned nFrame, Node *var) | ilasynth::MicroUnroller | inline |
| getOutput(unsigned nFrame, int nNum) | ilasynth::MicroUnroller | inline |
| getOutputs(unsigned nFrame) | ilasynth::MicroUnroller | inline |
| getPrimaryInput(int nNum) | ilasynth::MicroUnroller | inline |
| getPrimaryInput(Node *var) | ilasynth::MicroUnroller | inline |
| getPrimaryInputs() | ilasynth::MicroUnroller | inline |
| InsertAssumptions() | ilasynth::MicroUnroller | |
| InsertAssumptSub(z3::expr_vector &src, z3::expr_vector &dest) | ilasynth::MicroUnroller | |
| m_Assumps | ilasynth::MicroUnroller | private |
| m_mInputIndices | ilasynth::MicroUnroller | private |
| m_mStateIndices | ilasynth::MicroUnroller | private |
| m_nFrames | ilasynth::MicroUnroller | private |
| m_pAbstraction | ilasynth::MicroUnroller | private |
| m_pContext | ilasynth::MicroUnroller | private |
| m_pSolver | ilasynth::MicroUnroller | private |
| m_pUAbstraction | ilasynth::MicroUnroller | private |
| m_sName | ilasynth::MicroUnroller | private |
| m_vOutputs | ilasynth::MicroUnroller | private |
| m_vPrimaryInputs | ilasynth::MicroUnroller | private |
| MicroUnrollContext | ilasynth::MicroUnroller | privatestatic |
| MicroUnroller(const char *suffix, Abstraction &abs, Abstraction &uabs, z3::context &c, z3::solver &s, bool InitCond) | ilasynth::MicroUnroller | inline |
| MicroUnrollSolver | ilasynth::MicroUnroller | privatestatic |
| newFrame() | ilasynth::MicroUnroller | inline |
| NewUnroller(AbstractionWrapper *Abs, AbstractionWrapper *Uabs, bool InitCond) | ilasynth::MicroUnroller | static |
| reset(z3::solver *solver) | ilasynth::MicroUnroller | inline |
| setup2Frames(bool initCond) | ilasynth::MicroUnroller | private |
| subsFormula(Node *n) | ilasynth::MicroUnroller | private |
| subsFormulaOnFrame(unsigned nframe, nptr_t &formula) | ilasynth::MicroUnroller | |
| unrollToStep(unsigned bound) | ilasynth::MicroUnroller | |
| ~MicroUnroller() | ilasynth::MicroUnroller | inline |
