Repository: pacti-org/pacti (language: python)

Issue:
Add license

Addressing problems with deduction
Here we fix #14
There was a problem with the algorithm for deduction.


Discussion / hints:

Fix patch:
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 00000000..6fa9c981
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,25 @@
+This software is licensed under the BSD 2-Clause License.
+
+Copyright (c) 2022, the Gear contributors.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
\ No newline at end of file
diff --git a/src/gear/polyhedralterm.py b/src/gear/polyhedralterm.py
index 65fbd66e..29947cce 100644
--- a/src/gear/polyhedralterm.py
+++ b/src/gear/polyhedralterm.py
@@ -54,8 +54,10 @@ def __eq__(self, other):
         return match and self.constant == other.constant
 
     def __str__(self) -> str:
+        varlist = list(self.variables.items())
+        varlist.sort(key = lambda x: str(x[0]))
         res = " + ".join([str(coeff)+"*"+var.name
-                          for var, coeff in self.variables.items()])
+                          for var, coeff in varlist])
         res += " <= " + str(self.constant)
         return res
 
@@ -927,7 +929,7 @@ def get_kaykobad_context(term:PolyhedralTerm, context:PolyhedralTermSet,
                     continue
                 # 1. Verify Kaykobad pair: sign of nonzero matrix terms
                 for var in forbidden_vars:
-                    if context_term.get_coefficient(var) != 0 and context_term.get_sign(var) != term.get_sign(var):
+                    if context_term.get_coefficient(var) != 0 and transform_coeff * context_term.get_sign(var) != term.get_sign(var):
                         term_is_invalid = True
                         logging.debug("Failed first matrix-vector verification")
                         break
@@ -940,8 +942,8 @@ def get_kaykobad_context(term:PolyhedralTerm, context:PolyhedralTermSet,
                 for j, j_var in enumerate(forbidden_vars):
                     logging.debug("Verifying third condition on variable %s", j_var)
                     if j != i:
-                        residuals[j] = term.get_sign(j_var) * transform_coeff * context_term.get_coefficient(j_var) * term.get_coefficient(i_var) / context_term.get_coefficient(i_var)
-                    if np.abs(term.get_coefficient(j_var)) * transform_coeff <= partial_sums[j] + residuals[j]:
+                        residuals[j] = term.get_sign(j_var) * context_term.get_coefficient(j_var) * term.get_coefficient(i_var) / context_term.get_coefficient(i_var)
+                    if np.abs(term.get_coefficient(j_var)) <= partial_sums[j] + residuals[j]:
                         logging.debug("q coefficient: %s", term.get_coefficient(j_var))
                         logging.debug("RHS: %s", partial_sums[j] + residuals[j])
                         term_is_invalid = True


Test patch:
diff --git a/tests/test_polyhedral_terms.py b/tests/test_polyhedral_terms.py
index 4e112105..0bb1bd11 100644
--- a/tests/test_polyhedral_terms.py
+++ b/tests/test_polyhedral_terms.py
@@ -95,7 +95,20 @@ def test_polyhedral_abduce_6():
     reference = reference.abduce_with_context(context, vars_elim)
     assert(reference.terms == expected.terms)
 
-def test_polyhedral_abduce_7():
+
+def test_polyhedral_deduce_7():
+    # a term that can be simplified with one element of the context
+    x = Var('x')
+    y = Var('y')
+    z = Var('z')
+    reference = to_pts(["x - y <= -1"])
+    context = to_pts(["y - z <= -1"])
+    expected = to_pts(["x - z <= -2"])
+    vars_elim = {y}
+    reference = reference.deduce_with_context(context, vars_elim)
+    assert(reference.terms == expected.terms)
+
+def test_polyhedral_abduce_8():
     # a term that can be simplified with one element of the context
     y = Var('y')
     z = Var('z')