From 564f64c6850aed39c8090f5b3dae865bafb7718d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 15 Jul 2017 15:23:11 +0100 Subject: [PATCH 1/2] added a non-recursive variant of APPLY --- src/solvers/miniBDD/miniBDD.cpp | 120 +++++++++++++++++++++++++++++--- 1 file changed, 111 insertions(+), 9 deletions(-) diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index d32330a0995..fc47235b076 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -194,18 +194,19 @@ class mini_bdd_applyt mini_bddt operator()(const mini_bddt &x, const mini_bddt &y) { - return APP(x, y); + return APP_non_rec(x, y); } protected: bool (*fkt)(bool, bool); - mini_bddt APP(const mini_bddt &x, const mini_bddt &y); + mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y); + mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y); typedef std::map, mini_bddt> Gt; Gt G; }; -mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y) +mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y) { assert(x.is_initialized() && y.is_initialized()); assert(x.node->mgr==y.node->mgr); @@ -224,22 +225,123 @@ mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y) u=mini_bddt(fkt(x.is_true(), y.is_true())?mgr->True():mgr->False()); else if(x.var()==y.var()) u=mgr->mk(x.var(), - APP(x.low(), y.low()), - APP(x.high(), y.high())); + APP_rec(x.low(), y.low()), + APP_rec(x.high(), y.high())); else if(x.var()mk(x.var(), - APP(x.low(), y), - APP(x.high(), y)); + APP_rec(x.low(), y), + APP_rec(x.high(), y)); else /* x.var() > y.var() */ u=mgr->mk(y.var(), - APP(x, y.low()), - APP(x, y.high())); + APP_rec(x, y.low()), + APP_rec(x, y.high())); G[key]=u; return u; } +mini_bddt mini_bdd_applyt::APP_non_rec( + const mini_bddt &_x, + const mini_bddt &_y) +{ + struct stack_elementt + { + stack_elementt( + mini_bddt &_result, + const mini_bddt &_x, + const mini_bddt &_y): + result(_result), x(_x), y(_y), + key(x.node_number(), y.node_number()), + var(0), phase(phaset::INIT) { } + mini_bddt &result, x, y, lr, hr; + std::pair key; + unsigned var; + enum class phaset { INIT, FINISH } phase; + }; + + mini_bddt u; // return value + + std::stack stack; + stack.push(stack_elementt(u, _x, _y)); + + while(!stack.empty()) + { + auto &t=stack.top(); + const mini_bddt &x=t.x; + const mini_bddt &y=t.y; + assert(x.is_initialized() && y.is_initialized()); + assert(x.node->mgr==y.node->mgr); + + switch(t.phase) + { + case stack_elementt::phaset::INIT: + { + // dynamic programming + Gt::const_iterator G_it=G.find(t.key); + if(G_it!=G.end()) + { + t.result=G_it->second; + stack.pop(); + } + else + { + if(x.is_constant() && y.is_constant()) + { + bool result_truth=fkt(x.is_true(), y.is_true()); + const mini_bdd_mgrt &mgr=*x.node->mgr; + t.result=result_truth?mgr.True():mgr.False(); + stack.pop(); + } + else if(x.var()==y.var()) + { + t.var=x.var(); + t.phase=stack_elementt::phaset::FINISH; + assert(x.low().var()>t.var); + assert(y.low().var()>t.var); + assert(x.high().var()>t.var); + assert(y.high().var()>t.var); + stack.push(stack_elementt(t.lr, x.low(), y.low())); + stack.push(stack_elementt(t.hr, x.high(), y.high())); + } + else if(x.var()t.var); + assert(x.high().var()>t.var); + stack.push(stack_elementt(t.lr, x.low(), y)); + stack.push(stack_elementt(t.hr, x.high(), y)); + } + else /* x.var() > y.var() */ + { + t.var=y.var(); + t.phase=stack_elementt::phaset::FINISH; + assert(y.low().var()>t.var); + assert(y.high().var()>t.var); + stack.push(stack_elementt(t.lr, x, y.low())); + stack.push(stack_elementt(t.hr, x, y.high())); + } + } + } + break; + + case stack_elementt::phaset::FINISH: + { + mini_bdd_mgrt *mgr=x.node->mgr; + t.result=mgr->mk(t.var, t.lr, t.hr); + G[t.key]=t.result; + stack.pop(); + } + break; + } + } + + assert(u.is_initialized()); + + return u; +} + bool equal_fkt(bool x, bool y) { return x==y; From a71ca413f8ae145161911ce939dd6b31a8c57b7b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 20 Jul 2017 22:29:42 +0100 Subject: [PATCH 2/2] disable linter for assertions --- src/solvers/miniBDD/miniBDD.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index fc47235b076..aebe4e0a3a4 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com void mini_bdd_nodet::remove_reference() { + // NOLINTNEXTLINE(build/deprecated) assert(reference_counter!=0); reference_counter--; @@ -208,7 +209,9 @@ class mini_bdd_applyt mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y) { + // NOLINTNEXTLINE(build/deprecated) assert(x.is_initialized() && y.is_initialized()); + // NOLINTNEXTLINE(build/deprecated) assert(x.node->mgr==y.node->mgr); // dynamic programming @@ -270,7 +273,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( auto &t=stack.top(); const mini_bddt &x=t.x; const mini_bddt &y=t.y; + // NOLINTNEXTLINE(build/deprecated) assert(x.is_initialized() && y.is_initialized()); + // NOLINTNEXTLINE(build/deprecated) assert(x.node->mgr==y.node->mgr); switch(t.phase) @@ -297,9 +302,13 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=x.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(x.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(x.high().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.high().var()>t.var); stack.push(stack_elementt(t.lr, x.low(), y.low())); stack.push(stack_elementt(t.hr, x.high(), y.high())); @@ -308,7 +317,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=x.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(x.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(x.high().var()>t.var); stack.push(stack_elementt(t.lr, x.low(), y)); stack.push(stack_elementt(t.hr, x.high(), y)); @@ -317,7 +328,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec( { t.var=y.var(); t.phase=stack_elementt::phaset::FINISH; + // NOLINTNEXTLINE(build/deprecated) assert(y.low().var()>t.var); + // NOLINTNEXTLINE(build/deprecated) assert(y.high().var()>t.var); stack.push(stack_elementt(t.lr, x, y.low())); stack.push(stack_elementt(t.hr, x, y.high())); @@ -337,6 +350,7 @@ mini_bddt mini_bdd_applyt::APP_non_rec( } } + // NOLINTNEXTLINE(build/deprecated) assert(u.is_initialized()); return u; @@ -364,6 +378,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const mini_bddt mini_bddt::operator!() const { + // NOLINTNEXTLINE(build/deprecated) assert(is_initialized()); return node->mgr->True()^*this; } @@ -406,8 +421,11 @@ mini_bddt mini_bdd_mgrt::mk( const mini_bddt &low, const mini_bddt &high) { + // NOLINTNEXTLINE(build/deprecated) assert(var<=var_table.size()); + // NOLINTNEXTLINE(build/deprecated) assert(low.var()>var); + // NOLINTNEXTLINE(build/deprecated) assert(high.var()>var); if(low.node_number()==high.node_number()) @@ -501,6 +519,7 @@ mini_bddt restrictt::RES(const mini_bddt &u) { // replace 'var' in 'u' by constant 'value' + // NOLINTNEXTLINE(build/deprecated) assert(u.is_initialized()); mini_bdd_mgrt *mgr=u.node->mgr;