diff options
| author |  Ken McMillan <unknown> | 2013-06-14 17:23:44 -0700 |
|---|---|---|
| committer | Ken McMillan <unknown> | 2013-06-14 17:23:44 -0700 |
| commit | 4c7694f31f5a841a3d2eadc94c8e7f49aabbcc40 (patch) | |
| tree | 495aa31c76de499319035d32955e95699eab77a2 /Source/VCGeneration/Check.cs | |
| parent | 6a9e8449f14e8c3858ab0809036e68a0a43c2d4e (diff) | |
Fixes for duality under corral
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 90 |
1 files changed, 56 insertions, 34 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index e88c000e..6897a982 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -137,40 +137,7 @@ namespace Microsoft.Boogie { } else {
if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- TypeCtorDecl t = decl as TypeCtorDecl;
- if (t != null) {
- ctx.DeclareType(t, null);
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Constant c = decl as Constant;
- if (c != null) {
- ctx.DeclareConstant(c, c.Unique, null);
- } else {
- Function f = decl as Function;
- if (f != null) {
- ctx.DeclareFunction(f, null);
- }
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Axiom ax = decl as Axiom;
- if (ax != null) {
- ctx.AddAxiom(ax, null);
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- GlobalVariable v = decl as GlobalVariable;
- if (v != null) {
- ctx.DeclareGlobalVariable(v, null);
- }
- }
+ Setup(prog, ctx);
// we first generate the prover and then store a clone of the
// context in the cache, so that the prover can setup stuff in
@@ -184,6 +151,61 @@ namespace Microsoft.Boogie { this.gen = prover.VCExprGen;
}
+ public void Retarget(Program prog, ProverContext ctx)
+ {
+ ctx.Clear();
+ Setup(prog, ctx);
+ }
+
+ private static void Setup(Program prog, ProverContext ctx)
+ {
+ // set up the context
+ foreach (Declaration decl in prog.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ TypeCtorDecl t = decl as TypeCtorDecl;
+ if (t != null)
+ {
+ ctx.DeclareType(t, null);
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ Constant c = decl as Constant;
+ if (c != null)
+ {
+ ctx.DeclareConstant(c, c.Unique, null);
+ }
+ else
+ {
+ Function f = decl as Function;
+ if (f != null)
+ {
+ ctx.DeclareFunction(f, null);
+ }
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ Axiom ax = decl as Axiom;
+ if (ax != null)
+ {
+ ctx.AddAxiom(ax, null);
+ }
+ }
+ foreach (Declaration decl in prog.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ GlobalVariable v = decl as GlobalVariable;
+ if (v != null)
+ {
+ ctx.DeclareGlobalVariable(v, null);
+ }
+ }
+ }
+
/// <summary>
/// Clean-up.
|