improve printing of NaN in couterexamples
MODIFY
ir/type.cpp
ir/type.cpp
@@ -308,7 +308,8 @@ expr VoidType::mkInput(State &s, const char *name,
UNREACHABLE();
}
-void VoidType::printVal(ostream &os, const State &s, const expr &e) const {
+void VoidType::printVal(ostream &os, const State &s, const Model &m,
+ const expr &e) const {
UNREACHABLE();
}
@@ -367,7 +368,8 @@ expr IntType::mkInput(State &s, const char *name,
return expr::mkVar(name, bits());
}
-void IntType::printVal(ostream &os, const State &s, const expr &e) const {
+void IntType::printVal(ostream &os, const State &s, const Model &m,
+ const expr &e) const {
e.printHexadecimal(os);
os << " (";
e.printUnsigned(os);
@@ -551,19 +553,18 @@ expr FloatType::mkInput(State &s, const char *name,
return expr::mkVar(name, bits());
}
-void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
- if (isNaN(e, true).isTrue()) {
- os << "SNaN";
- return;
- }
- if (isNaN(e, false).isTrue()) {
- os << "QNaN";
- return;
- }
+void FloatType::printVal(ostream &os, const State &s, const Model &m,
+ const expr &e) const {
e.printHexadecimal(os);
- os << " (";
auto f = getFloat(e);
- if (f.isFPZero().isTrue()) {
+ os << " (";
+ if (m.eval(isNaN(e, true)).isTrue()) {
+ os << "SNaN";
+ } else if (m.eval(isNaN(e, false)).isTrue()) {
+ os << "QNaN";
+ } else if (f.isNaN().isTrue()) {
+ os << "NaN";
+ } else if (f.isFPZero().isTrue()) {
os << (f.isFPNegative().isTrue() ? "-0.0" : "+0.0");
} else if (f.isInf().isTrue()) {
os << (f.isFPNegative().isTrue() ? "-oo" : "+oo");
@@ -675,7 +676,8 @@ PtrType::mkUndefInput(State &s, const ParamAttrs &attrs) const {
return s.getMemory().mkUndefInput(attrs);
}
-void PtrType::printVal(ostream &os, const State &s, const expr &e) const {
+void PtrType::printVal(ostream &os, const State &s, const Model &m,
+ const expr &e) const {
os << Pointer(s.getMemory(), e);
}
@@ -965,7 +967,8 @@ unsigned AggregateType::numPointerElements() const {
return count;
}
-void AggregateType::printVal(ostream &os, const State &s, const expr &e) const {
+void AggregateType::printVal(ostream &os, const State &s, const Model &m,
+ const expr &e) const {
UNREACHABLE();
}
@@ -1390,8 +1393,9 @@ SymbolicType::mkUndefInput(State &st, const ParamAttrs &attrs) const {
DISPATCH(mkUndefInput(st, attrs), UNREACHABLE());
}
-void SymbolicType::printVal(ostream &os, const State &st, const expr &e) const {
- DISPATCH(printVal(os, st, e), UNREACHABLE());
+void SymbolicType::printVal(ostream &os, const State &st, const Model &m,
+ const expr &e) const {
+ DISPATCH(printVal(os, st, m, e), UNREACHABLE());
}
void SymbolicType::print(ostream &os) const {

MODIFY
ir/type.h
ir/type.h
@@ -116,7 +116,7 @@ public:
virtual std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const;
- virtual void printVal(std::ostream &os, const State &s,
+ virtual void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const = 0;
virtual void print(std::ostream &os) const = 0;
@@ -141,7 +141,7 @@ public:
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -169,7 +169,7 @@ public:
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -212,7 +212,7 @@ public:
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -248,7 +248,7 @@ public:
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -305,7 +305,7 @@ public:
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
unsigned numPointerElements() const;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
const AggregateType* getAsAggregateType() const override;
};
@@ -414,7 +414,7 @@ public:
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, const State &s,
+ void printVal(std::ostream &os, const State &s, const smt::Model &m,
const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -61,7 +61,7 @@ static void print_single_varval(ostream &os, const State &st, const Model &m,
expr partial = m.eval(val.value);
- type.printVal(os, st, m.eval(val.value, true));
+ type.printVal(os, st, m, m.eval(val.value, true));
// undef variables may not have a model since each read uses a copy
// TODO: add intervals of possible values for ints at least?

improve printing of NaN in couterexamples