Make the SMTLIB backend work again, particularly with /typeEncoding:m

4 files changed, 241 insertions, 46 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 926624b4..a0686adc 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -54,15 +54,21 @@ void ObjectInvariant()
       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 ();

       Namer = namer;

+      Namer.Spacer = "__";

       this.DeclCollector = new TypeDeclCollector (namer);

       

     }

@@ -176,12 +182,14 @@ void ObjectInvariant()
         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);

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 281d36f9..677ff296 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -9,6 +9,7 @@ using System.IO;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

+using System.Linq;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

 

@@ -124,7 +125,7 @@ void ObjectInvariant()
         using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

           t.Emit(stream);

         }

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

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

       }

     }

 

@@ -656,17 +657,27 @@ void ObjectInvariant()
         //Contract.Requires(options != null);

        

         ExprLineariser.AssertAsFormula(distinctName, options);

-        

+

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

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

-          foreach (VCExpr e in node) {

-            Contract.Assert(e!=null);

-            wr.Write(" ");

-            ExprLineariser.LineariseAsTerm(e, options);

+          var groupings = node.GroupBy(e => e.Type).Where(g => g.Count() > 1).ToArray();

+

+          if (groupings.Length > 1)

+            wr.Write("(and ");

+

+          foreach (var g in groupings) {

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

+            foreach (VCExpr e in g) {

+              Contract.Assert(e != null);

+              wr.Write(" ");

+              ExprLineariser.LineariseAsTerm(e, options);

+            }

+            wr.Write(")");

           }

-          wr.Write(")");

+

+          if (groupings.Length > 1)

+            wr.Write(")");

         }

 

         return true;

@@ -684,18 +695,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 = SimplifyLikeExprLineariser.SelectOpName(node);

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

+

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

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

+          Contract.Assert(e != null);

+          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 = SimplifyLikeExprLineariser.StoreOpName(node);

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

+

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

+        foreach (VCExpr e in node) {

+          Contract.Assert(e != null);

+          wr.Write(" ");

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

+        }

+        wr.Write(")");

+        return true;

       }

 

       public bool VisitBvOp       (VCExprNAry node, LineariserOptions options) {

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 2211701c..a60b01ee 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -48,6 +48,12 @@ void ObjectInvariant()
     private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

       new Dictionary<VCExprVar/*!*/, bool> ();

 

+

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

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

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

+

+

     public List<string/*!>!*/> AllDeclarations { get {

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));

 

@@ -86,31 +92,35 @@ void ObjectInvariant()
 

     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, SMTLibExprLineariser.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);

-        }

+      if (node.Op is VCExprStoreOp) RegisterStore(node);

+      else if (node.Op is VCExprSelectOp) RegisterSelect(node);

+      else {

+        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, SMTLibExprLineariser.MakeIdPrintable(f.Name));

+          Contract.Assert(printedName != null);

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

 

-        decl += "))";

-        

-        AddDeclaration(decl);

-        KnownFunctions.Add(f, true);

+          foreach (Variable v in f.InParams) {

+            Contract.Assert(v != null);

+            RegisterType(v.TypedIdent.Type);

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

+          }

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

+          foreach (Variable v in f.OutParams) {

+            Contract.Assert(v != null);

+            RegisterType(v.TypedIdent.Type);

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

+          }

+

+          decl += "))";

+

+          AddDeclaration(decl);

+          KnownFunctions.Add(f, true);

+        }

       }

 

       return base.Visit(node, arg);

@@ -121,6 +131,7 @@ void ObjectInvariant()
       if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

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

         Contract.Assert(printedName!=null);

+        RegisterType(node.Type);

         string decl =

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

         AddDeclaration(decl);

@@ -129,6 +140,154 @@ void ObjectInvariant()
 

       return base.Visit(node, arg);

     }

+

+

+

+    public override bool Visit(VCExprQuantifier node, bool arg)

+    {

+      Contract.Requires(node != null);

+      foreach (VCExprVar v in node.BoundVars) {

+        Contract.Assert(v != null);

+        RegisterType(v.Type);

+      }

+

+      return base.Visit(node, arg);

+    } 

+

+    private void RegisterType(Type type)

+    {

+      Contract.Requires(type != null);

+      if (KnownTypes.ContainsKey(type)) return;

+

+      if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {

+        KnownTypes.Add(type, true);

+        string declString = "";

+        MapType mapType = type.AsMap;

+        Contract.Assert(mapType != null);

+

+        foreach (Type t in mapType.Arguments) {

+          Contract.Assert(t != null);

+          RegisterType(t);

+        }

+        RegisterType(mapType.Result);

+

+        declString += ":extrasorts ( " + TypeToString(type);

+

+        /*

+        if (CommandLineOptions.Clo.UseArrayTheory) {

+          declString += " :BUILTIN Array ";

+          foreach (Type t in mapType.Arguments) {

+            declString += TypeToString(t);

+            declString += " ";

+          }

+          declString += TypeToString(mapType.Result);

+        }

+         */

+

+        declString += ")";

+        AddDeclaration(declString);

+        return;

+      }

+

+      if (type.IsBool || type.IsInt)

+        return;

+

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

+        AddDeclaration(":extrasorts ( " + TypeToString(type) + " )");

+        KnownTypes.Add(type, true);

+        return;

+      }

+    }

+

+    private void RegisterSelect(VCExprNAry node)

+    {

+      RegisterType(node[0].Type);

+      string name = SimplifyLikeExprLineariser.SelectOpName(node);

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

+

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

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

+

+        foreach (VCExpr ch in node) {

+          decl += " " + TypeToString(ch.Type);

+        }

+        decl += " " + TypeToString(node.Type);

+

+        decl += " ))";

+        AddDeclaration(decl);

+        KnownSelectFunctions.Add(name, true);

+      }

+    }

+

+    private void RegisterStore(VCExprNAry node)

+    {

+      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));

+

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

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

+

+        foreach (VCExpr ch in node) {

+          decl += " " + TypeToString(ch.Type);

+        }

+        decl += " " + TypeToString(node.Type);

+

+        decl += "))";

+        AddDeclaration(decl);

+

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

+          var sel = SimplifyLikeExprLineariser.SelectOpName(node);

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

+          

+          if (!KnownSelectFunctions.ContainsKey(sel)) {

+            // need to declare it before reference

+            string seldecl = ":extrafuns (( " + sel;

+            foreach (VCExpr ch in node) {

+              seldecl += " " + TypeToString(ch.Type);

+            }

+            AddDeclaration(seldecl + "))");

+            KnownSelectFunctions.Add(sel, true);

+          }

+

+          var eq = "=";

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

+            eq = "iff";

+

+          string ax1 = ":assumption (forall ";

+          string ax2 = ":assumption (forall ";

+

+          string argX = "", argY = "";

+          string dist = "";

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

+            var t = " " + TypeToString(node[i].Type);

+            var x = " ?x" + i;

+            var y = " ?y" + i;

+            ax1 += " (" + x + t + ")";

+            ax2 += " (" + x + t + ")";

+            if (i != 0 && i != node.Arity - 1) {

+              argX += x;

+              argY += y;

+              ax2 += " (" + y + t + ")";

+              dist += " (not (=" + x + y + "))";

+            }

+          }

+          string v = " ?x" + (node.Arity - 1);

+          ax1 += "(" + eq + " (" + sel + " (" + name + " ?x0" + argX + v + ")" + argX + ") " + v + ")";

+          ax1 += ")";

+

+          ax2 += "(implies (or " + dist + ") (" + eq + " (" + sel + " (" + name + " ?x0" + argX + v + ")" + argY + ") (" + sel + " ?x0" + argY + ")))";

+          ax2 += ")";

+

+          AddDeclaration(ax1);

+          AddDeclaration(ax2);

+        }

+

+        KnownStoreFunctions.Add(name, true);

+      }

+      //

+    }

+

   }

 

 }
\ No newline at end of file
diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs
index cc4f8060..78b87590 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -118,7 +118,6 @@ void ObjectInvariant()
       case impliesName:

       case iffName:

       case eqName:

-      case distinctName:

       case TRUEName:

       case FALSEName:

       case "Array":

@@ -163,8 +162,6 @@ void ObjectInvariant()
     internal const string subtypeName = "UOrdering2";

     internal const string subtypeArgsName = "UOrdering3";

 

-    internal const string distinctName = "distinct";

-

     internal const string boolTrueName = "boolTrue";

     internal const string boolFalseName = "boolFalse";

     internal const string boolIteName = "ite";

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

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

        

-        ExprLineariser.AssertAsFormula(distinctName, options);

+        ExprLineariser.AssertAsFormula("distinct", options);

         

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);