Z3
InterpolationContext.cs
Go to the documentation of this file.
1 using System;
2 using System.Collections.Generic;
3 using System.Linq;
4 using System.Text;
5 using System.Diagnostics.Contracts;
6 using System.Runtime.InteropServices;
7 
8 namespace Microsoft.Z3
9 {
15  [ContractVerification(true)]
17  {
18 
22  public InterpolationContext() : base() { }
23 
28  public InterpolationContext(Dictionary<string, string> settings) : base(settings) { }
29 
30  #region Terms
31  public BoolExpr MkInterpolant(BoolExpr a)
35  {
36  Contract.Requires(a != null);
37  Contract.Ensures(Contract.Result<BoolExpr>() != null);
38 
39  CheckContextMatch(a);
40  return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
41  }
42  #endregion
43 
50  public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
51  {
52  Contract.Requires(pf != null);
53  Contract.Requires(pat != null);
54  Contract.Requires(p != null);
55  Contract.Ensures(Contract.Result<Expr>() != null);
56 
57  CheckContextMatch(pf);
58  CheckContextMatch(pat);
59  CheckContextMatch(p);
60 
61  ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
62  uint n = seq.Size;
63  Expr[] res = new Expr[n];
64  for (uint i = 0; i < n; i++)
65  res[i] = Expr.Create(this, seq[i].NativeObject);
66  return res;
67  }
68 
75  public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
76  {
77  Contract.Requires(pat != null);
78  Contract.Requires(p != null);
79  Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
80  Contract.Ensures(Contract.ValueAtReturn(out model) != null);
81 
82  CheckContextMatch(pat);
83  CheckContextMatch(p);
84 
85  IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
86  int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
87  interp = new ASTVector(this, i);
88  model = new Model(this, m);
89  return (Z3_lbool)r;
90  }
91 
98  public string InterpolationProfile()
99  {
100  return Native.Z3_interpolation_profile(nCtx);
101  }
102 
109  public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
110  {
111  Contract.Requires(cnsts.Length == parents.Length);
112  Contract.Requires(cnsts.Length == interps.Length + 1);
113  IntPtr n_err_str;
114  int r = Native.Z3_check_interpolant(nCtx,
115  (uint)cnsts.Length,
116  Expr.ArrayToNative(cnsts),
117  parents,
118  Expr.ArrayToNative(interps),
119  out n_err_str,
120  (uint)theory.Length,
121  Expr.ArrayToNative(theory));
122  error = Marshal.PtrToStringAnsi(n_err_str);
123  return r;
124  }
125 
132  public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
133  {
134  uint num = 0, num_theory = 0;
135  IntPtr[] n_cnsts;
136  IntPtr[] n_theory;
137  IntPtr n_err_str;
138  int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
139  error = Marshal.PtrToStringAnsi(n_err_str);
140  cnsts = new Expr[num];
141  parents = new uint[num];
142  theory = new Expr[num_theory];
143  for (int i = 0; i < num; i++)
144  cnsts[i] = Expr.Create(this, n_cnsts[i]);
145  for (int i = 0; i < num_theory; i++)
146  theory[i] = Expr.Create(this, n_theory[i]);
147  return r;
148  }
149 
156  public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
157  {
158  Contract.Requires(cnsts.Length == parents.Length);
159  Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
160  }
161  }
162 }
Boolean expressions
Definition: BoolExpr.cs:31
static Z3_ast Z3_mk_interpolant(Z3_context a0, Z3_ast a1)
Definition: Native.cs:5975
string InterpolationProfile()
Return a string summarizing cumulative time used for interpolation.
static int Z3_compute_interpolant(Z3_context a0, Z3_ast a1, Z3_params a2, [In, Out] ref Z3_ast_vector a3, [In, Out] ref Z3_model a4)
Definition: Native.cs:5996
static int Z3_read_interpolation_problem(Z3_context a0, [In, Out] ref uint a1, [Out] out Z3_ast[] a2, [Out] out uint[] a3, string a4, out IntPtr a5, [In, Out] ref uint a6, [Out] out Z3_ast[] a7)
Definition: Native.cs:6012
Vectors of ASTs.
Definition: ASTVector.cs:28
Expressions are terms.
Definition: Expr.cs:29
uint Size
The size of the vector
Definition: ASTVector.cs:34
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
Computes an interpolant.
The InterpolationContext is suitable for generation of interpolants.
static int Z3_check_interpolant(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, [In] Z3_ast[] a4, out IntPtr a5, uint a6, [In] Z3_ast[] a7)
Definition: Native.cs:6020
int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
Reads an interpolation problem from a file.
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
Checks the correctness of an interpolant.
static string Z3_interpolation_profile(Z3_context a0)
Definition: Native.cs:6004
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
Writes an interpolation problem to a file.
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
static void Z3_write_interpolation_problem(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, string a4, uint a5, [In] Z3_ast[] a6)
Definition: Native.cs:6028
Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
Computes an interpolant.
static Z3_ast_vector Z3_get_interpolant(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_params a3)
Definition: Native.cs:5988
InterpolationContext(Dictionary< string, string > settings)
Constructor.