simplify mkLambda
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1210,7 +1210,7 @@ void Memory::storeLambda(const Pointer &ptr, const expr &offset,
blk.type = stored_ty;
}
} else {
- blk.val = expr::mkLambda({ offset }, expr::mkIf(cond && offset_cond, val,
+ blk.val = expr::mkLambda(offset, expr::mkIf(cond && offset_cond, val,
blk.val.load(offset)));
}
blk.type |= stored_ty;
@@ -1530,23 +1530,9 @@ Memory::mkCallState(const vector<PtrInput> *ptr_inputs, bool nofree) const {
modifies |= ptr_in.val.non_poison && argp.getBid() == bid;
}
- if (modifies.isTrue())
- continue;
-
auto &new_val = st.non_local_block_val[bid - num_consts];
auto &old_val = non_local_block_val[bid].val;
-
- if (modifies.isFalse()) {
- new_val = old_val;
- continue;
- }
-
- expr offset
- = expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
- new_val
- = expr::mkLambda({ offset },
- expr::mkIf(modifies, new_val.load(offset),
- old_val.load(offset)));
+ new_val = expr::mkIf(modifies, new_val, old_val);
}
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1612,16 +1612,10 @@ expr expr::mkForAll(const set<expr> &vars, expr &&val) {
val());
}
-expr expr::mkLambda(const set<expr> &vars, const expr &val) {
- C2(val);
- assert(!vars.empty());
-
- unique_ptr<Z3_app[]> vars_ast(new Z3_app[vars.size()]);
- unsigned i = 0;
- for (auto &v : vars) {
- vars_ast[i++] = (Z3_app)v();
- }
- return Z3_mk_lambda_const(ctx(), vars.size(), vars_ast.get(), val());
+expr expr::mkLambda(const expr &var, const expr &val) {
+ C2(var, val);
+ auto ast = (Z3_app)var();
+ return Z3_mk_lambda_const(ctx(), 1, &ast, val());
}
expr expr::simplify() const {

MODIFY
smt/expr.h
smt/expr.h
@@ -296,7 +296,7 @@ public:
static expr mkIf(const expr &cond, const expr &then, const expr &els);
static expr mkForAll(const std::set<expr> &vars, expr &&val);
- static expr mkLambda(const std::set<expr> &vars, const expr &val);
+ static expr mkLambda(const expr &var, const expr &val);
expr simplify() const;

simplify mkLambda