Z3
InterpolationContext.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.util.Map;
21 import java.lang.String;
22 
24 
31 public class InterpolationContext extends Context
32 {
37  {
38  m_ctx = Native.mkInterpolationContext(0);
39  initContext();
40  }
41 
49  public InterpolationContext(Map<String, String> settings)
50  {
51  long cfg = Native.mkConfig();
52  for (Map.Entry<String, String> kv : settings.entrySet())
53  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
54  m_ctx = Native.mkInterpolationContext(cfg);
55  Native.delConfig(cfg);
56  initContext();
57  }
58 
64  {
65  checkContextMatch(a);
66  return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
67  }
68 
76  public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
77  {
78  checkContextMatch(pf);
79  checkContextMatch(pat);
80  checkContextMatch(p);
81 
82  ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
83  int n = seq.size();
84  Expr[] res = new Expr[n];
85  for (int i = 0; i < n; i++)
86  res[i] = Expr.create(this, seq.get(i).getNativeObject());
87  return res;
88  }
89 
97  public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
98  {
99  checkContextMatch(pat);
100  checkContextMatch(p);
101 
102  Native.LongPtr n_i = new Native.LongPtr();
103  Native.LongPtr n_m = new Native.LongPtr();
104  int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
105  interp = new ASTVector(this, n_i.value);
106  model = new Model(this, n_m.value);
107  return Z3_lbool.fromInt(r);
108  }
109 
116  public String InterpolationProfile()
117  {
118  return Native.interpolationProfile(nCtx());
119  }
120 
127  public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
128  {
129  Native.StringPtr n_err_str = new Native.StringPtr();
130  int r = Native.checkInterpolant(nCtx(),
131  cnsts.length,
132  Expr.arrayToNative(cnsts),
133  parents,
134  Expr.arrayToNative(interps),
135  n_err_str,
136  theory.length,
137  Expr.arrayToNative(theory));
138  error = n_err_str.value;
139  return r;
140  }
141 
148  public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
149  {
150  Native.IntPtr n_num = new Native.IntPtr();
151  Native.IntPtr n_num_theory = new Native.IntPtr();
152  Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
153  Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
154  Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
155  Native.StringPtr n_err_str = new Native.StringPtr();
156  int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
157  int num = n_num.value;
158  int num_theory = n_num_theory.value;
159  error = n_err_str.value;
160  cnsts = new Expr[num];
161  parents = new int[num];
162  theory = new Expr[num_theory];
163  for (int i = 0; i < num; i++)
164  {
165  cnsts[i] = Expr.create(this, n_cnsts.value[i]);
166  parents[i] = n_parents.value[i];
167  }
168  for (int i = 0; i < num_theory; i++)
169  theory[i] = Expr.create(this, n_theory.value[i]);
170  return r;
171  }
172 
179  public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
180  {
181  Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
182  }
183 }
static void delConfig(long a0)
Definition: Native.java:645
static long mkConfig()
Definition: Native.java:639
Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
static int readInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
Definition: Native.java:5288
static String interpolationProfile(long a0)
Definition: Native.java:5279
static long mkInterpolant(long a0, long a1)
Definition: Native.java:5246
static int computeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
Definition: Native.java:5270
int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:650
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
static long mkInterpolationContext(long a0)
Definition: Native.java:5255
InterpolationContext(Map< String, String > settings)
static long getInterpolant(long a0, long a1, long a2, long a3)
Definition: Native.java:5261
static void writeInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
Definition: Native.java:5306
int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
def Map(f, args)
Definition: z3py.py:4063
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
static int checkInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)
Definition: Native.java:5297