Repository: pysmt/pysmt
Pull request #257 (2016-05-16 01:32:40)

Fixed bug in Non-linear theories comparison
Linearity information was being incorrectly compared and propagated in logics oracles.


Patch:
diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
index 3b7f0a2..6f6fae4 100755
--- a/pysmt/cmd/install.py
+++ b/pysmt/cmd/install.py
@@ -30,7 +30,7 @@ from pysmt.cmd.installers import CuddInstaller
 Installer = namedtuple("Installer", ["InstallerClass", "version", "extra_params"])
 INSTALLERS = [Installer(MSatInstaller,    "5.3.9", {}),
               Installer(Z3Installer,      "4.4.1", {}),
-              Installer(CVC4Installer,    "1.5-prerelease", {"git_version" : "c15ff43597b41ea457befecb1b0e2402e28cb523"}),
+              Installer(CVC4Installer,    "1.5-prerelease", {"git_version" : "68f22235a62f5276b206e9a6692a85001beb8d42"}),
               Installer(YicesInstaller,   "2.4.1", {}),
               Installer(BtorInstaller,    "2.2.0", {"lingeling_version": "bal"}),
               Installer(PicoSATInstaller, "960", {}),
diff --git a/pysmt/cmd/installers/cvc4.py b/pysmt/cmd/installers/cvc4.py
index 5828bce..397e68d 100644
--- a/pysmt/cmd/installers/cvc4.py
+++ b/pysmt/cmd/installers/cvc4.py
@@ -41,6 +41,15 @@ class CVC4Installer(SolverInstaller):
                                         self.bindings_dir)
 
     def compile(self):
+        # Patch the distribution to avoid a known problem
+        patch_name = "cvc4_wrapper.patch"
+        plink = "https://raw.githubusercontent.com/pysmt/solvers_patches/master/%s" % patch_name
+        SolverInstaller.do_download(plink, os.path.join(self.extract_path, patch_name))
+
+        # Apply patch
+        SolverInstaller.run("patch -p1 -i %s" % patch_name,
+                            directory=self.extract_path)
+
         # Prepare the building system
         SolverInstaller.run("bash autogen.sh", directory=self.extract_path)
 
diff --git a/pysmt/logics.py b/pysmt/logics.py
index 1463dff..8528767 100644
--- a/pysmt/logics.py
+++ b/pysmt/logics.py
@@ -102,15 +102,15 @@ class Theory(object):
             real_difference = False
 
         return Theory(
-            arrays=self.arrays | other.arrays,
-            bit_vectors=self.bit_vectors | other.bit_vectors,
-            floating_point=self.floating_point | other.floating_point,
-            integer_arithmetic=self.integer_arithmetic | other.integer_arithmetic,
-            real_arithmetic=self.real_arithmetic | other.real_arithmetic,
+            arrays=self.arrays or other.arrays,
+            bit_vectors=self.bit_vectors or other.bit_vectors,
+            floating_point=self.floating_point or other.floating_point,
+            integer_arithmetic=self.integer_arithmetic or other.integer_arithmetic,
+            real_arithmetic=self.real_arithmetic or other.real_arithmetic,
             integer_difference=integer_difference,
             real_difference=real_difference,
-            linear=self.linear | other.linear,
-            uninterpreted=self.uninterpreted | other.uninterpreted)
+            linear=self.linear and other.linear,
+            uninterpreted=self.uninterpreted or other.uninterpreted)
 
     def __eq__(self, other):
         if other is None or (not isinstance(other, Theory)):
@@ -145,6 +145,14 @@ class Theory(object):
         else:
             le_real_difference = False
 
+        if self.linear == other.linear:
+            le_linear = True
+        elif self.linear and not other.linear:
+            le_linear = True
+        else:
+            le_linear = False
+
+
         return (self.arrays <= other.arrays and
                 self.bit_vectors <= other.bit_vectors and
                 self.floating_point <= other.floating_point and
@@ -153,7 +161,7 @@ class Theory(object):
                 self.integer_arithmetic <= other.integer_arithmetic and
                 le_real_difference and
                 self.real_arithmetic <= other.real_arithmetic and
-                self.linear <= other.linear)
+                le_linear)
 
     def __str__(self):
         return "Arrays: %s, " % self.arrays +\


Test patch:
diff --git a/pysmt/test/test_logics.py b/pysmt/test/test_logics.py
index 3b98cb2..be14621 100644
--- a/pysmt/test/test_logics.py
+++ b/pysmt/test/test_logics.py
@@ -18,7 +18,7 @@
 import pysmt.logics
 from pysmt.logics import get_logic_by_name, get_logic, most_generic_logic
 from pysmt.logics import PYSMT_LOGICS
-from pysmt.logics import QF_LIA, LIA, UFLIRA, LRA, QF_UFLIRA, QF_BV
+from pysmt.logics import QF_LIA, LIA, UFLIRA, LRA, QF_UFLIRA, QF_BV, NRA
 from pysmt.exceptions import (UndefinedLogicError, NoSolverAvailableError,
                               NoLogicAvailableError)
 from pysmt.shortcuts import Solver, get_env
@@ -111,7 +111,7 @@ class TestLogic(TestCase):
                 Solver(logic=pysmt.logics.QF_BOOL)
 
         with self.assertRaises(NoSolverAvailableError):
-            Solver(logic=pysmt.logics.QF_ABV)
+            Solver(logic=NRA)
 
         with self.assertRaises(NoSolverAvailableError):
             Solver(name='picosat', logic=pysmt.logics.QF_BV)
@@ -128,6 +128,7 @@ class TestLogic(TestCase):
         self.assertEqual(mgl, UFLIRA)
         self.assertFalse(QF_BV >= QF_UFLIRA)
         self.assertFalse(QF_BV <= QF_UFLIRA)
+        self.assertTrue(NRA > LRA)
         with self.assertRaises(NoLogicAvailableError):
             most_generic_logic(PYSMT_LOGICS)