Z3
InterpolationContext.cs
Go to the documentation of this file.
1 
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4 
5 --*/
6 
7 using System;
8 using System.Collections.Generic;
9 using System.Linq;
10 using System.Text;
12 using System.Runtime.InteropServices;
13 
14 namespace Microsoft.Z3
15 {
21  [ContractVerification(true)]
23  {
24 
28  public InterpolationContext() : base() { }
29 
34  public InterpolationContext(Dictionary<string, string> settings) : base(settings) { }
35 
36  #region Terms
37  public BoolExpr MkInterpolant(BoolExpr a)
41  {
42  Contract.Requires(a != null);
43  Contract.Ensures(Contract.Result<BoolExpr>() != null);
44 
45  CheckContextMatch(a);
46  return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
47  }
48  #endregion
49 
56  public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
57  {
58  Contract.Requires(pf != null);
59  Contract.Requires(pat != null);
60  Contract.Requires(p != null);
61  Contract.Ensures(Contract.Result<Expr>() != null);
62 
63  CheckContextMatch(pf);
64  CheckContextMatch(pat);
65  CheckContextMatch(p);
66 
67  ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
68  return seq.ToBoolExprArray();
69  }
70 
77  public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
78  {
79  Contract.Requires(pat != null);
80  Contract.Requires(p != null);
81  Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
82  Contract.Ensures(Contract.ValueAtReturn(out model) != null);
83 
84  CheckContextMatch(pat);
85  CheckContextMatch(p);
86 
87  IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
88  int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
89  interp = new ASTVector(this, i).ToBoolExprArray();
90  model = new Model(this, m);
91  return (Z3_lbool)r;
92  }
93 
100  public string InterpolationProfile()
101  {
102  return Native.Z3_interpolation_profile(nCtx);
103  }
104 
111  public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
112  {
113  Contract.Requires(cnsts.Length == parents.Length);
114  Contract.Requires(cnsts.Length == interps.Length + 1);
115  IntPtr n_err_str;
116  int r = Native.Z3_check_interpolant(nCtx,
117  (uint)cnsts.Length,
118  Expr.ArrayToNative(cnsts),
119  parents,
120  Expr.ArrayToNative(interps),
121  out n_err_str,
122  (uint)theory.Length,
123  Expr.ArrayToNative(theory));
124  error = Marshal.PtrToStringAnsi(n_err_str);
125  return r;
126  }
127 
134  public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
135  {
136  uint num = 0, num_theory = 0;
137  IntPtr[] n_cnsts;
138  IntPtr[] n_theory;
139  IntPtr n_err_str;
140  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);
141  error = Marshal.PtrToStringAnsi(n_err_str);
142  cnsts = new Expr[num];
143  parents = new uint[num];
144  theory = new Expr[num_theory];
145  for (int i = 0; i < num; i++)
146  cnsts[i] = Expr.Create(this, n_cnsts[i]);
147  for (int i = 0; i < num_theory; i++)
148  theory[i] = Expr.Create(this, n_theory[i]);
149  return r;
150  }
151 
158  public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
159  {
160  Contract.Requires(cnsts.Length == parents.Length);
161  Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
162  }
163  }
164 }
Boolean expressions
Definition: BoolExpr.cs:31
string InterpolationProfile()
Return a string summarizing cumulative time used for interpolation.
Vectors of ASTs.
Definition: ASTVector.cs:28
Expressions are terms.
Definition: Expr.cs:29
Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
Computes an interpolant.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
The InterpolationContext is suitable for generation of interpolants.
int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
Reads an interpolation problem from a file.
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
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
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
BoolExpr [] GetInterpolant(Expr pf, Expr pat, Params p)
Computes an interpolant.
void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
Writes an interpolation problem to a file.
int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
Checks the correctness of an interpolant.
InterpolationContext(Dictionary< string, string > settings)
Constructor.