add a simple SMT model minimizer
use it to minimize typing models to eliminate many equivalent models
MODIFY
ir/type.cpp
ir/type.cpp
@@ -734,8 +734,7 @@ expr SymbolicType::operator==(const Type &b) const {
expr c(false);
c |= isInt() && i == rhs->i;
c |= isFloat() && f == rhs->f;
- // TODO: to reenable this, we need partial models and/or a shrinker
- //c |= isPtr() && p == rhs->p;
+ c |= isPtr() && p == rhs->p;
c |= isArray() && a == rhs->a;
c |= isVector() && v == rhs->v;
// FIXME: add support for this: c |= isStruct() && s == rhs->s;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -973,6 +973,22 @@ void expr::operator|=(const expr &rhs) {
}
}
+expr expr::mk_and(const set<expr> &vals) {
+ expr ret(true);
+ for (auto &e : vals) {
+ ret &= e;
+ }
+ return ret;
+}
+
+expr expr::mk_or(const set<expr> &vals) {
+ expr ret(false);
+ for (auto &e : vals) {
+ ret |= e;
+ }
+ return ret;
+}
+
expr expr::implies(const expr &rhs) const {
if (eq(rhs))
return true;

MODIFY
smt/expr.h
smt/expr.h
@@ -197,6 +197,9 @@ public:
void operator&=(const expr &rhs);
void operator|=(const expr &rhs);
+ static expr mk_and(const std::set<expr> &vals);
+ static expr mk_or(const std::set<expr> &vals);
+
expr implies(const expr &rhs) const;
expr notImplies(const expr &rhs) const;

MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -200,7 +200,11 @@ ostream& operator<<(ostream &os, const Model &m) {
}
-SolverPop::~SolverPop() {
+SolverPush::SolverPush(Solver &s) : s(s) {
+ Z3_solver_push(ctx(), s.s);
+}
+
+SolverPush::~SolverPush() {
Z3_solver_pop(ctx(), s.s, 1);
}
@@ -233,17 +237,29 @@ void Solver::add(const expr &e) {
}
}
-void Solver::block(const Model &m) {
- expr c(false);
+void Solver::block(const Model &m, bool minimize) {
+ set<expr> assignments;
for (const auto &[var, val] : m) {
- c |= var != val;
+ assignments.insert(var == val);
+ }
+
+ if (minimize) {
+ // simple left-to-right variable discard algorithm
+ Solver s;
+ s.add(!assertions());
+
+ for (auto I = assignments.begin(); I != assignments.end(); ) {
+ SolverPush push(s);
+ expr val = *I;
+ I = assignments.erase(I);
+
+ s.add(expr::mk_and(assignments));
+ if (!s.check().isUnsat())
+ assignments.insert(val);
}
- add(c);
}
-SolverPop Solver::push() {
- Z3_solver_push(ctx(), s);
- return *this;
+ add(!expr::mk_and(assignments));
}
void Solver::reset() {
@@ -251,6 +267,19 @@ void Solver::reset() {
tactic->reset_solver();
}
+expr Solver::assertions() const {
+ auto vect = Z3_solver_get_assertions(ctx(), s);
+ Z3_ast_vector_inc_ref(ctx(), vect);
+ expr ret(true);
+
+ for (unsigned i = 0, e = Z3_ast_vector_size(ctx(), vect); i != e; ++i) {
+ ret &= Z3_ast_vector_get(ctx(), vect, i);
+ }
+
+ Z3_ast_vector_dec_ref(ctx(), vect);
+ return ret;
+}
+
Result Solver::check() const {
if (config::skip_smt) {
++num_skips;

MODIFY
smt/solver.h
smt/solver.h
@@ -84,12 +84,11 @@ private:
class Solver;
-class SolverPop {
+class SolverPush {
Solver &s;
- SolverPop(Solver &s) : s(s) {}
public:
- ~SolverPop();
- friend class Solver;
+ SolverPush(Solver &s);
+ ~SolverPush();
};
@@ -102,14 +101,15 @@ public:
~Solver();
void add(const expr &e);
- void block(const Model &m);
- SolverPop push();
+ void block(const Model &m, bool minimize = false);
void reset();
+ expr assertions() const;
+
Result check() const;
static void check(std::initializer_list<E> queries);
- friend class SolverPop;
+ friend class SolverPush;
};

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -187,6 +187,7 @@ re2c:yyfill:check = 0;
"nsw" { return NSW; }
"nuw" { return NUW; }
"exact" { return EXACT; }
+"bitcast" { return BITCAST; }
"sext" { return SEXT; }
"zext" { return ZEXT; }
"trunc" { return TRUNC; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -626,6 +626,7 @@ static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
ConversionOp::Op op;
switch (op_token) {
+ case BITCAST: op = ConversionOp::BitCast; break;
case SEXT: op = ConversionOp::SExt; break;
case ZEXT: op = ConversionOp::ZExt; break;
case TRUNC: op = ConversionOp::Trunc; break;
@@ -810,6 +811,7 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case FSHL:
case FSHR:
return parse_ternary(name, t);
+ case BITCAST:
case SEXT:
case ZEXT:
case TRUNC:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -7,6 +7,7 @@ TOKEN(AND)
TOKEN(ARROW)
TOKEN(ASHR)
TOKEN(BAND)
+TOKEN(BITCAST)
TOKEN(BITREVERSE)
TOKEN(BSWAP)
TOKEN(BOR)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -332,7 +332,7 @@ void TypingAssignments::operator++(void) {
is_unsat = true;
} else {
EnableSMTQueriesTMP tmp;
- s.block(r.getModel());
+ s.block(r.getModel(), /*minimize=*/true);
r = s.check();
assert(!r.isUnknown());
}

add a simple SMT model minimizer
use it to minimize typing models to eliminate many equivalent models