Z3
InterpolationContext.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
22 import java.util.Map;
23 
30 public class InterpolationContext extends Context
31 {
36  {
37  long m_ctx;
38  synchronized(creation_lock) {
39  m_ctx = Native.mkInterpolationContext(0);
40  }
41  return new InterpolationContext(m_ctx);
42  }
43 
51  public static InterpolationContext mkContext(Map<String, String> settings)
52  {
53  long m_ctx;
54  synchronized(creation_lock) {
55  long cfg = Native.mkConfig();
56  for (Map.Entry<String, String> kv : settings.entrySet())
57  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
58  m_ctx = Native.mkInterpolationContext(cfg);
59  Native.delConfig(cfg);
60  }
61  return new InterpolationContext(m_ctx);
62  }
63 
64  private InterpolationContext(long m_ctx) {
65  super(m_ctx);
66  }
67 
73  {
74  checkContextMatch(a);
75  return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
76  }
77 
85  public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
86  {
87  checkContextMatch(pf);
88  checkContextMatch(pat);
89  checkContextMatch(p);
90 
91  ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
92  return seq.ToBoolExprArray();
93  }
94 
96  {
98  public BoolExpr[] interp = null;
99  public Model model = null;
100  };
101 
110  {
111  checkContextMatch(pat);
112  checkContextMatch(p);
113 
115  Native.LongPtr n_i = new Native.LongPtr();
116  Native.LongPtr n_m = new Native.LongPtr();
117  res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
118  if (res.status == Z3_lbool.Z3_L_FALSE)
119  res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
120  if (res.status == Z3_lbool.Z3_L_TRUE)
121  res.model = new Model(this, n_m.value);
122  return res;
123  }
124 
132  {
133  return Native.interpolationProfile(nCtx());
134  }
135 
137  {
138  public int return_value = 0;
139  public String error = null;
140  }
141 
148  public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
149  {
151  Native.StringPtr n_err_str = new Native.StringPtr();
152  res.return_value = Native.checkInterpolant(nCtx(),
153  cnsts.length,
154  Expr.arrayToNative(cnsts),
155  parents,
156  Expr.arrayToNative(interps),
157  n_err_str,
158  theory.length,
159  Expr.arrayToNative(theory));
160  res.error = n_err_str.value;
161  return res;
162  }
163 
165  {
166  public int return_value = 0;
167  public Expr[] cnsts;
168  public int[] parents;
169  public String error;
170  public Expr[] theory;
171  };
172 
179  public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
180  {
182 
183  Native.IntPtr n_num = new Native.IntPtr();
184  Native.IntPtr n_num_theory = new Native.IntPtr();
185  Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
186  Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
187  Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
188  Native.StringPtr n_err_str = new Native.StringPtr();
189  res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
190  int num = n_num.value;
191  int num_theory = n_num_theory.value;
192  res.error = n_err_str.value;
193  res.cnsts = new Expr[num];
194  res.parents = new int[num];
195  theory = new Expr[num_theory];
196  for (int i = 0; i < num; i++)
197  {
198  res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
199  res.parents[i] = n_parents.value[i];
200  }
201  for (int i = 0; i < num_theory; i++)
202  res.theory[i] = Expr.create(this, n_theory.value[i]);
203  return res;
204  }
205 
212  public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
213  {
214  Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
215  }
216 }
static void delConfig(long a0)
Definition: Native.java:669
static long mkConfig()
Definition: Native.java:663
static int readInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
Definition: Native.java:5490
static String interpolationProfile(long a0)
Definition: Native.java:5481
static InterpolationContext mkContext(Map< String, String > settings)
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
static long mkInterpolant(long a0, long a1)
Definition: Native.java:5446
ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
static int computeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
Definition: Native.java:5472
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:674
static long mkInterpolationContext(long a0)
Definition: Native.java:5455
static long getInterpolant(long a0, long a1, long a2, long a3)
Definition: Native.java:5463
static void writeInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
Definition: Native.java:5508
void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
def Map(f, args)
Definition: z3py.py:4207
static InterpolationContext mkContext()
BoolExpr [] GetInterpolant(Expr pf, Expr pat, Params p)
CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
def String(name, ctx=None)
Definition: z3py.py:9443
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
static int checkInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)
Definition: Native.java:5499