1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
using System;
using System.Collections;
using System.Collections.Generic;
using System.Threading;
using System.IO;
using System.Diagnostics;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie;
using Microsoft.Boogie.Z3;
using Microsoft.Z3;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.Simplify;
using TypeAst = System.IntPtr;
using TermAst = System.IntPtr;
using ConstDeclAst = System.IntPtr;
using ConstAst = System.IntPtr;
using Value = System.IntPtr;
using PatternAst = System.IntPtr;
namespace Microsoft.Boogie.Z3
{
public class Z3apiProcessTheoremProver : ApiProverInterface
{
public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)
{
this.options = opts;
this.context = (Z3apiProverContext) ctxt;
this.numAxiomsPushed = 0;
}
private Z3InstanceOptions options;
private Z3apiProverContext context;
public override ProverContext Context
{
get { return context; }
}
public override VCExpressionGenerator VCExprGen
{
get { return context.ExprGen; }
}
private int numAxiomsPushed;
public override void Close()
{
base.Close();
context.CloseLog();
context.z3.Dispose();
context.config.Dispose();
}
public void PushAxiom(VCExpr axiom)
{
context.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
context.AddAxiom(axiom, linOptions);
}
private void PushConjecture(VCExpr conjecture)
{
context.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
context.AddConjecture(conjecture, linOptions);
}
public override void PushVCExpression(VCExpr vc)
{
PushAxiom(vc);
numAxiomsPushed++;
}
public void CreateBacktrackPoint()
{
context.CreateBacktrackPoint();
}
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
Push();
context.AddAxiom(context.Axioms, linOptions);
context.AddConjecture(vc, linOptions);
outcome = context.Check(out z3LabelModels);
Pop();
}
public override void Check()
{
outcome = context.Check(out z3LabelModels);
}
public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
outcome = context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
{
context.CreateBacktrackPoint();
}
public override void Pop()
{
context.Backtrack();
}
public override void Assert(VCExpr vc, bool polarity)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
if (polarity)
context.AddAxiom(vc, linOptions);
else
context.AddConjecture(vc, linOptions);
}
public override void AssertAxioms()
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
context.AddAxiom(context.Axioms, linOptions);
}
// Number of axioms pushed since the last call to FlushAxioms
public override int NumAxiomsPushed()
{
return numAxiomsPushed;
}
public override int FlushAxiomsToTheoremProver()
{
var ret = numAxiomsPushed;
numAxiomsPushed = 0;
return ret;
}
private Outcome outcome;
private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();
[NoDefaultContract]
public override Outcome CheckOutcome(ErrorHandler handler)
{
if (outcome == Outcome.Invalid)
{
foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
{
List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
}
}
return outcome;
}
private List<string> RemovePrefixes(List<string> labels)
{
List<string> result = new List<string>();
foreach (string label in labels)
{
if (label.StartsWith("+"))
{
result.Add(label.Substring(1));
}
else if (label.StartsWith("|"))
{
result.Add(label.Substring(1));
}
else if (label.StartsWith("@"))
{
result.Add(label.Substring(1));
}
else
throw new Exception("Unknown prefix in label " + label);
}
return result;
}
}
}
namespace Microsoft.Boogie.Z3api
{
public class Factory : ProverFactory
{
public override object SpawnProver(ProverOptions options, object ctxt)
{
return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);
}
public override object NewProverContext(ProverOptions opts)
{
if (CommandLineOptions.Clo.BracketIdsInVC < 0)
{
CommandLineOptions.Clo.BracketIdsInVC = 0;
}
VCExpressionGenerator gen = new VCExpressionGenerator();
return new Z3apiProverContext((Z3InstanceOptions)opts, gen);
}
public override ProverOptions BlankProverOptions()
{
return new Z3InstanceOptions();
}
}
}
|
