From 8c652afd6e603ce672e3a0e5fbb3bf533b3d641d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Thu, 26 Dec 2019 15:39:08 +0100
Subject: [PATCH] Verification: Added IntRange::isLessThan and
 IntRange::isGreaterThan

---
 lib/exprengine.cpp | 58 ++++++++++++++++++++++++++++++++++++++++++++++
 lib/exprengine.h   |  2 ++
 2 files changed, 60 insertions(+)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 71a9378b0..4d4108916 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -707,6 +707,64 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
 #endif
 }
 
+bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
+{
+    if (value < minValue || value > maxValue)
+        return false;
+
+    const Data *data = dynamic_cast<Data *>(dataBase);
+    if (data->constraints.empty())
+        return true;
+#ifdef USE_Z3
+    // Check the value against the constraints
+    ExprData exprData;
+    z3::solver solver(exprData.context);
+    try {
+        z3::expr e = exprData.context.int_const(name.c_str());
+        exprData.valueExpr.emplace(name, e);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
+        solver.add(e > value);
+        return solver.check() == z3::sat;
+    } catch (const z3::exception &exception) {
+        std::cerr << "z3: " << exception << std::endl;
+        return true;  // Safe option is to return true
+    }
+#else
+    // The value may or may not be in range
+    return false;
+#endif
+}
+
+bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
+{
+    if (value < minValue || value > maxValue)
+        return false;
+
+    const Data *data = dynamic_cast<Data *>(dataBase);
+    if (data->constraints.empty())
+        return true;
+#ifdef USE_Z3
+    // Check the value against the constraints
+    ExprData exprData;
+    z3::solver solver(exprData.context);
+    try {
+        z3::expr e = exprData.context.int_const(name.c_str());
+        exprData.valueExpr.emplace(name, e);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
+        solver.add(e < value);
+        return solver.check() == z3::sat;
+    } catch (const z3::exception &exception) {
+        std::cerr << "z3: " << exception << std::endl;
+        return true;  // Safe option is to return true
+    }
+#else
+    // The value may or may not be in range
+    return false;
+#endif
+}
+
 bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const
 {
 #ifdef USE_Z3
diff --git a/lib/exprengine.h b/lib/exprengine.h
index aaceb0a33..d4ea132be 100644
--- a/lib/exprengine.h
+++ b/lib/exprengine.h
@@ -129,6 +129,8 @@ namespace ExprEngine {
             return str(minValue) + ":" + str(maxValue);
         }
         bool isEqual(DataBase *dataBase, int value) const override;
+        bool isGreaterThan(DataBase *dataBase, int value) const override;
+        bool isLessThan(DataBase *dataBase, int value) const override;
 
         int128_t minValue;
         int128_t maxValue;