reset Z3 memory state after every transformation
gives a ~4x speedup
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -280,12 +280,12 @@ expr Select::getTypeConstraints(const Function &f) const {
ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
: Instr(type, move(name)), a(a), b(b), cond(cond), defined(cond != Any) {
- if (!defined) {
- auto str = getName() + "_cond" + fresh_id();
- cond_var = expr::mkVar(str.c_str(), 4);
- } else {
- cond_var = expr::mkUInt(cond, 4);
+ if (!defined)
+ cond_name = getName() + "_cond" + fresh_id();
}
+
+expr ICmp::cond_var() const {
+ return defined ? expr::mkUInt(cond, 4) : expr::mkVar(cond_name.c_str(), 4);
}
void ICmp::print(ostream &os) const {
@@ -334,21 +334,21 @@ expr ICmp::getTypeConstraints(const Function &f) const {
a.getType().enforceIntOrPtrOrVectorType() &&
a.getType() == b.getType();
if (!defined)
- e &= cond_var.ule(expr::mkUInt(9, 4));
+ e &= cond_var().ule(expr::mkUInt(9, 4));
return e;
}
void ICmp::fixupTypes(const Model &m) {
Value::fixupTypes(m);
if (!defined)
- cond = (Cond)m.getUInt(cond_var);
+ cond = (Cond)m.getUInt(cond_var());
}
expr ICmp::eqType(const Instr &i) const {
expr eq = Instr::eqType(i);
if (auto rhs = dynamic_cast<const ICmp*>(&i)) {
if (!defined || !rhs->defined) {
- eq &= cond_var == rhs->cond_var;
+ eq &= cond_var() == rhs->cond_var();
}
}
return eq;

MODIFY
ir/instr.h
ir/instr.h
@@ -77,9 +77,10 @@ public:
private:
Value &a, &b;
- smt::expr cond_var;
+ std::string cond_name;
Cond cond;
bool defined;
+ smt::expr cond_var() const;
public:
ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b);

MODIFY
smt/smt.cpp
smt/smt.cpp
namespace smt {
smt_initializer::smt_initializer() {
+ init();
+}
+
+void smt_initializer::reset() {
+ destroy();
+ Z3_reset_memory();
+ init();
+}
+
+smt_initializer::~smt_initializer() {
+ destroy();
+ Z3_finalize_memory();
+}
+
+void smt_initializer::init() {
ctx.init();
solver_init();
}
-smt_initializer::~smt_initializer() {
+void smt_initializer::destroy() {
solver_destroy();
ctx.destroy();
- Z3_finalize_memory();
}

MODIFY
smt/smt.h
smt/smt.h
@@ -8,6 +8,11 @@ namespace smt {
struct smt_initializer {
smt_initializer();
~smt_initializer();
+ void reset();
+
+private:
+ void init();
+ void destroy();
};

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -85,8 +85,8 @@ int main(int argc, char **argv) {
for (; argc_i < argc; ++argc_i) {
cout << "Processing " << argv[argc_i] << "..\n";
try {
- file_reader f(argv[argc_i], PARSER_READ_AHEAD);
- for (auto &t : parse(*f)) {
+ for (auto &t : parse(*file_reader(argv[argc_i], PARSER_READ_AHEAD))) {
+ smt_init.reset();
t.print(cout, print_opts);
cout << '\n';

reset Z3 memory state after every transformation
gives a ~4x speedup