Skip to content

Commit c440810

Browse files
committed
SMT2 parser: support fp.abs
This commit adds the obvious mapping from fp.abs to our abs_exprt.
1 parent c91cf24 commit c440810

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

src/solvers/smt2/smt2_parser.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1106,6 +1106,18 @@ void smt2_parsert::setup_expressions()
11061106
return with_exprt(op[0], op[1], op[2]);
11071107
};
11081108

1109+
expressions["fp.abs"] = [this] {
1110+
auto op = operands();
1111+
1112+
if(op.size() != 1)
1113+
throw error("fp.abs takes one operand");
1114+
1115+
if(op[0].type().id() != ID_floatbv)
1116+
throw error("fp.abs takes FloatingPoint operand");
1117+
1118+
return abs_exprt(op[0]);
1119+
};
1120+
11091121
expressions["fp.isNaN"] = [this] {
11101122
auto op = operands();
11111123

0 commit comments

Comments
 (0)