Merge pull request #276 from kenmcmil/issue260

issue #260 -- support timeout in Z3_compute_interpolant

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,7 +271,14 @@ extern "C" {
         ast_manager &_m = mk_c(c)->m();
 
         model_ref m;
-        lbool _status = iz3interpolate(_m,
+        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,
@@ -271,6 +286,12 @@ extern "C" {
                                          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,11 +313,13 @@ extern "C" {
         else {
             model_ref mr;
             m_solver.get()->get_model(mr);
+            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);
 

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)
+    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.