add timeout parameter to check_context

Author: Dejan Jovanovic

Makefile

@@ -47,7 +47,7 @@ publish: dist
 	python -m twine upload --repository pypi dist/*
 
 install:
-	pip install
+	pip install .
 
 clean:
 	rm -rf  *.pyc *~ __pycache__ */*.pyc */*~ */__pycache__ */*/*.pyc */*/*~ */*/__pycache_

test/context_test.py

@@ -75,6 +75,24 @@ def test_context(self):
         param.dispose()
         ctx.dispose()
 
+    def test_timeout(self):
+        cfg = Config()
+        cfg.default_config_for_logic('QF_NIA')
+        ctx = Context(cfg)
+        int_t = Types.int_type()
+        [x, y, z] = [Terms.new_uninterpreted_term(int_t, id) for id in ['x', 'y', 'z']]
+        # x, y, z > 0
+        for var in [x, y, z]:
+            ctx.assert_formula(Terms.arith_gt0_atom(var))
+        # x^3 + y^3 = z3
+        [x3, y3, z3] = [Terms.product([var, var, var]) for var in [x, y, z]]
+        lhs = Terms.sum([x3, y3])
+        eq = Terms.arith_eq_atom(lhs, z3)
+        ctx.assert_formula(eq)
+        status = ctx.check_context(timeout=1)
+        self.assertEqual(status, Status.INTERRUPTED)
+        ctx.dispose()
+        cfg.dispose()
 
 if __name__ == '__main__':
     unittest.main()

yices/Context.py

@@ -11,6 +11,8 @@
 from .Status import Status
 from .Yices import Yices
 
+import threading
+
 class Context:
 
     __population = 0
@@ -62,12 +64,18 @@ def assert_formulas(self, python_array_or_tuple):
         return True
 
 
-    def check_context(self, params=None):
+    def check_context(self, params=None, timeout=None):
         assert self.context is not None
-        #unwrap the params object
+        # unwrap the params object
         if params is not None:
             params = params.params
+        # set the timeout
+        if timeout is not None:
+            timer = threading.Timer(timeout, Context.stop_search, [self])
+            timer.start()
         status = Yices.check_context(self.context, params)
+        if timeout is not None:
+            timer.cancel()
         if status == -1:
             raise YicesException('yices_check_context')
         return status