From d4dff70f39a5976bb5ced3a7299a1be7a998070d Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 28 Oct 2015 18:01:22 -0700
Subject: [PATCH] issue #260 -- support timeout in Z3_compute_interpolant

---
 src/api/api_interp.cpp | 47 +++++++++++++++++++++++++++++++-----------
 src/api/python/z3.py   | 19 +++++++++++++++--
 2 files changed, 52 insertions(+), 14 deletions(-)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index fab778bb3..2c1fd7d9b 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -255,6 +255,14 @@ extern "C" {
         scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
         m_solver.get()->updt_params(_p); // why do we have to do this?
 
+
+        // some boilerplate stolen from Z3_solver_check
+        unsigned timeout     =  to_params(p)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      =  to_params(p)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  =  to_params(p)->m_params.get_bool("ctrl_c", false);
+        cancel_eh<solver> eh(*m_solver.get());
+        api::context::set_interruptable si(*(mk_c(c)), eh);
+
         ast *_pat = to_ast(pat);
 
         ptr_vector<ast> interp;
@@ -263,14 +271,27 @@ extern "C" {
         ast_manager &_m = mk_c(c)->m();
 
         model_ref m;
-        lbool _status = iz3interpolate(_m,
-                                       *(m_solver.get()),
-                                       _pat,
-                                       cnsts,
-                                       interp,
-                                       m,
-                                       0 // ignore params for now
-                                       );
+        lbool _status;
+
+        {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            try {
+                _status = iz3interpolate(_m,
+                                         *(m_solver.get()),
+                                         _pat,
+                                         cnsts,
+                                         interp,
+                                         m,
+                                         0 // ignore params for now
+                                         );
+            }
+            catch (z3_exception & ex) {
+                mk_c(c)->handle_exception(ex);
+                return Z3_L_UNDEF;
+            }
+        }
 
         for (unsigned i = 0; i < cnsts.size(); i++)
             _m.dec_ref(cnsts[i]);
@@ -292,10 +313,12 @@ extern "C" {
         else {
             model_ref mr;
             m_solver.get()->get_model(mr);
-            Z3_model_ref *tmp_val = alloc(Z3_model_ref);
-            tmp_val->m_model = mr.get();
-            mk_c(c)->save_object(tmp_val);
-            *model = of_model(tmp_val);
+            if(mr.get()){
+                Z3_model_ref *tmp_val = alloc(Z3_model_ref);
+                tmp_val->m_model = mr.get();
+                mk_c(c)->save_object(tmp_val);
+                *model = of_model(tmp_val);
+            }
         }
 
         *out_interp = of_ast_vector(v);
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 5763db916..107c3b974 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7560,6 +7560,10 @@ def tree_interpolant(pat,p=None,ctx=None):
     If pat is satisfiable, raises an object of class ModelRef
     that represents a model of pat.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
@@ -7585,7 +7589,9 @@ def tree_interpolant(pat,p=None,ctx=None):
     res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
     if res == Z3_L_FALSE:
         return AstVector(ptr[0],ctx)
-    raise ModelRef(mptr[0], ctx)
+    if mptr[0]:
+        raise ModelRef(mptr[0], ctx)
+    return None
 
 def binary_interpolant(a,b,p=None,ctx=None):
     """Compute an interpolant for a binary conjunction.
@@ -7600,6 +7606,10 @@ def binary_interpolant(a,b,p=None,ctx=None):
     If a & b is satisfiable, raises an object of class ModelRef
     that represents a model of a &b.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
@@ -7608,7 +7618,8 @@ def binary_interpolant(a,b,p=None,ctx=None):
     Not(x >= 0)
     """
     f = And(Interpolant(a),b)
-    return tree_interpolant(f,p,ctx)[0]
+    ti = tree_interpolant(f,p,ctx)
+    return ti[0] if ti != None else None
 
 def sequence_interpolant(v,p=None,ctx=None):
     """Compute interpolant for a sequence of formulas.
@@ -7626,6 +7637,10 @@ def sequence_interpolant(v,p=None,ctx=None):
     If a & b is satisfiable, raises an object of class ModelRef
     that represents a model of a & b.
 
+    If neither a proof of unsatisfiability nor a model is obtained
+    (for example, because of a timeout, or because models are disabled)
+    then None is returned.
+
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.