The TPTP backend works for some very limited examples

5 files changed, 235 insertions, 319 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 0f7be0fd..286feb13 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -148,6 +148,10 @@
       <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Provers\TPTP\TPTP.csproj">

+      <Project>{A598ED5A-93AD-4125-A555-3921A2F936FA}</Project>

+      <Name>TPTP</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Provers\Z3\Z3.csproj">

       <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

       <Name>Z3</Name>

diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index d4bc7dc8..2b2590d1 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -23,6 +23,7 @@ namespace Microsoft.Boogie.TPTP
   public class TPTPProcessTheoremProver : LogProverInterface

   {

     private readonly DeclFreeProverContext ctx;

+    private readonly VCExpressionGenerator Gen;

 

     [ContractInvariantMethod]

     void ObjectInvariant()

@@ -31,7 +32,6 @@ namespace Microsoft.Boogie.TPTP
       Contract.Invariant(AxBuilder != null);

       Contract.Invariant(Namer != null);

       Contract.Invariant(DeclCollector != null);

-      Contract.Invariant(BadBenchmarkWords != null);

       Contract.Invariant(cce.NonNullElements(Axioms));

       Contract.Invariant(cce.NonNullElements(TypeDecls));

       Contract.Invariant(_backgroundPredicates != null);

@@ -47,23 +47,31 @@ namespace Microsoft.Boogie.TPTP
       Contract.Requires(options != null);

       Contract.Requires(gen != null);

       Contract.Requires(ctx != null);

-      InitializeGlobalInformation("UnivBackPred2.smt");

+

+      // No bg predicate at the moment

+      // InitializeGlobalInformation("UnivBackPred.tptp");

 

       this.ctx = ctx;

+      this.Gen = gen;

 

       TypeAxiomBuilder axBuilder;

       switch (CommandLineOptions.Clo.TypeEncodingMethod) {

         case CommandLineOptions.TypeEncoding.Arguments:

           axBuilder = new TypeAxiomBuilderArguments(gen);

+          axBuilder.Setup();

+          break;

+        case CommandLineOptions.TypeEncoding.Monomorphic:

+          axBuilder = new TypeAxiomBuilderPremisses(gen);

           break;

         default:

           axBuilder = new TypeAxiomBuilderPremisses(gen);

+          axBuilder.Setup();

           break;

       }

-      axBuilder.Setup();

       AxBuilder = axBuilder;

-      UniqueNamer namer = new UniqueNamer();

+      UniqueNamer namer = new UniqueNamer();      

       Namer = namer;

+      Namer.Spacer = "__";

       this.DeclCollector = new TypeDeclCollector(namer);

 

     }

@@ -98,10 +106,10 @@ namespace Microsoft.Boogie.TPTP
       TextWriter output = OpenOutputFile(descriptiveName);

       Contract.Assert(output != null);

 

-      string name =

-        MakeBenchmarkNameSafe(TPTPExprLineariser.MakeIdPrintable(descriptiveName));

-      Contract.Assert(name != null);

-      WriteLineAndLog(output, "(benchmark " + name);

+      WriteLineAndLog(output, "%------------------------------------------------------------------------------");

+      WriteLineAndLog(output, "% Boogie benchmark: " + descriptiveName);

+      WriteLineAndLog(output, "%------------------------------------------------------------------------------");

+

       WriteLineAndLog(output, _backgroundPredicates);

 

       if (!AxiomsAreSetup) {

@@ -109,7 +117,7 @@ namespace Microsoft.Boogie.TPTP
         AxiomsAreSetup = true;

       }

 

-      string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";

+      string vcString = "fof(vc, conjecture, " + VCExpr2String(vc, 1) + ").";

       string prelude = ctx.GetProverCommands(true);

       Contract.Assert(prelude != null);

       WriteLineAndLog(output, prelude);

@@ -118,36 +126,19 @@ namespace Microsoft.Boogie.TPTP
         Contract.Assert(s != null);

         WriteLineAndLog(output, s);

       }

+      int id = 0;

       foreach (string s in Axioms) {

         Contract.Assert(s != null);

-        WriteLineAndLog(output, ":assumption");

+        WriteLineAndLog(output, "fof(ax" + id++ + ", axiom,");

         WriteLineAndLog(output, s);

+        WriteLineAndLog(output, ").");

       }

 

       WriteLineAndLog(output, vcString);

-      WriteLineAndLog(output, ")");

 

       output.Close();

     }

 

-    // certain words that should not occur in the name of a benchmark

-    // because some solvers don't like them

-    private readonly static List<string/*!>!*/> BadBenchmarkWords = new List<string/*!*/>();

-    static TPTPProcessTheoremProver()

-    {

-      BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");

-    }

-

-    private string MakeBenchmarkNameSafe(string name)

-    {

-      Contract.Requires(name != null);

-      Contract.Ensures(Contract.Result<string>() != null);

-

-      for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2)

-        name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i + 1]);

-      return name;

-    }

-

     private TextWriter OpenOutputFile(string descriptiveName)

     {

       Contract.Requires(descriptiveName != null);

@@ -188,27 +179,30 @@ namespace Microsoft.Boogie.TPTP
         case CommandLineOptions.TypeEncoding.Arguments:

           eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);

           break;

+        case CommandLineOptions.TypeEncoding.Monomorphic:

+          eraser = null;

+          break;

         default:

           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);

           break;

-      }

-      Contract.Assert(eraser != null);

-      VCExpr exprWithoutTypes = eraser.Erase(expr, polarity);

+      }      

+      VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);

       Contract.Assert(exprWithoutTypes != null);

 

-      LetBindingSorter letSorter = new LetBindingSorter(gen);

-      Contract.Assert(letSorter != null);

-      VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);

-      Contract.Assert(sortedExpr != null);

-      VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

-      Contract.Assert(sortedAxioms != null);

+      var letImplier = new Let2ImpliesMutator(Gen);

+      var flattener = new TermFormulaFlattener(Gen);

+      var exprWithLet = flattener.Flatten(exprWithoutTypes);

+      var exprWithoutLet = letImplier.Mutate(exprWithLet);

+

+      var axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());

+      var axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);

 

-      DeclCollector.Collect(sortedAxioms);

-      DeclCollector.Collect(sortedExpr);

+      DeclCollector.Collect(axiomsWithoutLet);

+      DeclCollector.Collect(exprWithoutLet);

       FeedTypeDeclsToProver();

 

-      AddAxiom(TPTPExprLineariser.ToString(sortedAxioms, Namer));

-      string res = TPTPExprLineariser.ToString(sortedExpr, Namer);

+      AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer));

+      string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer);

       Contract.Assert(res != null);

 

       if (CommandLineOptions.Clo.Trace) {

@@ -252,7 +246,7 @@ namespace Microsoft.Boogie.TPTP
 

     ////////////////////////////////////////////////////////////////////////////

 

-    private static string _backgroundPredicates;

+    private static string _backgroundPredicates = "";

 

     static void InitializeGlobalInformation(string backgroundPred)

     {

diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs
index f1ac4f33..3e3e5ed2 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -106,30 +106,6 @@ void ObjectInvariant()
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    internal static string TypeToString(Type t) {

-      Contract.Requires(t != null);

-      Contract.Ensures(Contract.Result<string>() != null);

-

-      if (t.IsBool)

-        return "TermBool";

-      else if (t.IsInt)

-        return "Int";

-      else if (t.IsBv) {

-        Contract.Assert(false);

-        throw new cce.UnreachableException();

-      } // bitvectors are currently not handled for SMT-Lib solvers

-      else {

-        // at this point, only the types U, T should be left

-        System.IO.StringWriter buffer = new System.IO.StringWriter();

-        using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

-          t.Emit(stream);

-        }

-        return "boogie" + buffer.ToString();

-      }

-    }

-

-    /////////////////////////////////////////////////////////////////////////////////////

-

     public static string MakeIdPrintable(string s) {

       Contract.Requires(s != null);

       Contract.Ensures(Contract.Result<string>() != null);

@@ -150,41 +126,40 @@ void ObjectInvariant()
         break;

       }

 

-      string newS = "";

+      var res = new StringBuilder();

+      

       foreach (char ch in s) {

-        if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')

-          newS = newS + ch;

+        if (Char.IsLetterOrDigit(ch))

+          res.Append(ch);

         else

-          // replace everything else with a .

-          newS = newS + '.';

+          // replace everything else with a _

+          res.Append('_');

       }

 

-      // ensure that the first character is not . or _ (some SMT-solvers do

-      // not like that, e.g., yices and cvc3)

-      if (newS[0] == '.' || newS[0] == '_')

-        newS = "x" + newS;

+      return res.ToString();

+    }

 

-      return newS;

+    public static string Lowercase(string s)

+    {

+      if (char.IsLower(s[0])) return MakeIdPrintable(s);

+      else return MakeIdPrintable("x" + s);

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    /// <summary>

-    /// The name for logical conjunction in Simplify

-    /// </summary>

-    internal const string andName = "and"; // conjunction

-    internal const string orName = "or"; // disjunction

-    internal const string notName = "not"; // negation

-    internal const string impliesName = "implies"; // implication

-    internal const string iteName = "ite"; // if-then-else

-    internal const string iffName = "iff"; // logical equivalence

+    internal const string andName = "&"; // conjunction

+    internal const string orName = "|"; // disjunction

+    internal const string notName = "~"; // negation

+    internal const string impliesName = "=>"; // implication

+    internal const string iteName = "$itef"; // if-then-else

+    internal const string iffName = "<=>"; // logical equivalence

     internal const string eqName = "="; // equality

-    internal const string lessName = "<";

-    internal const string greaterName = ">";

-    internal const string atmostName = "<=";

-    internal const string atleastName = ">=";

-    internal const string TRUEName = "true"; // nullary predicate that is always true

-    internal const string FALSEName = "false"; // nullary predicate that is always false

+    internal const string lessName = "lt";

+    internal const string greaterName = "gt";

+    internal const string atmostName = "le";

+    internal const string atleastName = "ge";

+    internal const string TRUEName = "$true"; // nullary predicate that is always true

+    internal const string FALSEName = "$false"; // nullary predicate that is always false

     internal const string subtypeName = "UOrdering2";

     internal const string subtypeArgsName = "UOrdering3";

 

@@ -192,22 +167,10 @@ void ObjectInvariant()
 

     internal const string boolTrueName = "boolTrue";

     internal const string boolFalseName = "boolFalse";

-    internal const string boolAndName = "boolAnd";

-    internal const string boolOrName = "boolOr";

-    internal const string boolNotName = "boolNot";

-    internal const string boolIffName = "boolIff";

-    internal const string boolImpliesName = "boolImplies";

     internal const string boolIteName = "ite";

-    internal const string termUEqual = "UEqual";

-    internal const string termTEqual = "TEqual";

-    internal const string termIntEqual = "IntEqual";

-    internal const string termLessName = "intLess";

-    internal const string termGreaterName = "intGreater";

-    internal const string termAtmostName = "intAtMost";

-    internal const string termAtleastName = "intAtLeast";

-    internal const string intAddName = "+";

-    internal const string intSubName = "-";

-    internal const string intMulName = "*";

+    internal const string intAddName = "intAdd";

+    internal const string intSubName = "intSub";

+    internal const string intMulName = "intMul";

     internal const string intDivName = "boogieIntDiv";

     internal const string intModName = "boogieIntMod";

 

@@ -237,13 +200,8 @@ void ObjectInvariant()
         else if (node == VCExpressionGenerator.False)

           wr.Write("{0}", boolFalseName);

         else if (node is VCExprIntLit) {

-          // some SMT-solvers do not understand negative literals

-          // (e.g., yices)

           BigNum lit = ((VCExprIntLit)node).Val;

-          if (lit.IsNegative)

-            wr.Write("({0} 0 {1})", intSubName, lit.Abs);

-          else

-            wr.Write(lit);

+          wr.Write(lit);

         } else {

           Contract.Assert(false);

           throw new cce.UnreachableException();

@@ -279,14 +237,17 @@ void ObjectInvariant()
            op.Equals(VCExpressionGenerator.OrOp))) {

         // handle these operators without recursion

 

-        wr.Write("({0}",

-                 op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);

+        var sop = op.Equals(VCExpressionGenerator.AndOp) ? andName : orName;

+        wr.Write("(");

         IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);

         Contract.Assert(enumerator!=null);

+        var cnt = 0;

         while (enumerator.MoveNext()) {

           VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

           if (naryExpr == null || !naryExpr.Op.Equals(op)) {

-            wr.Write(" ");

+            if (cnt > 0)

+              wr.Write(" {0} ", sop);

+            cnt++;

             Linearise(cce.NonNull((VCExpr)enumerator.Current), options);

           }

         }

@@ -304,7 +265,7 @@ void ObjectInvariant()
     public bool Visit(VCExprVar node, LineariserOptions options) {

       //Contract.Requires(node != null);

       //Contract.Requires(options != null);

-      string printedName = Namer.GetName(node, MakeIdPrintable(node.Name));

+      string printedName = Namer.GetName(node, MakeIdPrintable(Lowercase(node.Name)));

       Contract.Assert(printedName!=null);

 

       if (options.AsTerm ||

@@ -312,7 +273,7 @@ void ObjectInvariant()
           printedName[0] == '$')

         wr.Write("{0}", printedName);

       else

-        wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName);

+        wr.Write("({0} = {1})", printedName, boolTrueName);

 

       return true;

     }

@@ -327,19 +288,22 @@ void ObjectInvariant()
 

       Namer.PushScope(); try {

 

-      string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";

-      wr.Write("({0} ", kind);

+      string kind = node.Quan == Quantifier.ALL ? "!" : "?";

+      wr.Write("{0} [", kind);

 

       for (int i = 0; i < node.BoundVars.Count; i++) 

         {

           VCExprVar var = node.BoundVars[i];

           Contract.Assert(var!=null);

           // ensure that the variable name starts with ?

-          string printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));

+          string printedName = Namer.GetLocalName(var, "V" + MakeIdPrintable(var.Name));

         Contract.Assert(printedName!=null);

-         Contract.Assert(printedName[0] == '?');

-          wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));

+         Contract.Assert(printedName[0] == 'V');

+         if (i > 0) wr.Write(",");

+          wr.Write("{0}", printedName);

         }

+

+      wr.Write("] : (");

         

       /*      if (options.QuantifierIds) {

         // only needed for Z3

@@ -358,7 +322,7 @@ void ObjectInvariant()
 

       Linearise(node.Body, options);

 

-      WriteTriggers(node.Triggers, options);

+      // WriteTriggers(node.Triggers, options);

       wr.Write(")");

 

       return true;

@@ -368,80 +332,12 @@ void ObjectInvariant()
       }

     }

 

-    private void WriteTriggers(List<VCTrigger/*!>!*/> triggers, LineariserOptions options) {

-      Contract.Requires(options != null);

-      Contract.Requires(triggers != null);

-      // first, count how many neg/pos triggers there are

-      int negTriggers = 0;

-      int posTriggers = 0;

-      foreach (VCTrigger vcTrig in triggers) {

-        Contract.Assert(vcTrig!=null);

-        if (vcTrig.Pos) {

-          posTriggers++;

-        } else {

-          negTriggers++;

-        }

-      }

-

-      if (posTriggers > 0) {

-        foreach (VCTrigger vcTrig in triggers) {

-          Contract.Assert(vcTrig!=null);

-          if (vcTrig.Pos) {

-            wr.Write(" :pat {");

-            foreach (VCExpr e in vcTrig.Exprs) {

-              Contract.Assert(e!=null);

-              wr.Write(" ");

-              LineariseAsTerm(e, options);

-            }

-            wr.Write(" } ");

-          }

-        }

-      } else if (negTriggers > 0) {

-        // if also positive triggers are given, the SMT solver (at least Z3)

-        // will ignore the negative patterns and output a warning. Therefore

-        // we never specify both negative and positive triggers

-        foreach (VCTrigger vcTrig in triggers) {

-          Contract.Assert(vcTrig!=null);

-          if (!vcTrig.Pos) {

-            wr.Write(" :nopat { ");

-           Contract.Assert(vcTrig.Exprs.Count == 1);

-            wr.Write(" ");

-            LineariseAsTerm(vcTrig.Exprs[0], options);

-            wr.Write(" } ");

-          }

-        }

-      }

-    }

+    

 

     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprLet node, LineariserOptions options) {

-      //Contract.Requires(node != null);

-      //Contract.Requires(options != null);

-      Namer.PushScope(); try {

-

-      foreach (VCExprLetBinding b in node) {

-        Contract.Assert(b != null);

-        bool formula = b.V.Type.IsBool;

-

-        wr.Write("({0} (", formula ? "flet" : "let");

-        string printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name));

-       Contract.Assert(printedName[0] == '$');

-        

-        wr.Write("{0} ", printedName);

-        Linearise(b.E, options.SetAsTerm(!formula));

-        wr.Write(") ");

-      }

-      Linearise(node.Body, options);

-

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

-        wr.Write(")");

-

-      return true;

-

-      } finally {

-        Namer.PopScope();

-      }

+      throw new NotImplementedException();

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

@@ -466,22 +362,13 @@ void ObjectInvariant()
       }

 

       ///////////////////////////////////////////////////////////////////////////////////

-

-      private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,

-                                    LineariserOptions options,

-                                    bool argsAsTerms) {

-      Contract.Requires(op != null);

-      Contract.Requires(cce.NonNullElements(args ));

-      Contract.Requires(options != null);

-        WriteApplication(op, op, args, options, argsAsTerms);

-      }

-

+     

       private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,

                                     LineariserOptions options) {

       Contract.Requires(op != null);

       Contract.Requires(cce.NonNullElements(args ));

       Contract.Requires(options != null);

-        WriteApplication(op, op, args, options, options.AsTerm);

+        WriteApplication(op, args, options, options.AsTerm);

       }

 

       private void WriteTermApplication(string op, IEnumerable<VCExpr/*!>!*/> args,

@@ -490,45 +377,55 @@ void ObjectInvariant()
       Contract.Requires(cce.NonNullElements(args ));

       Contract.Requires(options != null);

         ExprLineariser.AssertAsTerm(op, options);

-        WriteApplication(op, op, args, options, options.AsTerm);

+        WriteApplication(op, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string termOp, string predOp,

-                                    IEnumerable<VCExpr/*!>!*/> args, LineariserOptions options) {

-        Contract.Requires(predOp != null);

-        Contract.Requires(termOp != null);

-      Contract.Requires(cce.NonNullElements(args ));

-      Contract.Requires(options != null);

-        WriteApplication(termOp, predOp, args, options, options.AsTerm);

-      }

-

-      private void WriteApplication(string termOp, string predOp,

+   

+      private void WriteApplication(string termOp,

                                     IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,

                                     // change the AsTerm option for the arguments?

                                     bool argsAsTerms) {

-      Contract.Requires(predOp != null);

         Contract.Requires(termOp != null);

       Contract.Requires(cce.NonNullElements(args ));

       Contract.Requires(options != null);

-        string opName = options.AsTerm ? termOp : predOp;

-        Contract.Assert(opName!=null);

         LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);

         Contract.Assert(newOptions!=null);

 

-        bool hasArgs = false;

-        foreach (VCExpr e in args) {

-          Contract.Assert(e!=null);

-          if (!hasArgs)

-            wr.Write("({0}", opName);

-          wr.Write(" ");

-          ExprLineariser.Linearise(e, newOptions);

-          hasArgs = true;

-        }

-        

-        if (hasArgs)

+        var argCnt = 0;

+        if (termOp == "~") {

+          wr.Write("(~ ");

+          foreach (var e in args) {

+            ExprLineariser.Linearise(e, newOptions);

+            argCnt++;

+          }

+          Contract.Assert(argCnt == 1);

           wr.Write(")");

-        else

-          wr.Write("{0}", opName);

+        } else if ("&|~=><".IndexOf(termOp[0]) >= 0) {

+          wr.Write("(");

+          foreach (var e in args) {

+            ExprLineariser.Linearise(e, newOptions);

+            argCnt++;

+            if (argCnt == 1) {

+              wr.Write(" {0} ", termOp);

+            }

+          }

+          Contract.Assert(argCnt == 2);

+          wr.Write(")");

+        } else {

+          wr.Write(termOp);

+          foreach (var e in args) {

+            Contract.Assert(e != null);

+            if (argCnt == 0)

+              wr.Write("(");

+            else

+              wr.Write(", ");

+            argCnt++;

+            ExprLineariser.Linearise(e, newOptions);            

+          }

+

+          if (argCnt > 0)

+            wr.Write(")");

+        }

       }

 

       // write an application that can only be a term.

@@ -542,12 +439,12 @@ void ObjectInvariant()
         if (!options.AsTerm)

           // Write: (EQ (f args) |@true|)

           // where "args" are written as terms

-          wr.Write("({0} ", eqName);

+          wr.Write("(", eqName);

 

         WriteApplication(termOp, args, options, true);

 

         if (!options.AsTerm)

-          wr.Write(" {0})", boolTrueName);

+          wr.Write(" = {0})", boolTrueName);

       }

 

       ///////////////////////////////////////////////////////////////////////////////////

@@ -555,7 +452,7 @@ void ObjectInvariant()
       public bool VisitNotOp      (VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

-        WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas

+        WriteApplication(notName, node, options);      // arguments can be both terms and formulas

         return true;

       }

 

@@ -563,23 +460,7 @@ void ObjectInvariant()
         Contract.Requires(node != null);

         Contract.Requires(options != null);

         if (options.AsTerm) {

-          // use equality on terms, also if the arguments have type bool

-         Contract.Assert(node[0].Type.Equals(node[1].Type));

-          if (node[0].Type.IsBool) {

-            WriteApplication(boolIffName, node, options);

-          } else if (node[0].Type.IsInt) {

-            WriteApplication(termIntEqual, node, options);

-          } else {

-            // TODO: make this less hackish

-            CtorType t = node[0].Type as CtorType;

-            if (t != null && t.Decl.Name.Equals("U")) {

-              WriteApplication(termUEqual, node, options);

-            } else if (t != null && t.Decl.Name.Equals("T")) {

-              WriteApplication(termTEqual, node, options);

-            } else {

-             {Contract.Assert(false);  throw new cce.UnreachableException();}   // unknown type

-            }

-          }

+          throw new NotImplementedException();

         } else {

           if (node[0].Type.IsBool) {

            Contract.Assert(node[1].Type.IsBool);

@@ -603,7 +484,7 @@ void ObjectInvariant()
       public bool VisitNeqOp      (VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

-        wr.Write("({0} ", options.AsTerm ? boolNotName : notName);

+        wr.Write("(~ ");

         PrintEq(node, options);

         wr.Write(")");

         return true;

@@ -613,7 +494,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        Contract.Assert(options.AsTerm);

-        WriteApplication(boolAndName, andName, node, options);

+        WriteApplication(andName, node, options);

         return true;

       }

 

@@ -622,7 +503,7 @@ void ObjectInvariant()
         //Contract.Requires(options != null);

         

         Contract.Assert(options.AsTerm);

-        WriteApplication(boolOrName, orName, node, options);

+        WriteApplication(orName, node, options);

         return true;

       }

 

@@ -630,16 +511,14 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        WriteApplication(boolImpliesName, impliesName, node, options);

+        WriteApplication(impliesName, node, options);

         return true;

       }

 

       public bool VisitIfThenElseOp  (VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

-       

-        WriteApplication(boolIteName, iteName, node, options);

-        return true;

+        throw new NotImplementedException();

       }

 

       public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {

@@ -660,11 +539,23 @@ void ObjectInvariant()
         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

-          wr.Write("({0}", distinctName);

+          var bits = 0;

+          var cnt = node.Length;

+          while (cnt > 0) {

+            cnt >>= 1;

+            bits++;

+          }

+

+          wr.Write("($true ");

           foreach (VCExpr e in node) {

-            Contract.Assert(e!=null);

-            wr.Write(" ");

-            ExprLineariser.LineariseAsTerm(e, options);

+            for (var i = 0; i < bits; ++i) {

+              var neg = (cnt & (1 >> i)) != 0 ? "~" : "";

+              wr.Write(" & {0}distinct__f__{1}(", neg, i);

+              ExprLineariser.LineariseAsTerm(e, options);

+              wr.Write(")");

+            }

+            wr.WriteLine();

+            cnt++;

           }

           wr.Write(")");

         }

@@ -684,18 +575,38 @@ void ObjectInvariant()
         return true;

       }

 

-      public bool VisitSelectOp   (VCExprNAry node, LineariserOptions options) {

-        //Contract.Requires(node != null);

+      public bool VisitSelectOp(VCExprNAry node, LineariserOptions options)

+      {

         //Contract.Requires(options != null);

-       

-       {Contract.Assert(false);  throw new cce.UnreachableException();}      // should not occur in the output

+        //Contract.Requires(node != null);

+        var name = Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));

+        wr.Write(name + "(");

+        var cnt = 0;

+        foreach (VCExpr/*!*/ e in node) {

+          Contract.Assert(e != null);

+          if (cnt++ > 0)

+            wr.Write(", ");

+          ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

+        }

+        wr.Write(")");

+        return true;

       }

 

-      public bool VisitStoreOp    (VCExprNAry node, LineariserOptions options) {

-        //Contract.Requires(node != null);

+      public bool VisitStoreOp(VCExprNAry node, LineariserOptions options)

+      {

         //Contract.Requires(options != null);

-       

-       {Contract.Assert(false);  throw new cce.UnreachableException();}       // should not occur in the output

+        //Contract.Requires(node != null);

+        var name = Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));

+        wr.Write(name + "(");

+        var cnt = 0;

+        foreach (VCExpr e in node) {

+          Contract.Assert(e != null);

+          if (cnt++ > 0)

+            wr.Write(", ");

+          ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

+        }

+        wr.Write(")");

+        return true;

       }

 

       public bool VisitBvOp       (VCExprNAry node, LineariserOptions options) {

@@ -763,7 +674,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms

+        WriteApplication(lessName, node, options, true);  // arguments are always terms

         return true;

       }

 

@@ -771,7 +682,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms

+        WriteApplication(atmostName, node, options, true);  // arguments are always terms

         return true;

       }

 

@@ -779,7 +690,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms

+        WriteApplication(greaterName, node, options, true);  // arguments are always terms

         return true;

       }

 

@@ -787,7 +698,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms

+        WriteApplication(atleastName, node, options, true);  // arguments are always terms

         return true;

       }

 

@@ -813,7 +724,7 @@ void ObjectInvariant()
        

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op!=null);

-        string printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));

+        string printedName = ExprLineariser.Namer.GetName(op.Func, Lowercase(op.Func.Name));

         Contract.Assert(printedName!=null);

 

         // arguments are always terms

diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs
index ab14c0e2..0d0eb19a 100644
--- a/Source/Provers/TPTP/TypeDeclCollector.cs
+++ b/Source/Provers/TPTP/TypeDeclCollector.cs
@@ -17,6 +17,9 @@ namespace Microsoft.Boogie.TPTP
 

   public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

 

+    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions = new Dictionary<string, bool>();

+    private readonly Dictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions = new Dictionary<string, bool>();

+

     private readonly UniqueNamer Namer;

     [ContractInvariantMethod]

 void ObjectInvariant() 

@@ -77,55 +80,57 @@ void ObjectInvariant()
 

     ///////////////////////////////////////////////////////////////////////////

 

-    private static string TypeToString(Type t) {

-      Contract.Requires(t != null);

-      Contract.Ensures(Contract.Result<string>() != null);

-

-      return TPTPExprLineariser.TypeToString(t);

-    }

-

+  

     public override bool Visit(VCExprNAry node, bool arg) {

       Contract.Requires(node != null);

-      // there are a couple of cases where operators have to be

-      // registered by generating appropriate statements

-

-      VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-      if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

-        Function f = op.Func;

-        Contract.Assert(f!=null);

-        string printedName = Namer.GetName(f, TPTPExprLineariser.MakeIdPrintable(f.Name));

-        Contract.Assert(printedName!=null);

-        string decl = ":extrafuns ((" + printedName;

-

-        foreach (Variable v in f.InParams) {

-          Contract.Assert(v!=null);

-          decl += " " + TypeToString(v.TypedIdent.Type);

-        }

-       Contract.Assert(f.OutParams.Length == 1);

-        foreach (Variable v in f.OutParams) {

-          Contract.Assert(v!=null);

-          decl += " " + TypeToString(v.TypedIdent.Type);

-        }

 

-        decl += "))";

-        

-        AddDeclaration(decl);

-        KnownFunctions.Add(f, true);

+      if (node.Op is VCExprStoreOp) {

+        string name = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));

+        if (!KnownStoreFunctions.ContainsKey(name)) {

+          var id = KnownStoreFunctions.Count;

+

+          if (CommandLineOptions.Clo.MonomorphicArrays) {

+            var sel = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));

+

+            var eq = "=";

+            if (node[node.Arity - 1].Type.IsBool)

+              eq = "<=>";

+

+            string xS = "", yS = "";

+            string dist = "";

+

+            for (int i = 0; i < node.Arity - 2; i++) {

+              if (i != 0) {

+                dist += " | ";

+                xS += ",";

+                yS += ",";

+              }

+              var x = "X" + i;

+              var y = "Y" + i;

+              xS += x;

+              yS += y;

+              dist += string.Format("({0} != {1})", x, y);

+            }

+

+            string ax1 = "fof(selectEq" + id + ", axiom, ! [M,V," + xS + "] : (" +

+                             string.Format("{0}({1}(M,{2},V),{2}) = V", sel, name, xS) + ")).";

+            string ax2 = "fof(selectNeq" + id + ", axiom, ! [M,V," + xS + "," + yS + "] : (" +

+                             string.Format("( {0} ) => ", dist) +

+                             string.Format("{0}({1}(M,{2},V),{3}) = {0}(M,{3})", sel, name, xS, yS) + ")).";

+

+            AddDeclaration(ax1);

+            AddDeclaration(ax2);

+          }

+

+          KnownStoreFunctions.Add(name, true);

+        }

+        //

       }

 

       return base.Visit(node, arg);

     }

 

     public override bool Visit(VCExprVar node, bool arg) {

-      Contract.Requires(node != null);

-      if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

-        string printedName = Namer.GetName(node, TPTPExprLineariser.MakeIdPrintable(node.Name));

-        Contract.Assert(printedName!=null);

-        string decl =

-          ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";

-        AddDeclaration(decl);

-        KnownVariables.Add(node, true);

-      }

 

       return base.Visit(node, arg);

     }

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index 557171d1..bfccdb3a 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -20,6 +20,7 @@ namespace Microsoft.Boogie.VCExprAST {
   using TEHelperFuns = Microsoft.Boogie.TypeErasure.HelperFuns;

 

   public class UniqueNamer : ICloneable {

+    public string Spacer = "@@";

 

     public UniqueNamer() {

       GlobalNames = new Dictionary<Object, string>();

@@ -32,6 +33,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

     private UniqueNamer(UniqueNamer namer) {

       Contract.Requires(namer != null);

+      Spacer = namer.Spacer;

       GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);

 

       List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ localNames =

@@ -102,7 +104,7 @@ namespace Microsoft.Boogie.VCExprAST {
       int counter;

 

       if (CurrentCounters.TryGetValue(baseName, out counter)) {

-        candidate = baseName + "@@" + counter;

+        candidate = baseName + Spacer + counter;

         counter = counter + 1;

       } else {

         candidate = baseName;

@@ -111,7 +113,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

       bool dummy;

       while (UsedNames.TryGetValue(candidate, out dummy)) {

-        candidate = baseName + "@@" + counter;

+        candidate = baseName + Spacer + counter;

         counter = counter + 1;

       }

 

@@ -172,7 +174,7 @@ namespace Microsoft.Boogie.VCExprAST {
       string name;

       if (GlobalPlusLocalNames.TryGetValue(thingie, out name))

         return name;

-      return "@@undefined@@" + thingie.GetHashCode() + "@@";

+      return Spacer + "undefined" + Spacer + thingie.GetHashCode() + Spacer;

     }

   }

 }