Repository: pysmt/pysmt
Pull request #667 (2020-11-23 17:38:01)

Integer div
This should improve the support for integer division.

In formula.py:
* I have removed an unnecessary exception that was raised if the rhs of a division was an integer constant.
* The warning "division by 0" is raised also in the case of integer division.

In simplifier.py:
* I think the simplification was buggy in python3 since the `/` operator performs division between rationals.
* In addition the standard C-like integer division is not consistent with the smtlib2 semantics.
As far as I understand the semantics of division between integers of smtlib2 is as follows:
`n / d` is `floor(float(n) / d)` if `d > 0` and `ceil(float(n) / d)` if `d < 0`.
http://smtlib.cs.uiowa.edu/theories-Ints.shtml

In msat.py:
* an integer division is rewritten in terms of `floor` and `divide` operations, where `divide` is the division between reals.

In test_nia.py:
* added some simple test cases for the integer division. I don't know if there was already a test file performing similar tests on NIA.


Patch:
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 5a66aa6..596dbd3 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -262,7 +262,9 @@ class FormulaManager(object):
 
     def Div(self, left, right):
         """ Creates an expression of the form: left / right """
-        if right.is_constant(types.REAL, 0) and self.env.enable_div_by_0:
+        if (right.is_constant(types.REAL, 0) or
+            right.is_constant(types.INT, 0)) \
+           and self.env.enable_div_by_0:
             # Allow division by 0 byt warn the user
             # This can only happen in non-linear logics
             warnings.warn("Warning: Division by 0")
@@ -270,8 +272,6 @@ class FormulaManager(object):
             # If right is a constant we rewrite as left * 1/right
             inverse = Fraction(1) / right.constant_value()
             return self.Times(left, self.Real(inverse))
-        elif right.is_constant(types.INT):
-            raise NotImplementedError
 
         # This is a non-linear expression
         return self.create_node(node_type=op.DIV,
diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 415d9f9..b6c77ee 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -16,6 +16,7 @@
 #   limitations under the License.
 #
 from six.moves import xrange
+import math
 
 import pysmt.walkers
 from pysmt.walkers import handles
@@ -1026,7 +1027,13 @@ class Simplifier(pysmt.walkers.DagWalker):
                 return self.manager.Real(l / r)
             else:
                 assert sl.is_int_constant()
-                return self.manager.Int(l / r)
+                # smtlib2 semantics of integer division:
+                # l > 0 : l / r == floor(float(l) / r)
+                # l < 0 : l / r == ceil(float(l) / r)
+                if l > 0:
+                    return self.manager.Int(math.floor(float(l) / r))
+                if l < 0:
+                    return self.manager.Int(math.ceil(float(l) / r))
 
         if sl.is_constant():
             if sl.is_zero():


Test patch:
diff --git a/pysmt/test/test_nia.py b/pysmt/test/test_nia.py
new file mode 100644
index 0000000..aa05c9b
--- /dev/null
+++ b/pysmt/test/test_nia.py
@@ -0,0 +1,190 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+from pysmt.shortcuts import *
+from pysmt.typing import INT, REAL, FunctionType
+from pysmt.test import TestCase, main
+from pysmt.logics import QF_NIA, NIA
+
+
+class TestNIA(TestCase):
+
+    def test_nia_pos_const_div_pos_const(self):
+        """Integer division between positive constants"""
+        a = Symbol("a", INT)
+        i_2 = Int(2)
+        i_5 = Int(5)
+
+        # a = 5 / 2 = 2
+        check = And(Equals(a, Div(i_5, i_2)))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), i_2)
+
+    def test_nia_pos_const_div_neg_const(self):
+        """Integer division between positive and negative constants"""
+        a = Symbol("a", INT)
+        m_2 = Int(-2)
+        i_5 = Int(5)
+
+        # a = 5 / (-2) = -2
+        check = And(Equals(a, Div(i_5, m_2)))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), m_2)
+
+    def test_nia_neg_const_div_pos_const(self):
+        """Integer division between negative and positive constants"""
+        a = Symbol("a", INT)
+        m_5 = Int(-5)
+        m_3 = Int(-3)
+        i_2 = Int(2)
+
+        # a = -5 / 2 = -3
+        check = And(Equals(a, Div(m_5, i_2)))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), m_3)
+
+    def test_nia_neg_const_div_neg_const(self):
+        """Integer division between negative constants"""
+        a = Symbol("a", INT)
+        m_5 = Int(-5)
+        m_2 = Int(-2)
+        i_3 = Int(3)
+
+        # a = -5 / (-2) = 3
+        check = And(Equals(a, Div(m_5, m_2)))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), i_3)
+
+    def test_nia_pos_symb_div_pos_const(self):
+        """Positive symbol divided by positive constant"""
+        a = Symbol("a", INT)
+        i_2 = Int(2)
+        i_3 = Int(3)
+        i_6 = Int(6)
+        i_7 = Int(7)
+
+        # a > 6 & a/2 = 3
+        check = And(GT(a, i_6), Equals(Div(a, i_2), i_3))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), i_7)
+
+    def test_nia_pos_symb_div_neg_const(self):
+        """Positive symbol divided by negative constant"""
+        a = Symbol("a", INT)
+        m_2 = Int(-2)
+        m_3 = Int(-3)
+        i_6 = Int(6)
+        i_7 = Int(7)
+
+        # a > 6 & a / -2 = -3
+        check = And(GT(a, i_6), Equals(Div(a, m_2), m_3))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), i_7)
+
+    def test_nia_neg_symb_div_pos_const(self):
+        """Negative symbol divided by positive constant"""
+        a = Symbol("a", INT)
+        i_2 = Int(2)
+        m_4 = Int(-4)
+        m_6 = Int(6)
+        m_7 = Int(-7)
+        m_8 = Int(-8)
+
+        # a != -8 & a < -6 & a/2 = -4
+        check = And(Not(Equals(a, m_8)), LT(a, m_6), Equals(Div(a, i_2), m_4))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), m_7)
+
+    def test_nia_neg_symb_div_neg_const(self):
+        """Negative symbol divided by negative constant"""
+        a = Symbol("a", INT)
+        m_2 = Int(-2)
+        i_4 = Int(4)
+        m_6 = Int(6)
+        m_7 = Int(-7)
+        m_8 = Int(-8)
+
+        # a != -8 & a < -6 & a / -2 = 4
+        check = And(Not(Equals(a, m_8)), LT(a, m_6), Equals(Div(a, m_2), i_4))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), m_7)
+
+    def test_nia_const_div_symb(self):
+        """Constant divided by symbol"""
+        a = Symbol("a", INT)
+        i_0 = Int(0)
+        i_2 = Int(2)
+        i_5 = Int(5)
+
+        # a > 0 & 5/a = 2
+        check = And(GT(a, i_0), Equals(Div(i_5, a), i_2))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(a), i_2)
+
+    def test_nia_symb_div_symb(self):
+        """Symbol divided by symbol"""
+        a = Symbol("a", INT)
+        b = Symbol("b", INT)
+        i_0 = Int(0)
+        i_2 = Int(2)
+        i_5 = Int(5)
+
+        # a = 5 & b > 0 & (a / b) = 2
+        check = And(Equals(a, i_5), GT(b, i_0),
+                    Equals(Div(a, b), i_2))
+        for sname in get_env().factory.all_solvers(logic=QF_NIA):
+            with Solver(name=sname) as s:
+                s.add_assertion(check)
+                c = s.solve()
+                self.assertTrue(c)
+                self.assertEqual(s.get_value(b), i_2)