cheap precondition simplification
MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -17,6 +17,11 @@ void AndExpr::add(const AndExpr &other) {
exprs.insert(other.exprs.begin(), other.exprs.end());
}
+void AndExpr::del(const AndExpr &other) {
+ for (auto &e : other.exprs)
+ exprs.erase(e);
+}
+
expr AndExpr::operator()() const {
return expr::mk_and(exprs);
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -17,6 +17,7 @@ class AndExpr {
public:
void add(expr &&e);
void add(const AndExpr &other);
+ void del(const AndExpr &other);
expr operator()() const;
friend std::ostream &operator<<(std::ostream &os, const AndExpr &e);
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -283,12 +283,13 @@ static void check_refinement(Errors &errs, Transform &t,
// FIXME: broken handling of transformation precondition
//src_state.startParsingPre();
//expr pre = t.precondition ? t.precondition->toSMT(src_state) : true;
- expr pre_src = src_state.getPre()();
- expr pre_tgt = tgt_state.getPre()();
+ auto pre_src_and = src_state.getPre();
+ auto &pre_tgt_and = tgt_state.getPre();
// optimization: rewrite "tgt /\ (src -> foo)" to "tgt /\ foo" if src = tgt
- if (pre_src.eq(pre_tgt))
- pre_src = true;
+ pre_src_and.del(pre_tgt_and);
+ expr pre_src = pre_src_and();
+ expr pre_tgt = pre_tgt_and();
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
expr memory_cnstr

cheap precondition simplification