diff options
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) |