ilasynth  1.0
ILASynth: Template-based ILA Synthesis Engine
Public Member Functions | Static Public Member Functions | Public Attributes | Private Member Functions | Static Private Member Functions | Private Attributes | Static Private Attributes | List of all members
ilasynth::MicroUnroller Class Reference

#include <MicroUnroller.hpp>

Public Member Functions

 MicroUnroller (const char *suffix, Abstraction &abs, Abstraction &uabs, z3::context &c, z3::solver &s, bool InitCond)
 
 ~MicroUnroller ()
 
void reset (z3::solver *solver)
 
void addAssump (z3::expr &a)
 register literal as an assumption More...
 
std::vector< z3::expr > & getAssumps ()
 return all assumptions More...
 
unsigned frame ()
 
void newFrame ()
 
unsigned frames ()
 
unsigned addPrimaryInput (z3::expr in)
 
z3::expr & getPrimaryInput (int nNum)
 
z3::expr & getPrimaryInput (Node *var)
 
std::vector< z3::expr > & getPrimaryInputs ()
 
unsigned addOutput (z3::expr out)
 
z3::expr & getOutput (Node *var)
 
z3::expr & getOutput (unsigned nFrame, Node *var)
 
z3::expr & getOutput (unsigned nFrame, int nNum)
 
std::vector< z3::expr > & getOutputs (unsigned nFrame)
 
std::vector< std::vector< z3::expr > > & getAllOutputs ()
 
bool checkAssertion (NodeRef *assertion)
 
void dumpAssertion (NodeRef *assertion, const std::string &fileName)
 
void addAssumption (NodeRef *assumption)
 
z3::expr subsFormulaOnFrame (unsigned nframe, nptr_t &formula)
 
z3::expr getNodeOnFrame (unsigned nframe, nptr_t &node)
 
void unrollToStep (unsigned bound)
 
void InsertAssumptions ()
 
void InsertAssumptSub (z3::expr_vector &src, z3::expr_vector &dest)
 

Static Public Member Functions

static MicroUnroller * NewUnroller (AbstractionWrapper *Abs, AbstractionWrapper *Uabs, bool InitCond)
 
static void EqOffline (const std::string &fileName, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2)
 
static void EqOffline (const std::string &fileName, MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps)
 
static bool EqCheck (MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2)
 
static bool EqCheck (MicroUnroller *m1, MicroUnroller *m2, const std::string &n1, const std::string &n2, py::list &assumps)
 

Public Attributes

bool debug
 

Private Member Functions

void setup2Frames (bool initCond)
 
void _initVar (Z3ExprAdapter &z3expr, const npair_t &p, bool allowInit)
 
void addInputNodes ()
 
void addArchStatesToFirstFrame ()
 
void addAllStatesToSecondFrame (bool initCondSet)
 
void addAllStatesToLaterFrame ()
 
z3::expr subsFormula (Node *n)
 
void debugFrame ()
 

Static Private Member Functions

static std::string frame2suffix (unsigned fr, bool init=false)
 
static void EvalEachFrame (z3::model &m, MicroUnroller *u, std::ostream &cexf)
 
static bool checkMiter (z3::solver &S, z3::expr &e1, z3::expr &e2, MicroUnroller *u1, MicroUnroller *u2)
 

Private Attributes

std::string m_sName
 
Abstraction * m_pAbstraction
 
Abstraction * m_pUAbstraction
 
z3::context * m_pContext
 
z3::solver * m_pSolver
 
unsigned m_nFrames
 
std::unordered_map< Node *, int, decltype(&nodeHash), decltype(&nodeEqual)> m_mInputIndices
 Map between primary input pointers and indices into m_vPrimaryInputs. More...
 
std::vector< z3::expr > m_vPrimaryInputs
 Primary Inputs, by frame. More...
 
std::unordered_map< Node *, unsigned, decltype(&nodeHash), decltype(&nodeEqual)> m_mStateIndices
 Map between state pointers and indices into m_vOutputs. More...
 
std::vector< std::vector< z3::expr > > m_vOutputs
 Outputs, by frame. More...
 
std::vector< z3::expr > m_Assumps
 All assumptions. More...
 

Static Private Attributes

static z3::context MicroUnrollContext
 
static z3::solver MicroUnrollSolver
 

Constructor & Destructor Documentation

◆ MicroUnroller()

ilasynth::MicroUnroller::MicroUnroller ( const char *  suffix,
Abstraction &  abs,
Abstraction &  uabs,
z3::context &  c,
z3::solver &  s,
bool  InitCond 
)
inline

◆ ~MicroUnroller()

ilasynth::MicroUnroller::~MicroUnroller ( )
inline

Member Function Documentation

◆ _initVar()

void ilasynth::MicroUnroller::_initVar ( Z3ExprAdapter &  z3expr,
const npair_t &  p,
bool  allowInit 
)
private

◆ addAllStatesToLaterFrame()

void ilasynth::MicroUnroller::addAllStatesToLaterFrame ( )
private

◆ addAllStatesToSecondFrame()

void ilasynth::MicroUnroller::addAllStatesToSecondFrame ( bool  initCondSet)
private

◆ addArchStatesToFirstFrame()

void ilasynth::MicroUnroller::addArchStatesToFirstFrame ( )
private

◆ addAssump()

void ilasynth::MicroUnroller::addAssump ( z3::expr &  a)
inline

register literal as an assumption

◆ addAssumption()

void ilasynth::MicroUnroller::addAssumption ( NodeRef *  assumption)

◆ addInputNodes()

void ilasynth::MicroUnroller::addInputNodes ( )
private

◆ addOutput()

unsigned ilasynth::MicroUnroller::addOutput ( z3::expr  out)
inline

◆ addPrimaryInput()

unsigned ilasynth::MicroUnroller::addPrimaryInput ( z3::expr  in)
inline

◆ checkAssertion()

bool ilasynth::MicroUnroller::checkAssertion ( NodeRef *  assertion)

◆ checkMiter()

static bool ilasynth::MicroUnroller::checkMiter ( z3::solver &  S,
z3::expr &  e1,
z3::expr &  e2,
MicroUnroller *  u1,
MicroUnroller *  u2 
)
staticprivate

◆ debugFrame()

void ilasynth::MicroUnroller::debugFrame ( )
private

◆ dumpAssertion()

void ilasynth::MicroUnroller::dumpAssertion ( NodeRef *  assertion,
const std::string &  fileName 
)

◆ EqCheck() [1/2]

static bool ilasynth::MicroUnroller::EqCheck ( MicroUnroller *  m1,
MicroUnroller *  m2,
const std::string &  n1,
const std::string &  n2 
)
static

◆ EqCheck() [2/2]

static bool ilasynth::MicroUnroller::EqCheck ( MicroUnroller *  m1,
MicroUnroller *  m2,
const std::string &  n1,
const std::string &  n2,
py::list &  assumps 
)
static

◆ EqOffline() [1/2]

static void ilasynth::MicroUnroller::EqOffline ( const std::string &  fileName,
MicroUnroller *  m1,
MicroUnroller *  m2,
const std::string &  n1,
const std::string &  n2 
)
static

◆ EqOffline() [2/2]

static void ilasynth::MicroUnroller::EqOffline ( const std::string &  fileName,
MicroUnroller *  m1,
MicroUnroller *  m2,
const std::string &  n1,
const std::string &  n2,
py::list &  assumps 
)
static

◆ EvalEachFrame()

static void ilasynth::MicroUnroller::EvalEachFrame ( z3::model &  m,
MicroUnroller *  u,
std::ostream &  cexf 
)
staticprivate

◆ frame()

unsigned ilasynth::MicroUnroller::frame ( )
inline

◆ frame2suffix()

static std::string ilasynth::MicroUnroller::frame2suffix ( unsigned  fr,
bool  init = false 
)
staticprivate

◆ frames()

unsigned ilasynth::MicroUnroller::frames ( )
inline

◆ getAllOutputs()

std::vector<std::vector<z3::expr> >& ilasynth::MicroUnroller::getAllOutputs ( )
inline

◆ getAssumps()

std::vector<z3::expr>& ilasynth::MicroUnroller::getAssumps ( )
inline

return all assumptions

◆ getNodeOnFrame()

z3::expr ilasynth::MicroUnroller::getNodeOnFrame ( unsigned  nframe,
nptr_t &  node 
)

◆ getOutput() [1/3]

z3::expr& ilasynth::MicroUnroller::getOutput ( Node *  var)
inline

◆ getOutput() [2/3]

z3::expr& ilasynth::MicroUnroller::getOutput ( unsigned  nFrame,
Node *  var 
)
inline

◆ getOutput() [3/3]

z3::expr& ilasynth::MicroUnroller::getOutput ( unsigned  nFrame,
int  nNum 
)
inline

◆ getOutputs()

std::vector<z3::expr>& ilasynth::MicroUnroller::getOutputs ( unsigned  nFrame)
inline

◆ getPrimaryInput() [1/2]

z3::expr& ilasynth::MicroUnroller::getPrimaryInput ( int  nNum)
inline

◆ getPrimaryInput() [2/2]

z3::expr& ilasynth::MicroUnroller::getPrimaryInput ( Node *  var)
inline

◆ getPrimaryInputs()

std::vector<z3::expr>& ilasynth::MicroUnroller::getPrimaryInputs ( )
inline

◆ InsertAssumptions()

void ilasynth::MicroUnroller::InsertAssumptions ( )

◆ InsertAssumptSub()

void ilasynth::MicroUnroller::InsertAssumptSub ( z3::expr_vector &  src,
z3::expr_vector &  dest 
)

◆ newFrame()

void ilasynth::MicroUnroller::newFrame ( )
inline

◆ NewUnroller()

static MicroUnroller* ilasynth::MicroUnroller::NewUnroller ( AbstractionWrapper *  Abs,
AbstractionWrapper *  Uabs,
bool  InitCond 
)
static

◆ reset()

void ilasynth::MicroUnroller::reset ( z3::solver *  solver)
inline

Reset everything

◆ setup2Frames()

void ilasynth::MicroUnroller::setup2Frames ( bool  initCond)
private

◆ subsFormula()

z3::expr ilasynth::MicroUnroller::subsFormula ( Node *  n)
private

◆ subsFormulaOnFrame()

z3::expr ilasynth::MicroUnroller::subsFormulaOnFrame ( unsigned  nframe,
nptr_t &  formula 
)

◆ unrollToStep()

void ilasynth::MicroUnroller::unrollToStep ( unsigned  bound)

Member Data Documentation

◆ debug

bool ilasynth::MicroUnroller::debug

◆ m_Assumps

std::vector<z3::expr> ilasynth::MicroUnroller::m_Assumps
private

All assumptions.

◆ m_mInputIndices

std::unordered_map<Node*, int, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::MicroUnroller::m_mInputIndices
private

Map between primary input pointers and indices into m_vPrimaryInputs.

◆ m_mStateIndices

std::unordered_map<Node*, unsigned, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::MicroUnroller::m_mStateIndices
private

Map between state pointers and indices into m_vOutputs.

◆ m_nFrames

unsigned ilasynth::MicroUnroller::m_nFrames
private

◆ m_pAbstraction

Abstraction* ilasynth::MicroUnroller::m_pAbstraction
private

◆ m_pContext

z3::context* ilasynth::MicroUnroller::m_pContext
private

◆ m_pSolver

z3::solver* ilasynth::MicroUnroller::m_pSolver
private

◆ m_pUAbstraction

Abstraction* ilasynth::MicroUnroller::m_pUAbstraction
private

◆ m_sName

std::string ilasynth::MicroUnroller::m_sName
private

◆ m_vOutputs

std::vector<std::vector<z3::expr> > ilasynth::MicroUnroller::m_vOutputs
private

Outputs, by frame.

◆ m_vPrimaryInputs

std::vector<z3::expr> ilasynth::MicroUnroller::m_vPrimaryInputs
private

Primary Inputs, by frame.

◆ MicroUnrollContext

z3::context ilasynth::MicroUnroller::MicroUnrollContext
staticprivate

◆ MicroUnrollSolver

z3::solver ilasynth::MicroUnroller::MicroUnrollSolver
staticprivate
The documentation for this class was generated from the following file:
Generated by   doxygen 1.8.15