tame exponential explosion in AndExpr
uncommon, but exists in some unit tests
MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -11,27 +11,27 @@ using namespace std;
namespace smt {
-void AndExpr::add(const expr &e) {
+void AndExpr::add(const expr &e, unsigned limit) {
if (e.isTrue())
return;
expr a, b;
- if (e.isAnd(a, b)) {
- add(move(a));
- add(move(b));
+ if (limit > 0 && e.isAnd(a, b)) {
+ add(move(a), limit-1);
+ add(move(b), limit-1);
return;
}
exprs.insert(e);
}
-void AndExpr::add(expr &&e) {
+void AndExpr::add(expr &&e, unsigned limit) {
if (e.isTrue())
return;
expr a, b;
- if (e.isAnd(a, b)) {
- add(move(a));
- add(move(b));
+ if (limit > 0 && e.isAnd(a, b)) {
+ add(move(a), limit-1);
+ add(move(b), limit-1);
return;
}
exprs.insert(move(e));

MODIFY
smt/exprs.h
smt/exprs.h
@@ -24,8 +24,8 @@ public:
template <typename T>
AndExpr(T &&e) { add(std::forward<T>(e)); }
- void add(const expr &e);
- void add(expr &&e);
+ void add(const expr &e, unsigned limit = 16);
+ void add(expr &&e, unsigned limit = 16);
void add(const AndExpr &other);
void del(const AndExpr &other);
void reset();

tame exponential explosion in AndExpr
uncommon, but exists in some unit tests