ilang  1.1.4
ILAng: A Modeling and Verification Platform for SoCs
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Friends Macros
axiom_helper.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_MCM_AXIOM_HELPER_H__
5 #define ILANG_MCM_AXIOM_HELPER_H__
6 
8 namespace ilang {
9 
10 /******************************************************************************/
11 // Helper Functions
12 /******************************************************************************/
13 
14 #if 0
15 z3::expr Z3ForallList(const std::vector<z3::expr> & l); // move into mcm class
18 z3::expr Z3ExistsList(const std::vector<z3::expr> & l);
19 #endif
20 
22 z3::expr Z3And(const z3::expr& a, const z3::expr& b);
23 
24 } // namespace ilang
25 
26 #endif // ILANG_MCM_AXIOM_HELPER_H__
z3::expr Z3And(const z3::expr &a, const z3::expr &b)
This is just a shortcut to be used for generated axiom.