Boogie\VCGeneration: Renaming sources in preparation for my addition of the ported C# version

1 files changed, 200 insertions, 0 deletions

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
new file mode 100644
index 00000000..2db00964
--- /dev/null
+++ b/Source/VCGeneration/Context.cs
@@ -0,0 +1,200 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.IO;

+using System.Text;

+using Microsoft.Contracts;

+using Microsoft.Boogie.VCExprAST;

+

+namespace Microsoft.Boogie

+{

+  /// <summary>

+  /// The methods of this class are called in the following order:

+  ///   DeclareType*

+  ///   (DeclareConstant DeclareFunction)*

+  ///   AddAxiom*

+  ///   DeclareGlobalVariable*

+  /// At this time, all "attributes" are passed in as null.

+  /// </summary>

+  public abstract class ProverContext : ICloneable {

+    protected virtual void ProcessDeclaration(Declaration! decl) {}

+    public virtual void DeclareType(TypeCtorDecl! t, string attributes) { ProcessDeclaration(t); }

+    public virtual void DeclareConstant(Constant! c, bool uniq, string attributes) { ProcessDeclaration(c); }

+    public virtual void DeclareFunction(Function! f, string attributes) { ProcessDeclaration(f); }

+    public virtual void AddAxiom(Axiom! a, string attributes) { ProcessDeclaration(a); }

+    public abstract void AddAxiom(VCExpr! vc);

+    public virtual void DeclareGlobalVariable(GlobalVariable! v, string attributes) { ProcessDeclaration(v); }

+    

+    public abstract VCExpressionGenerator! ExprGen { get; }

+    public abstract Boogie2VCExprTranslator! BoogieExprTranslator { get; }

+    public abstract VCGenerationOptions! VCGenOptions { get; }

+

+    public abstract object! Clone();

+  }

+  

+  // -----------------------------------------------------------------------------------------------

+  // -----------------------------------------------------------------------------------------------

+  // -----------------------------------------------------------------------------------------------

+  

+  /// <summary>

+  /// This ProverContext subclass is intended for use with untyped provers that do not require names

+  /// to be declared before use.  It constructs its context from unique constants and given axioms.

+  /// </summary>

+  public class DeclFreeProverContext : ProverContext {

+    protected VCExpressionGenerator! gen;

+    protected VCGenerationOptions! genOptions;

+    protected Boogie2VCExprTranslator! translator;

+    

+    protected OrderingAxiomBuilder! orderingAxiomBuilder;

+

+    StringBuilder! proverCommands;

+    StringBuilder! incrementalProverCommands;

+    

+    protected List<Variable!>! distincts;

+    protected List<VCExpr!>! axiomConjuncts;

+

+    public VCExprTranslator exprTranslator;

+

+    public DeclFreeProverContext(VCExpressionGenerator! gen,

+                                 VCGenerationOptions! genOptions) {

+      this.gen = gen;

+      this.genOptions = genOptions;

+      Boogie2VCExprTranslator! t = new Boogie2VCExprTranslator (gen, genOptions);

+      this.translator = t;

+      OrderingAxiomBuilder! oab = new OrderingAxiomBuilder(gen, t);

+      oab.Setup();

+      this.orderingAxiomBuilder = oab;

+

+      proverCommands = new StringBuilder();

+      incrementalProverCommands = new StringBuilder();

+    

+      distincts = new List<Variable!>();

+      axiomConjuncts = new List<VCExpr!>();

+

+      exprTranslator = null;

+    }

+

+    private DeclFreeProverContext(DeclFreeProverContext! ctxt) {

+      this.gen = ctxt.gen;

+      this.genOptions = ctxt.genOptions;

+      Boogie2VCExprTranslator! t = (Boogie2VCExprTranslator)ctxt.translator.Clone();

+      this.translator = t;

+      this.orderingAxiomBuilder = new OrderingAxiomBuilder(ctxt.gen, t, ctxt.orderingAxiomBuilder);

+

+      StringBuilder! cmds = new StringBuilder ();

+      cmds.Append(ctxt.proverCommands);

+      proverCommands = cmds;

+      StringBuilder! incCmds = new StringBuilder ();

+      incCmds.Append(ctxt.incrementalProverCommands);

+      incrementalProverCommands = incCmds;

+    

+      distincts = new List<Variable!>(ctxt.distincts);

+      axiomConjuncts = new List<VCExpr!>(ctxt.axiomConjuncts);

+

+      if (ctxt.exprTranslator == null)

+        exprTranslator = null;

+      else

+        exprTranslator = (VCExprTranslator!)ctxt.exprTranslator.Clone();

+    }

+

+    public override object! Clone() {

+      return new DeclFreeProverContext(this);

+    }

+

+    internal protected void SayToProver(string! msg)

+    {

+      msg = msg + "\r\n";

+      proverCommands.Append(msg);

+      incrementalProverCommands.Append(msg);

+    }

+

+    protected override void ProcessDeclaration(Declaration! decl)

+    {

+      for (QKeyValue a = decl.Attributes; a != null; a = a.Next) {

+        if (a.Key == "prover" && a.Params.Count == 1) {

+          string cmd = a.Params[0] as string;

+          if (cmd != null) {

+            int pos = cmd.IndexOf(':');

+            if (pos <= 0)

+              throw new ProverException("Invalid syntax of :prover string: `" + cmd + "'");

+            string kind = cmd.Substring(0, pos);

+            if (genOptions.IsAnyProverCommandSupported(kind))

+              SayToProver(cmd.Substring(pos + 1));

+          }

+        }

+      }

+    }

+    

+    public override void DeclareFunction(Function! f, string attributes) {

+      base.ProcessDeclaration(f);

+    }

+

+    public override void DeclareConstant(Constant! c, bool uniq, string attributes) {

+      base.DeclareConstant(c, uniq, attributes);

+      orderingAxiomBuilder.AddConstant(c);

+

+      // TODO: make separate distinct lists for names coming from different types

+      // e.g., one for strings, one for ints, one for program types.

+      if (uniq){

+        distincts.Add(c);

+      }

+    }

+    

+    public override void AddAxiom(Axiom! ax, string attributes) {

+      base.AddAxiom(ax, attributes);

+

+      string ignore = ax.FindStringAttribute("ignore");

+      if (ignore != null && genOptions.IsAnyProverCommandSupported(ignore)) {

+        return;

+      }

+

+      axiomConjuncts.Add(translator.Translate(ax.Expr));

+    }

+

+    public override void AddAxiom(VCExpr! vc)

+    {

+      axiomConjuncts.Add(vc);

+    }

+

+    public VCExpr! Axioms {

+      get {

+        VCExpr axioms = gen.NAry(VCExpressionGenerator.AndOp, axiomConjuncts);

+        List<VCExpr!>! distinctVars = new List<VCExpr!> ();

+        foreach (Variable! v in distincts)

+          distinctVars.Add(translator.LookupVariable(v));

+        axioms = gen.AndSimp(gen.Distinct(distinctVars), axioms);

+        if (CommandLineOptions.Clo.TypeEncodingMethod != CommandLineOptions.TypeEncoding.Monomorphic)

+          axioms = gen.AndSimp(orderingAxiomBuilder.Axioms, axioms);

+        return axioms;

+      }

+    }

+

+    public string! GetProverCommands(bool full) {

+      string! res = (full ? proverCommands : incrementalProverCommands).ToString();

+      incrementalProverCommands.Length = 0;

+      return res;

+    }

+

+    public override VCExpressionGenerator! ExprGen { get {

+     return gen;

+    } }

+    public override Boogie2VCExprTranslator! BoogieExprTranslator { get {

+      return translator;

+    } }

+    public override VCGenerationOptions! VCGenOptions { get {

+      return genOptions;

+    } }

+  }

+

+  // Translator from VCExpressions to strings, which are implemented

+  // by the various provers

+  public abstract class VCExprTranslator : ICloneable {

+    public abstract string! translate(VCExpr! expr, int polarity);

+    public abstract string! Lookup(VCExprVar! var);

+    public abstract Object! Clone();    

+  }

+}