mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
removing python changes for interp
This commit is contained in:
parent
b933a4da85
commit
5a107095c9
|
@ -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()
|
||||
|
|
|
@ -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):
|
||||
|
|
Loading…
Reference in a new issue