ilang
1.1.4
ILAng: A Modeling and Verification Platform for SoCs
Main Page
Namespaces
Classes
Files
File List
File Members
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Friends
Macros
include
ilang
mcm
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__
ilang::Z3And
z3::expr Z3And(const z3::expr &a, const z3::expr &b)
This is just a shortcut to be used for generated axiom.
Generated by
1.8.5