diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-27 12:08:24 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 19:08:24 +0000 |
| commit | c95d4c5473e8c26832fef89a9a42275517a42613 (patch) | |
| tree | 36f42cad17c22b39c232c97b111df1e1e9a382f2 /examples/api | |
| parent | 1483676841847216a7cfe15e5d201a924739d014 (diff) | |
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)
This is to make it consistent with the name of the SMT-LIB operator
(fp.add).
Diffstat (limited to 'examples/api')
| -rw-r--r-- | examples/api/java/FloatingPointArith.java | 8 | ||||
| -rw-r--r-- | examples/api/python/floating_point.py | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index bf8d3a238..61ab18148 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -51,13 +51,13 @@ public class FloatingPointArith { // Assert that floating-point addition is not associative: // (a + (b + c)) != ((a + b) + c) Expr rm = em.mkConst(RoundingMode.roundNearestTiesToEven); - Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS, + Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, a, - em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, b, c)); - Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS, + em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, b, c)); + Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, - em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, a, b), + em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, a, b), c); smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, a, b))); diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 44a3d66d2..66b18642d 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -43,7 +43,7 @@ if __name__ == "__main__": z = slv.mkConst(fp32, 'z') # check floating-point arithmetic is commutative, i.e. x + y == y + x - commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPPlus, rm, x, y), slv.mkTerm(kinds.FPPlus, rm, y, x)) + commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPAdd, rm, x, y), slv.mkTerm(kinds.FPAdd, rm, y, x)) slv.push() slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) @@ -76,8 +76,8 @@ if __name__ == "__main__": slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z)) # (x + y) + z == x + (y + z) - lhs = slv.mkTerm(kinds.FPPlus, rm, slv.mkTerm(kinds.FPPlus, rm, x, y), z) - rhs = slv.mkTerm(kinds.FPPlus, rm, x, slv.mkTerm(kinds.FPPlus, rm, y, z)) + lhs = slv.mkTerm(kinds.FPAdd, rm, slv.mkTerm(kinds.FPAdd, rm, x, y), z) + rhs = slv.mkTerm(kinds.FPAdd, rm, x, slv.mkTerm(kinds.FPAdd, rm, y, z)) associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs)) slv.assertFormula(associative) |