Boogie: Get rid of {:inline} attributes on axioms

3 files changed, 4 insertions, 153 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0b40c86e..8f51aac8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -312,9 +312,6 @@ namespace Microsoft.Boogie {
           seeker.Visit(d);

         }

       }

-

-      AxiomExpander expander = new AxiomExpander(this, tc);

-      expander.CollectExpansions();

     }

 

     public void ComputeStronglyConnectedComponents() {

@@ -1796,13 +1793,7 @@ namespace Microsoft.Boogie {
 

     // the body is only set if the function is declared with {:inline}

     public Expr Body;

-    public List<Expansion/*!*/> expansions;

     public bool doingExpansion;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(expansions, true));

-    }

-

 

     private bool neverTrigger;

     private bool neverTriggerComputed;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index de1fdb00..16b988c9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1856,14 +1856,6 @@ namespace Microsoft.Boogie {
       one of them to keep; otherwise, Boogie ignore the :extern declaration

       and keeps the other.

 

-  ---- On axioms -------------------------------------------------------------

-

-    {:inline true}

-      Works on axiom of the form:

-        (forall VARS :: f(VARS) = expr(VARS))

-      Makes Boogie replace f(VARS) with expr(VARS) everywhere just before

-      doing VC generation.

-

   ---- On implementations and procedures -------------------------------------

 

      {:inline N}

@@ -1897,6 +1889,10 @@ namespace Microsoft.Boogie {
      {:bvbuiltin ""spec""}

        Rewrite the function to built-in prover function symbol 'fn'.

 

+     {:inline}

+     {:inline true}

+       Expand function according to its definition before going to the prover.

+

      {:never_pattern true}

        Terms starting with this function symbol will never be

        automatically selected as patterns. It does not prevent them

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 802fd390..d9c33bd4 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -601,140 +601,4 @@ namespace Microsoft.Boogie {
       }

     }

   } // end class CodeCopier

-

-

-  public class AxiomExpander : Duplicator {

-    readonly Program/*!*/ program;

-    readonly TypecheckingContext/*!*/ tc;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(program != null);

-      Contract.Invariant(tc != null);

-    }

-

-

-    public AxiomExpander(Program prog, TypecheckingContext t) {

-      Contract.Requires(t != null);

-      Contract.Requires(prog != null);

-      program = prog;

-      tc = t;

-    }

-

-    public void CollectExpansions() {

-      foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

-        Contract.Assert(decl != null);

-        Axiom ax = decl as Axiom;

-        if (ax != null) {

-          bool expand = false;

-          if (!ax.CheckBooleanAttribute("inline", ref expand)) {

-            Error(decl.tok, "{:inline ...} expects either true or false as the argument");

-          }

-          if (expand) {

-            AddExpansion(ax.Expr, ax.FindStringAttribute("ignore"));

-          }

-        }

-        Function f = decl as Function;

-        if (f != null && f.Body != null) {

-          Variable[]/*!*/ formals = new Variable[f.InParams.Length];

-          Contract.Assert(formals != null);

-          for (int i = 0; i < formals.Length; ++i)

-            formals[i] = f.InParams[i];

-          AddExpansion(f, new Expansion(null, f.Body,

-                                        new TypeVariableSeq(f.TypeParameters),

-                                        formals));

-        }

-      }

-    }

-

-    void Error(IToken tok, string msg) {

-      Contract.Requires(tok != null);

-      tc.Error(tok, "expansion: " + msg);

-    }

-

-    void AddExpansion(Expr axiomBody, string ignore) {

-      Contract.Requires(axiomBody != null);

-      // it would be sooooooooo much easier with pattern matching

-      ForallExpr all = axiomBody as ForallExpr;

-      if (all != null) {

-        NAryExpr nary = all.Body as NAryExpr;

-        BinaryOperator bin = nary == null ? null : nary.Fun as BinaryOperator;

-        //System.Console.WriteLine("{0} {1} {2}", nary==null, bin==null, bin==null?0 : bin.Op);

-        if (nary != null && bin != null && (bin.Op == BinaryOperator.Opcode.Eq || bin.Op == BinaryOperator.Opcode.Iff)) {

-

-          NAryExpr func = nary.Args[0] as NAryExpr;

-          //System.Console.WriteLine("{0} {1}", func == null, func == null ? null : func.Fun.GetType());

-          while (func != null && func.Fun is TypeCoercion)

-            func = func.Args[0] as NAryExpr;

-          if (func != null && func.Fun is FunctionCall) {

-            Function fn = cce.NonNull((FunctionCall)func.Fun).Func;

-            Expansion exp = new Expansion(ignore, cce.NonNull(nary.Args[1]),

-                                          new TypeVariableSeq(),

-                                          new Variable[func.Args.Length]);

-            int pos = 0;

-            HashSet<Declaration> parms = new HashSet<Declaration>();

-            foreach (Expr/*!*/ e in func.Args) {

-              Contract.Assert(e != null);

-              IdentifierExpr id = e as IdentifierExpr;

-              if (id == null) {

-                Error(e.tok, "only identifiers supported as function arguments");

-                return;

-              }

-              exp.formals[pos++] = id.Decl;

-              if (parms.Contains(id.Decl)) {

-                Error(all.tok, "an identifier was used more than once");

-                return;

-              }

-              parms.Add(id.Decl);

-              if (!all.Dummies.Has(id.Decl)) {

-                Error(all.tok, "identifier was not quantified over");

-                return;

-              }

-            }

-            if (func.Args.Length != all.Dummies.Length) {

-              Error(all.tok, "more variables quantified over, than used in function");

-              return;

-            }

-

-            HashSet<TypeVariable/*!*/> typeVars = new HashSet<TypeVariable/*!*/>();

-            foreach (TypeVariable/*!*/ v in cce.NonNull(func.TypeParameters).FormalTypeParams) {

-              Contract.Assert(v != null);

-              if (!func.TypeParameters[v].IsVariable) {

-                Error(all.tok, "only identifiers supported as type parameters");

-                return;

-              }

-              TypeVariable/*!*/ formal = func.TypeParameters[v].AsVariable;

-              Contract.Assert(formal != null);

-              exp.TypeParameters.Add(formal);

-              if (typeVars.Contains(formal)) {

-                Error(all.tok, "an identifier was used more than once");

-                return;

-              }

-              typeVars.Add(formal);

-              if (!all.TypeParameters.Has(formal)) {

-                Error(all.tok, "identifier was not quantified over");

-                return;

-              }

-            }

-            if (((FunctionCall)func.Fun).Func.TypeParameters.Length != all.TypeParameters.Length) {

-              Error(all.tok, "more variables quantified over, than used in function");

-              return;

-            }

-            AddExpansion(fn, exp);

-            return;

-          }

-        }

-      }

-

-      Error(axiomBody.tok, "axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))");

-    }

-

-    void AddExpansion(Function fn, Expansion x) {

-      Contract.Requires(x != null);

-      Contract.Requires(fn != null);

-      if (fn.expansions == null) {

-        fn.expansions = new List<Expansion/*!*/>();

-      }

-      fn.expansions.Add(x);

-    }

-  }

 } // end namespace
\ No newline at end of file