From 6f1309183345f31163cc6b8302ff29233055f5b5 Mon Sep 17 00:00:00 2001
From: Sven Verdoolaege <sven.verdoolaege@gmail.com>
Date: Fri, 18 May 2018 20:27:52 +0200
Subject: [PATCH] doc: explicitly state that the divisor of an ?div_? operation
 is positive

The isl AST generator will always produce division of this form.
For those created by the user, it's the user's responsibility.

Requested-by: Uday Reddy B <udayreddy@gmail.com>
Signed-off-by: Sven Verdoolaege <sven.verdoolaege@gmail.com>
---
 doc/user.pod | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/doc/user.pod b/doc/user.pod
index 959a8881..fd8d787c 100644
--- a/doc/user.pod
+++ b/doc/user.pod
@@ -9959,18 +9959,22 @@ Exact division.  That is, the result is known to be an integer.
 
 Result of integer division, rounded towards negative
 infinity.
+The divisor is known to be positive.
 
 =item C<isl_ast_op_pdiv_q>
 
 Result of integer division, where dividend is known to be non-negative.
+The divisor is known to be positive.
 
 =item C<isl_ast_op_pdiv_r>
 
 Remainder of integer division, where dividend is known to be non-negative.
+The divisor is known to be positive.
 
 =item C<isl_ast_op_zdiv_r>
 
 Equal to zero iff the remainder on integer division is zero.
+The divisor is known to be positive.
 
 =item C<isl_ast_op_cond>
 
@@ -10139,7 +10143,10 @@ the context of an C<isl_ast_build>.
 
 The function C<isl_ast_expr_address_of> can be applied to an
 C<isl_ast_expr> of type C<isl_ast_op_access> only. It is meant
-to represent the address of the C<isl_ast_expr_access>. The function
+to represent the address of the C<isl_ast_expr_access>.
+The second argument of the functions C<isl_ast_expr_pdiv_q> and
+C<isl_ast_expr_pdiv_r> should always evaluate to a positive number.
+The function
 C<isl_ast_expr_and_then> as well as C<isl_ast_expr_or_else> are short-circuit
 versions of C<isl_ast_expr_and> and C<isl_ast_expr_or>, respectively.
 
-- 
2.11.4.GIT