00001 00018 package com.microsoft.z3; 00019 00020 import java.util.Map; 00021 import java.lang.String; 00022 00023 import com.microsoft.z3.Native.IntPtr; 00024 import com.microsoft.z3.Native.UIntArrayPtr; 00025 import com.microsoft.z3.enumerations.Z3_lbool; 00026 00033 public class InterpolationContext extends Context 00034 { 00038 public InterpolationContext() throws Z3Exception 00039 { 00040 m_ctx = Native.mkInterpolationContext(0); 00041 initContext(); 00042 } 00043 00049 public InterpolationContext(Map<String, String> settings) throws Z3Exception 00050 { 00051 long cfg = Native.mkConfig(); 00052 for (Map.Entry<String, String> kv : settings.entrySet()) 00053 Native.setParamValue(cfg, kv.getKey(), kv.getValue()); 00054 m_ctx = Native.mkInterpolationContext(cfg); 00055 Native.delConfig(cfg); 00056 initContext(); 00057 } 00058 00063 public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception 00064 { 00065 checkContextMatch(a); 00066 return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); 00067 } 00068 00076 Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception 00077 { 00078 checkContextMatch(pf); 00079 checkContextMatch(pat); 00080 checkContextMatch(p); 00081 00082 ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); 00083 int n = seq.size(); 00084 Expr[] res = new Expr[n]; 00085 for (int i = 0; i < n; i++) 00086 res[i] = Expr.create(this, seq.get(i).getNativeObject()); 00087 return res; 00088 } 00089 00097 Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception 00098 { 00099 checkContextMatch(pat); 00100 checkContextMatch(p); 00101 00102 Native.LongPtr n_i = new Native.LongPtr(); 00103 Native.LongPtr n_m = new Native.LongPtr(); 00104 int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m); 00105 interp = new ASTVector(this, n_i.value); 00106 model = new Model(this, n_m.value); 00107 return Z3_lbool.fromInt(r); 00108 } 00109 00116 public String InterpolationProfile() throws Z3Exception 00117 { 00118 return Native.interpolationProfile(nCtx()); 00119 } 00120 00127 public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception 00128 { 00129 Native.StringPtr n_err_str = new Native.StringPtr(); 00130 int r = Native.checkInterpolant(nCtx(), 00131 cnsts.length, 00132 Expr.arrayToNative(cnsts), 00133 parents, 00134 Expr.arrayToNative(interps), 00135 n_err_str, 00136 theory.length, 00137 Expr.arrayToNative(theory)); 00138 error = n_err_str.value; 00139 return r; 00140 } 00141 00148 public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception 00149 { 00150 Native.IntPtr n_num = new Native.IntPtr(); 00151 Native.IntPtr n_num_theory = new Native.IntPtr(); 00152 Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); 00153 Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); 00154 Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr(); 00155 Native.StringPtr n_err_str = new Native.StringPtr(); 00156 int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory); 00157 int num = n_num.value; 00158 int num_theory = n_num_theory.value; 00159 error = n_err_str.value; 00160 cnsts = new Expr[num]; 00161 parents = new int[num]; 00162 theory = new Expr[num_theory]; 00163 for (int i = 0; i < num; i++) 00164 { 00165 cnsts[i] = Expr.create(this, n_cnsts.value[i]); 00166 parents[i] = n_parents.value[i]; 00167 } 00168 for (int i = 0; i < num_theory; i++) 00169 theory[i] = Expr.create(this, n_theory.value[i]); 00170 return r; 00171 } 00172 00179 public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception 00180 { 00181 Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); 00182 } 00183 }