Merge pull request #34 from smover/new_backends

New backends - add ic3ia tool

.github/workflows/python-app.yml

@@ -28,6 +28,20 @@ jobs:
         pip install flake8 nose pysmt sympy ply wolframclient six picos scipy control
         if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
         pysmt-install --confirm-agreement --z3 --bdd
+    - name: install ic3ia
+      run: |
+        cd
+        wget https://mathsat.fbk.eu/release/mathsat-5.6.10-linux-x86_64.tar.gz
+        tar xf mathsat-5.6.10-linux-x86_64.tar.gz
+        wget https://es-static.fbk.eu/people/griggio/ic3ia/ic3ia-23.05.tar.gz
+        tar xf ic3ia-23.05.tar.gz 
+        cd ic3ia-23.05
+        mkdir build
+        cd build
+        cmake -DMATHSAT_DIR=../../mathsat-5.6.10-linux-x86_64 -DCMAKE_BUILD_TYPE=Release ../
+        make
+        cd
+        export PATH=$PATH:~/ic3ia-23.05
 #    - name: Lint with flake8
 #      run: |
 #        # stop the build if there are Python syntax errors or undefined names

barrier/decomposition/explicit.py

@@ -32,7 +32,7 @@
     DecompositionEncoder
 )
 
-from barrier.msatic3 import MSatic3, prove_ts
+from barrier.vmt.vmt_engines import MSatic3, VmtResult, prove_ts
 
 from pysmt.logics import QF_NRA
 from pysmt.shortcuts import (
@@ -464,10 +464,10 @@ def get_dyn_sys_from_derivator(derivator):
 
                 msatic3_res = prove_ts(ts, p)
 
-                if (msatic3_res == MSatic3.Result.SAFE):
+                if (msatic3_res == VmtResult.SAFE):
                     res = Result.SAFE
                     reach_states = TRUE()
-                elif (msatic3_res == MSatic3.Result.UNSAFE):
+                elif (msatic3_res == VmtResult.UNSAFE):
                     res = Result.UNKNOWN
                     reach_states = FALSE()
 

barrier/test/__init__.py

@@ -14,7 +14,7 @@
 from pysmt.environment import reset_env
 from pysmt.exceptions import SolverAPINotFound
 
-from barrier.msatic3 import MSatic3
+from barrier.vmt.vmt_engines import MSatic3, MSatic3NotAvailable, Ic3IA, Ic3IANotAvailable
 from barrier.mathematica.mathematica import has_kernel
 
 class TestCase(unittest.TestCase):
@@ -53,8 +53,31 @@ def __init__(self):
 
     def __call__(self, test_fun):
         msg = "MSatic3 not available"
-        cond = MSatic3.find_msatic() is None
-        @unittest.skipIf(cond, msg)
+        skip = False
+        try:
+            MSatic3()
+        except MSatic3NotAvailable:
+            skip = True
+        @unittest.skipIf(skip, msg)
+        @wraps(test_fun)
+        def wrapper(*args, **kwargs):
+            return test_fun(*args, **kwargs)
+        return wrapper
+
+class skipIfIc3IAIsNotAvailable(object):
+    """Skip a test if the given solver is not available."""
+
+    def __init__(self):
+        pass
+
+    def __call__(self, test_fun):
+        msg = "MSatic3 not available"
+        skip = False
+        try:
+            Ic3IA()
+        except Ic3IANotAvailable:
+            skip = True
+        @unittest.skipIf(skip, msg)
         @wraps(test_fun)
         def wrapper(*args, **kwargs):
             return test_fun(*args, **kwargs)

barrier/test/test_dec_encoding.py

@@ -31,7 +31,7 @@
 from pysmt.logics import QF_NRA
 from pysmt.exceptions import SolverAPINotFound
 
-from barrier.test import TestCase, skipIfMSaticIsNotAvailable
+from barrier.test import TestCase, skipIfMSaticIsNotAvailable, skipIfIc3IAIsNotAvailable
 from barrier.system import DynSystem
 from barrier.utils import get_range_from_int, get_mathsat_smtlib
 
@@ -44,7 +44,7 @@
 from barrier.formula_utils import FormulaHelper
 
 from barrier.ts import TS
-from barrier.msatic3 import MSatic3
+from barrier.vmt.vmt_engines import MSatic3, Ic3IA, VmtResult, prove_ts
 
 from barrier.decomposition.encoding import (
     DecompositionEncoder, DecompositionOptions,
@@ -132,8 +132,8 @@ def test_enc(self):
         (ts, p) = encoder.get_quantified_ts()
         (ts, p, predicates) = encoder.get_ts_ia()
 
-        res = self._prove_ts(ts, p)
-        self.assertTrue(res == MSatic3.Result.SAFE)
+        res = prove_ts(ts, p)
+        self.assertTrue(res == VmtResult.SAFE)
 
     def test_invar_in_init(self):
         env = get_env()
@@ -195,7 +195,7 @@ def test_wiggins(self):
                                         cons,
                                         options)
         (ts, p, predicates) = encoder.get_ts_ia()
-        self.assertTrue(self._prove_ts(ts, p) == MSatic3.Result.UNSAFE)
+        self.assertTrue(prove_ts(ts, p) == VmtResult.UNSAFE)
 
 
         options = DecompositionOptions(False, False, False, False)
@@ -207,7 +207,7 @@ def test_wiggins(self):
                                         cons,
                                         options)
         (ts, p, predicates) = encoder.get_ts_ia()
-        self.assertTrue(self._prove_ts(ts, p) == MSatic3.Result.SAFE)
+        self.assertTrue(prove_ts(ts, p) == VmtResult.SAFE)
 
 
     @attr('msatic3')
@@ -217,17 +217,17 @@ def test_hs(self):
         env = get_env()
 
         models = [
-            ("disc1.hyb", MSatic3.Result.SAFE),
-            ("disc2.hyb", MSatic3.Result.UNSAFE),
-            ("disc3.hyb", MSatic3.Result.UNSAFE),
-            ("disc4.hyb", MSatic3.Result.SAFE),
-            ("disc5.hyb", MSatic3.Result.SAFE),
-            ("disc6.hyb", MSatic3.Result.SAFE),
-            ("disc7.hyb", MSatic3.Result.UNSAFE),
-            ("disc8.hyb", MSatic3.Result.SAFE),
-            ("cont1.hyb", MSatic3.Result.UNSAFE),
-            ("cont2.hyb", MSatic3.Result.SAFE),
-            ("hyb_fc.hyb", MSatic3.Result.SAFE)
+            ("disc1.hyb", VmtResult.SAFE),
+            ("disc2.hyb", VmtResult.UNSAFE),
+            ("disc3.hyb", VmtResult.UNSAFE),
+            ("disc4.hyb", VmtResult.SAFE),
+            ("disc5.hyb", VmtResult.SAFE),
+            ("disc6.hyb", VmtResult.SAFE),
+            ("disc7.hyb", VmtResult.UNSAFE),
+            ("disc8.hyb", VmtResult.SAFE),
+            ("cont1.hyb", VmtResult.UNSAFE),
+            ("cont2.hyb", VmtResult.SAFE),
+            ("hyb_fc.hyb", VmtResult.SAFE)
         ]
 
         for (m,expected) in models:
@@ -254,7 +254,7 @@ def test_hs(self):
 
                 print(ts.trans.serialize())
 
-                self.assertTrue(self._prove_ts(ts, p) == expected)
+                self.assertTrue(prove_ts(ts, p) == expected)
 
 
     def test_hs_hscc(self):
@@ -282,4 +282,4 @@ def test_hs_hscc(self):
             with open("/tmp/hscc2017.preds", "w") as outstream:
                 ts.dump_predicates(outstream, predicates)
 
-            # self.assertTrue(self._prove_ts(ts, p) == MSatic3.Result.SAFE)
+            # self.assertTrue(prove_ts(ts, p) == VmtResult.SAFE)

barrier/test/test_ts.py

@@ -20,9 +20,9 @@
 from pysmt.typing import REAL
 from pysmt.exceptions import SolverAPINotFound
 
-from barrier.test import TestCase, skipIfMSaticIsNotAvailable
+from barrier.test import TestCase, skipIfMSaticIsNotAvailable, skipIfIc3IAIsNotAvailable
 from barrier.ts import TS, ImplicitAbstractionEncoder
-from barrier.msatic3 import MSatic3
+from barrier.vmt.vmt_engines import MSatic3, Ic3IA
 
 class TestSystem(TestCase):
 
@@ -85,9 +85,7 @@ def test_serialize_to_mcmt(self):
             print(outstream.getvalue())
 
 
-    @attr('msatic3')
-    @skipIfMSaticIsNotAvailable()
-    def test_impl_abs(self):
+    def _aux_test_impl_abs(self, get_vmt_engine):
         long_tests = set(["toy",
                           "mem_slave_tlm.1",
                           "pipeline",
@@ -110,29 +108,16 @@ def test_impl_abs(self):
                 print("Skipping long test %s" % smtfile)
                 continue
 
-            # DEBUG
-            # print(base)
-            # if (base != "bist_cell"):
-            #     continue
-
             with open(smtfile, "r") as f:
                 print("Reading %s" % smtfile)
                 (ts, safe) = TS.from_vmt(f, env)
 
             with open(os.path.join(input_path, predfile), "r") as f:
                 predicates = ts.read_predicates(f)
 
-
-            try:
-                ic3 = MSatic3()
-
-                print("Verifying using IA...")
-                res_orig = ic3.solve(smtfile)
-            except SolverAPINotFound:
-                print("MSatic3 not found...")
-                logging.debug("MSatic3 not found...")
-                continue
-
+            ic3 = get_vmt_engine()
+            print("Verifying using IA...")
+            res_orig = ic3.solve(smtfile)
 
             print("\n---\nChecking encodings\n---\n")
 
@@ -155,17 +140,24 @@ def test_impl_abs(self):
                     f.close()
 
                 print("Verifying %s..." % base)
-                try:
-                    ic3 = MSatic3()
 
-                    print("Verifying using fixed IA encoding...")
-                    res = ic3.solve(outfile)
+                ic3 = get_vmt_engine()
+                print("Verifying using fixed IA encoding...")
+                res = ic3.solve(outfile)
+                self.assertTrue(res == res_orig)
 
-                    self.assertTrue(res == res_orig)
-                except SolverAPINotFound:
-                    print("MSatic3 not found...")
-                    logging.debug("MSatic3 not found...")
                 os.remove(outfile)
             print("Verified result %s" % str(res_orig))
 
+    @attr('msatic3')
+    @skipIfMSaticIsNotAvailable()
+    def test_impl_abs_msatic3(self):
+        init_f = lambda : MSatic3()
+        self._aux_test_impl_abs(init_f)
+
+    @attr('ic3ia')
+    @skipIfIc3IAIsNotAvailable()
+    def test_impl_abs_ic3ia(self):
+        init_f = lambda : Ic3IA()
+        self._aux_test_impl_abs(init_f)
 

barrier/vmt/__init__.py

@@ -0,0 +1 @@
+# Barrier python module