From 05eb73b23ab34f69302a5b6c34d7f82d6d44855b Mon Sep 17 00:00:00 2001
From: Valentyn Sobol <napster_1997@mail.ru>
Date: Tue, 25 Jul 2023 20:55:17 +0300
Subject: [PATCH] Add API comments

---
 .../usvm/constraints/UNumericConstraints.kt   | 28 +++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
index 45c001ed79..8e28a20866 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
@@ -36,6 +36,22 @@ import org.usvm.util.Intervals
 
 private typealias ConstraintTerms<Sort> = UExpr<Sort>
 
+/**
+ * Manage and simplify numeric constraints over bit-vectors (e.g. geq, lt, eq).
+ *
+ * [isNumericConstraint] --- check if expression is numeric constraint over bit-vectors and can
+ * be handled with [UNumericConstraints].
+ *
+ * [addNumericConstraint] --- add numeric constraint.
+ * Throws exception if constraint is not [isNumericConstraint]
+ *
+ * [addNegatedNumericConstraint] --- add negation of constraint.
+ * Throws exception if constraint is not [isNumericConstraint]
+ *
+ * [constraints] --- retrieve currently added constraints (possibly simplified).
+ *
+ * [evalInterval] --- retrieve possible values interval for the expression.
+ * */
 class UNumericConstraints<Sort : UBvSort> private constructor(
     private val ctx: UContext,
     val sort: Sort,
@@ -79,6 +95,10 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
             .flatMap { it.value.mkExpressions() }
     }
 
+    /**
+     * Check if [expr] is numeric constraint over bit-vectors and can
+     * be handled with [UNumericConstraints].
+     * */
     fun isNumericConstraint(expr: UBoolExpr): Boolean =
         recognizeNumericConstraint(
             expr = expr,
@@ -88,6 +108,10 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
             unknownConstraint = { false }
         )
 
+    /**
+     * Add numeric constraint [expr].
+     * Throws exception if constraint is not [isNumericConstraint]
+     * */
     fun addNumericConstraint(expr: UBoolExpr) {
         recognizeNumericConstraint(
             expr = expr,
@@ -116,6 +140,10 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
         )
     }
 
+    /**
+     * Add negation of constraint [expr].
+     * Throws exception if constraint is not [isNumericConstraint]
+     * */
     fun addNegatedNumericConstraint(expr: UBoolExpr) {
         recognizeNumericConstraint(
             expr = expr,