inter_ila_unroller.h File Reference

#include <functional>
#include <list>
#include <set>
#include <stack>
#include <vector>
#include <z3++.h>
#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/mcm/memory_model.h>

Go to the source code of this file.

Classes
class	ilang::InterIlaUnroller
	Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered. Ordered unrolling assumes an ordered program template, despite that some may not exist in the final outcome. By default the state with the same name among ILAs is considered as the same shared state. More...
class	ilang::HostRemoveRestore
	Class to remove and restore the host info This is useful as we want the ast with the same name generates the same z3 expr. This framework is based on an assumption that if we call z3 to create the variable of the same name multiple times they refer to the same one internally. FIXME: Need to check this assumption if we want to support other SMT solvers! More...

Namespaces
	ilang

Detailed Description

Header for multi-ILA unroller