SMT: check Z3's unknown reason instead of always declaring it a timeout
fixes
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -25,7 +25,8 @@ static unsigned num_invalid = 0;
static unsigned num_trivial = 0;
static unsigned num_sats = 0;
static unsigned num_unsats = 0;
-static unsigned num_unknown = 0;
+static unsigned num_timeout = 0;
+static unsigned num_errors = 0;
namespace {
class Tactic {
@@ -281,7 +282,7 @@ expr Solver::assertions() const {
Result Solver::check() const {
if (config::skip_smt) {
++num_skips;
- return Result::UNKNOWN;
+ return Result::SKIP;
}
if (!valid) {
@@ -302,9 +303,15 @@ Result Solver::check() const {
case Z3_L_TRUE:
++num_sats;
return Z3_solver_get_model(ctx(), s);
- case Z3_L_UNDEF:
- ++num_unknown;
- return Result::UNKNOWN;
+ case Z3_L_UNDEF: {
+ string reason = Z3_solver_get_reason_unknown(ctx(), s);
+ if (reason == "timeout") {
+ ++num_timeout;
+ return Result::TIMEOUT;
+ }
+ ++num_errors;
+ return { Result::ERROR, move(reason) };
+ }
default:
UNREACHABLE();
}
@@ -344,7 +351,8 @@ void solver_print_stats(ostream &os) {
float total = num_queries / 100.0;
float trivial_pc = num_queries == 0 ? 0 :
(num_trivial * 100.0) / (num_trivial + num_queries);
- float unknown_pc = num_queries == 0 ? 0 : num_unknown / total;
+ float to_pc = num_queries == 0 ? 0 : num_timeout / total;
+ float error_pc = num_queries == 0 ? 0 : num_errors / total;
float sat_pc = num_queries == 0 ? 0 : num_sats / total;
float unsat_pc = num_queries == 0 ? 0 : num_unsats / total;
@@ -354,7 +362,8 @@ void solver_print_stats(ostream &os) {
"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 timeout: " << num_timeout << " (" << to_pc << "%)\n"
+ "Num errors: " << num_errors << " (" << error_pc << "%)\n"
"Num SAT: " << num_sats << " (" << sat_pc << "%)\n"
"Num UNSAT: " << num_unsats << " (" << unsat_pc << "%)\n";
}

MODIFY
smt/solver.h
smt/solver.h
#include <cstdint>
#include <functional>
#include <ostream>
+#include <string>
#include <utility>
typedef struct _Z3_model* Z3_model;
@@ -57,14 +58,18 @@ public:
class Result {
public:
- enum answer { UNSAT, SAT, INVALID, UNKNOWN };
+ enum answer { UNSAT, SAT, INVALID, SKIP, TIMEOUT, ERROR };
- Result() : a(UNKNOWN) {}
+ Result() : a(ERROR) {}
bool isSat() const { return a == SAT; }
bool isUnsat() const { return a == UNSAT; }
bool isInvalid() const { return a == INVALID; }
- bool isUnknown() const { return a == UNKNOWN; }
+ bool isSkip() const { return a == SKIP; }
+ bool isTimeout() const { return a == TIMEOUT; }
+ bool isError() const { return a == ERROR; }
+
+ auto& getReason() const { return reason; }
const Model& getModel() const {
assert(isSat());
@@ -74,8 +79,10 @@ public:
private:
Model m;
answer a;
+ std::string reason;
Result(answer a) : a(a) {}
+ Result(answer a, std::string &&reason) : a(a), reason(std::move(reason)) {}
Result(Z3_model m) : m(m), a(SAT) {}
friend class Solver;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -112,11 +112,21 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
return;
}
- if (r.isUnknown()) {
+ if (r.isTimeout()) {
errs.add("Timeout", false);
return;
}
+ if (r.isError()) {
+ errs.add("SMT Error: " + r.getReason(), false);
+ return;
+ }
+
+ if (r.isSkip()) {
+ errs.add("Skip", false);
+ return;
+ }
+
stringstream s;
string empty;
auto &var_name = var ? var->getName() : empty;
@@ -607,7 +617,7 @@ void TypingAssignments::operator++(void) {
EnableSMTQueriesTMP tmp;
s.block(r.getModel(), &sneg);
r = s.check();
- assert(!r.isUnknown());
+ assert(r.isSat() || r.isUnsat());
}
}

SMT: check Z3's unknown reason instead of always declaring it a timeout
fixes #19