speedup type inference when there are many possible typings
see eg
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -218,8 +218,9 @@ void solver_tactic_verbose(bool yes) {
tactic_verbose = yes;
}
-Solver::Solver() {
- s = Z3_mk_solver_from_tactic(ctx(), tactic->t);
+Solver::Solver(bool simple) {
+ s = simple ? Z3_mk_simple_solver(ctx())
+ : Z3_mk_solver_from_tactic(ctx(), tactic->t);
Z3_solver_inc_ref(ctx(), s);
}
@@ -237,25 +238,22 @@ void Solver::add(const expr &e) {
}
}
-void Solver::block(const Model &m, bool minimize) {
+void Solver::block(const Model &m, Solver *sneg) {
set<expr> assignments;
for (const auto &[var, val] : m) {
assignments.insert(var == val);
}
- if (minimize) {
+ if (sneg) {
// simple left-to-right variable discard algorithm
- Solver s;
- s.add(!assertions());
-
for (auto I = assignments.begin(); I != assignments.end(); ) {
- SolverPush push(s);
+ SolverPush push(*sneg);
expr val = *I;
I = assignments.erase(I);
- s.add(expr::mk_and(assignments));
- if (!s.check().isUnsat())
- assignments.insert(val);
+ sneg->add(expr::mk_and(assignments));
+ if (!sneg->check().isUnsat())
+ assignments.insert(move(val));
}
}

MODIFY
smt/solver.h
smt/solver.h
@@ -97,11 +97,12 @@ class Solver {
bool valid = true;
using E = std::pair<expr, std::function<void(const Result &r)>>;
public:
- Solver();
+ Solver(bool simple = false);
~Solver();
void add(const expr &e);
- void block(const Model &m, bool minimize = false);
+ // use a negated solver for minimization
+ void block(const Model &m, Solver *sneg = nullptr);
void reset();
expr assertions() const;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -339,12 +339,13 @@ Errors TransformVerify::verify() const {
}
-TypingAssignments::TypingAssignments(const expr &e) {
+TypingAssignments::TypingAssignments(const expr &e) : s(true), sneg(true) {
if (e.isTrue()) {
has_only_one_solution = true;
} else {
EnableSMTQueriesTMP tmp;
s.add(e);
+ sneg.add(!e);
r = s.check();
}
}
@@ -358,7 +359,7 @@ void TypingAssignments::operator++(void) {
is_unsat = true;
} else {
EnableSMTQueriesTMP tmp;
- s.block(r.getModel(), /*minimize=*/true);
+ s.block(r.getModel(), &sneg);
r = s.check();
assert(!r.isUnknown());
}

MODIFY
tools/transform.h
tools/transform.h
@@ -28,7 +28,7 @@ struct Transform {
class TypingAssignments {
- smt::Solver s;
+ smt::Solver s, sneg;
smt::Result r;
bool has_only_one_solution = false;
bool is_unsat = false;

speedup type inference when there are many possible typings
see eg #113