Move name-quoting (already for SMT2 not SMT1) into a seprate class

6 files changed, 141 insertions, 58 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index fff7e1b3..d7251f09 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -128,7 +128,7 @@ void ObjectInvariant()
       Contract.Assert(output!=null);

 

       string name =

-        MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName));

+        MakeBenchmarkNameSafe(SMTLibNamer.QuoteId(descriptiveName));

       Contract.Assert(name!=null);

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

       WriteLineAndLog(output, _backgroundPredicates);

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 70391710..7e0ed5e7 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -109,6 +109,7 @@
   <ItemGroup>

     <Compile Include="ProverInterface.cs" />

     <Compile Include="SMTLibLineariser.cs" />

+    <Compile Include="SMTLibNamer.cs" />

     <Compile Include="TypeDeclCollector.cs" />

     <Compile Include="..\..\version.cs" />

   </ItemGroup>

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7b5e51b0..d7b6bb7f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -114,7 +114,7 @@ void ObjectInvariant()
       Contract.Ensures(Contract.Result<string>() != null);

 

       if (t.IsBool)

-        return "TermBool";

+        return "Bool";

       else if (t.IsInt)

         return "Int";

       else if (t.IsBv) {

@@ -127,49 +127,11 @@ void ObjectInvariant()
         using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

           t.Emit(stream);

         }

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

+        return SMTLibNamer.QuoteId("T@" + buffer.ToString());

       }

     }

 

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

-

-    public static string MakeIdPrintable(string s) {

-      Contract.Requires(s != null);

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

-

-      // make sure that no keywords are used as identifiers

-      switch(s) {

-      case andName:

-      case orName:

-      case notName:

-      case impliesName:

-      case iffName:

-      case eqName:

-      case distinctName:

-      case TRUEName:

-      case FALSEName:

-      case "Array":

-        s = "nonkeyword_" + s;

-        break;

-      }

-

-      string newS = "";

-      foreach (char ch in s) {

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

-          newS = newS + ch;

-        else

-          // replace everything else with a .

-          newS = newS + '.';

-      }

-

-      // 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 newS;

-    }

-

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

 

     /// <summary>

@@ -307,7 +269,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.GetQuotedName(node, node.Name);

       Contract.Assert(printedName!=null);

 

       if (options.AsTerm ||

@@ -336,11 +298,9 @@ void ObjectInvariant()
       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));

-        Contract.Assert(printedName!=null);

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

+          Contract.Assert(var!=null);          

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

+        Contract.Assert(printedName!=null);         

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

         }

         

@@ -427,9 +387,8 @@ void ObjectInvariant()
         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} (let");

+        string printedName = Namer.GetQuotedName(b.V, b.V.Name);

         

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

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

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

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

         var name = SimplifyLikeExprLineariser.SelectOpName(node);

-        name = ExprLineariser.Namer.GetName(name, MakeIdPrintable(name));

+        name = ExprLineariser.Namer.GetQuotedName(name, name);

 

         wr.Write("(" + name);

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

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

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

         var name = SimplifyLikeExprLineariser.StoreOpName(node);

-        name = ExprLineariser.Namer.GetName(name, MakeIdPrintable(name));

+        name = ExprLineariser.Namer.GetQuotedName(name, name);

 

         wr.Write("(" + name);

         foreach (VCExpr e in node) {

@@ -846,7 +805,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.GetQuotedName(op.Func, op.Func.Name);

         Contract.Assert(printedName!=null);

 

         if (ExprLineariser.ProverOptions.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool) {

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
new file mode 100644
index 00000000..a3528362
--- /dev/null
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -0,0 +1,113 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie.VCExprAST;

+

+namespace Microsoft.Boogie.SMTLib

+{

+  public class SMTLibNamer : UniqueNamer

+  {

+    // The following Boogie ID characters are not SMT ID characters: `'\#

+    const string idCharacters = "~!@$%^&*_-+=<>.?/";

+

+    static string[] reservedSmtWordsList = 

+    { // Basic symbols:

+      "", "!", "_", "as", "DECIMAL", "exists", "forall", "let", "NUMERAL", "par", "STRING", 

+      // Commands:

+      "assert", "check-sat", "declare-sort", "declare-fun", "define-sort,", "define-fun", "exit",

+      "get-assertions", "get-assignment", "get-info", "get-option,", "get-proof", "get-unsat-core",

+      "get-value", "pop", "push", "set-logic", "set-info", "set-option",

+      // Core theory:

+      "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool",

+      "=>", // implies (sic!)

+      // Integers

+      "Int", "*", "/", "-", "+", "<", "<=", ">", ">=",

+      // SMT v1 stuff

+      "flet", "implies", "!=", "if_then_else",

+      // Z3 extensions

+      "lblneg", "lblpos", "lbl-lit",

+      "if", "&&", "||", "equals", "equiv", "bool",

+    };

+

+    static Dictionary<string, bool> reservedSmtWords;

+    static bool[] validIdChar;

+    static bool symbolListsInitilized;

+

+    static void InitSymbolLists()

+    {

+      if (symbolListsInitilized)

+        return;

+

+      lock (reservedSmtWordsList) {

+        if (symbolListsInitilized)

+          return;

+        reservedSmtWords = new Dictionary<string, bool>();

+        foreach (var w in reservedSmtWordsList)

+          reservedSmtWords.Add(w, true);

+        validIdChar = new bool[255];

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

+          validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0;

+        System.Threading.Thread.MemoryBarrier(); // c.f. http://en.wikipedia.org/wiki/Double-checked_locking

+        symbolListsInitilized = true;

+      }

+    }

+

+    static string AddQuotes(string s)

+    {

+      InitSymbolLists();

+

+      var allGood = true;

+

+      foreach (char ch in s) {

+        var c = (int)ch;

+        if (c >= validIdChar.Length || !validIdChar[c]) {

+          allGood = false;

+          break;

+        }

+      }

+

+      if (allGood)

+        return s;

+

+      return "|" + s + "|";

+    }

+

+    static string NonKeyword(string s)

+    {

+      InitSymbolLists();

+

+      if (reservedSmtWords.ContainsKey(s) || char.IsDigit(s[0]))

+        s = "q@" + s;

+

+      // | and \ are illegal even in quoted identifiers

+      if (s.IndexOf('|') >= 0)

+        s = s.Replace("|", "");

+

+      if (s.IndexOf('\\') >= 0)

+        s = s.Replace("\\", "");

+

+      return s;

+    }

+

+    public static string QuoteId(string s)

+    {

+      return AddQuotes(NonKeyword(s));

+    }

+

+    public override string GetQuotedLocalName(object thingie, string inherentName)

+    {

+      return AddQuotes(base.GetLocalName(thingie, NonKeyword(inherentName)));

+    }

+

+    public override string GetQuotedName(object thingie, string inherentName)

+    {

+      return AddQuotes(base.GetName(thingie, NonKeyword(inherentName)));

+    }

+

+    public SMTLibNamer()

+    {

+      this.Spacer = "@@";

+    }

+  }

+}

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index f617e899..b4728ff7 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -103,7 +103,7 @@ void ObjectInvariant()
         if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

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

+          string printedName = Namer.GetQuotedName(f, f.Name);

           Contract.Assert(printedName != null);

 

           bool isPred = Options.UsePredicates && f.OutParams[0].TypedIdent.Type.IsBool;

@@ -137,7 +137,7 @@ void ObjectInvariant()
     public override bool Visit(VCExprVar node, bool arg) {

       Contract.Requires(node != null);

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

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

+        string printedName = Namer.GetQuotedName(node, node.Name);

         Contract.Assert(printedName!=null);

         RegisterType(node.Type);

         string decl =

@@ -211,7 +211,7 @@ void ObjectInvariant()
     {

       RegisterType(node[0].Type);

       string name = SimplifyLikeExprLineariser.SelectOpName(node);

-      name = Namer.GetName(name, SMTLibExprLineariser.MakeIdPrintable(name));

+      name = Namer.GetQuotedName(name, name);

 

       if (!KnownSelectFunctions.ContainsKey(name)) {

         string decl = ":extrafuns (( " + name;

@@ -231,7 +231,7 @@ void ObjectInvariant()
     {

       RegisterType(node.Type);        // this is the map type, registering it should register also the index and value types

       string name = SimplifyLikeExprLineariser.StoreOpName(node);

-      name = Namer.GetName(name, SMTLibExprLineariser.MakeIdPrintable(name));

+      name = Namer.GetQuotedName(name, name);

 

       if (!KnownStoreFunctions.ContainsKey(name)) {

         string decl = ":extrafuns (( " + name;

@@ -246,7 +246,7 @@ void ObjectInvariant()
 

         if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {

           var sel = SimplifyLikeExprLineariser.SelectOpName(node);

-          sel = Namer.GetName(sel, SMTLibExprLineariser.MakeIdPrintable(sel));

+          sel = Namer.GetQuotedName(sel, sel);

           

           if (!KnownSelectFunctions.ContainsKey(sel)) {

             // need to declare it before reference

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index bfccdb3a..4c6fcbb5 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -168,6 +168,16 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

+    public virtual string GetQuotedName(Object thingie, string inherentName)

+    {

+      return GetName(thingie, inherentName);

+    }

+

+    public virtual string GetQuotedLocalName(Object thingie, string inherentName)

+    {

+      return GetLocalName(thingie, inherentName);

+    }

+

     public string Lookup(Object thingie) {

       Contract.Requires(thingie != null);

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