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 BoolExpr[] 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  return seq.ToBoolExprArray();
84  }
85 
87  {
89  public BoolExpr[] interp = null;
90  public Model model = null;
91  };
92 
101  {
102  checkContextMatch(pat);
103  checkContextMatch(p);
104 
106  Native.LongPtr n_i = new Native.LongPtr();
107  Native.LongPtr n_m = new Native.LongPtr();
108  res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
109  if (res.status == Z3_lbool.Z3_L_FALSE)
110  res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
111  if (res.status == Z3_lbool.Z3_L_TRUE)
112  res.model = new Model(this, n_m.value);
113  return res;
114  }
115 
122  public String InterpolationProfile()
123  {
124  return Native.interpolationProfile(nCtx());
125  }
126 
128  {
129  public int return_value = 0;
130  public String error = null;
131  }
132 
139  public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
140  {
142  Native.StringPtr n_err_str = new Native.StringPtr();
143  res.return_value = Native.checkInterpolant(nCtx(),
144  cnsts.length,
145  Expr.arrayToNative(cnsts),
146  parents,
147  Expr.arrayToNative(interps),
148  n_err_str,
149  theory.length,
150  Expr.arrayToNative(theory));
151  res.error = n_err_str.value;
152  return res;
153  }
154 
156  {
157  public int return_value = 0;
158  public Expr[] cnsts;
159  public int[] parents;
160  public String error;
161  public Expr[] theory;
162  };
163 
170  public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
171  {
173 
174  Native.IntPtr n_num = new Native.IntPtr();
175  Native.IntPtr n_num_theory = new Native.IntPtr();
176  Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
177  Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
178  Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
179  Native.StringPtr n_err_str = new Native.StringPtr();
180  res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
181  int num = n_num.value;
182  int num_theory = n_num_theory.value;
183  res.error = n_err_str.value;
184  res.cnsts = new Expr[num];
185  res.parents = new int[num];
186  theory = new Expr[num_theory];
187  for (int i = 0; i < num; i++)
188  {
189  res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
190  res.parents[i] = n_parents.value[i];
191  }
192  for (int i = 0; i < num_theory; i++)
193  res.theory[i] = Expr.create(this, n_theory.value[i]);
194  return res;
195  }
196 
203  public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
204  {
205  Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
206  }
207 }
static void delConfig(long a0)
Definition: Native.java:672
static long mkConfig()
Definition: Native.java:666
static int readInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
Definition: Native.java:5512
static String interpolationProfile(long a0)
Definition: Native.java:5503
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:149
static long mkInterpolant(long a0, long a1)
Definition: Native.java:5470
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:5494
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:677
static long mkInterpolationContext(long a0)
Definition: Native.java:5479
InterpolationContext(Map< String, String > settings)
static long getInterpolant(long a0, long a1, long a2, long a3)
Definition: Native.java:5485
static void writeInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
Definition: Native.java:5530
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:4100
BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
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:5521