Z3
src/api/java/InterpolationContext.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines