typing: skip smt solver if there's only 1 solution
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -178,8 +178,8 @@ void solver_print_stats(ostream &os) {
"Num queries: " << num_queries << "\n"
"Num invalid: " << num_invalid << "\n"
"Num skips: " << num_skips << "\n"
- "Num trivial " << num_trivial << " (" << trivial_pc << "%)\n"
- "Num unknown " << num_unknown << " (" << unknown_pc << "%)\n"
+ "Num trivial: " << num_trivial << " (" << trivial_pc << "%)\n"
+ "Num unknown: " << num_unknown << " (" << unknown_pc << "%)\n"
"Num SAT: " << num_sats << " (" << sat_pc << "%)\n"
"Num UNSAT: " << num_unsats << " (" << unsat_pc << "%)\n";
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -85,17 +85,29 @@ Errors TransformVerify::verify() const {
TypingAssignments::TypingAssignments(const expr &e) {
+ if (e.isTrue()) {
+ has_only_one_solution = true;
+ } else {
EnableSMTQueriesTMP tmp;
s.add(e);
r = s.check();
}
+}
+
+TypingAssignments::operator bool() const {
+ return !is_unsat && (has_only_one_solution || r.isSat());
+}
void TypingAssignments::operator++(void) {
+ if (has_only_one_solution) {
+ is_unsat = true;
+ } else {
EnableSMTQueriesTMP tmp;
s.block(r.getModel());
r = s.check();
assert(!r.isUnknown());
}
+}
TypingAssignments TransformVerify::getTypings() const {
// TODO: missing cross-program type constraints
@@ -111,6 +123,8 @@ TypingAssignments TransformVerify::getTypings() const {
}
void TransformVerify::fixupTypes(const TypingAssignments &ty) {
+ if (ty.has_only_one_solution)
+ return;
t.src.fixupTypes(ty.r.getModel());
t.tgt.fixupTypes(ty.r.getModel());
}

MODIFY
tools/transform.h
tools/transform.h
@@ -29,11 +29,13 @@ struct Transform {
class TypingAssignments {
smt::Solver s;
smt::Result r;
+ bool has_only_one_solution = false;
+ bool is_unsat = false;
TypingAssignments(const smt::expr &e);
public:
- bool operator!() const { return !r.isSat(); }
- operator bool() const { return r.isSat(); }
+ bool operator!() const { return !(bool)*this; }
+ operator bool() const;
void operator++(void);
friend class TransformVerify;

typing: skip smt solver if there's only 1 solution