From 5a107095c937dd879ae411cfce87dc8806c5eba3 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 11:32:51 -0700
Subject: [PATCH] removing python changes for interp

---
 src/api/python/z3.py      | 15 ---------------
 src/api/python/z3types.py |  2 --
 2 files changed, 17 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 533a71956..ce53a4c1f 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7253,18 +7253,3 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
-def Interp(a):
-     ctx = main_ctx()
-     s = BoolSort(ctx)
-     a = s.cast(a)
-     return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
-
-def tree_interpolant(f,p=None,ctx=None):
-    ctx = _get_ctx(ctx)
-    ptr = (ctypes.POINTER(AstVectorObj) * 1)()
-    if p == None:
-        p = ParamsRef(ctx)
-    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr[0])
-    if res == Z3_L_FALSE:
-        return AstVector(ptr[0],ctx)
-    raise NoInterpolant()
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index 56316eb46..593312d68 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -110,5 +110,3 @@ class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
 
-class NoInterpolant():
-    def __init__(self):