Fixes for duality under corral

9 files changed, 205 insertions, 84 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d91ca010..82b550b7 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -423,6 +423,12 @@ namespace Microsoft.Boogie.SMTLib
             var labs = line[4];

             var refs = line[5];

             var predName = conseq.Name;

+            {

+                string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!

+                int pos = predName.LastIndexOf(spacer);

+                if (pos >= 0)

+                    predName = predName.Substring(0, pos);

+            }

             RPFP.Node node = null;

             if (!pmap.TryGetValue(predName, out node))

             {

@@ -461,7 +467,7 @@ namespace Microsoft.Boogie.SMTLib
                 return null;

             }

             int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;

-            if(ruleNum < 0 || ruleNum > rpfp.edges.Count)

+            if (ruleNum < 0 || ruleNum > rpfp.edges.Count)

             {

                 HandleProverError("bad rule name from prover: " + refs.ToString());

                 return null;

@@ -489,7 +495,7 @@ namespace Microsoft.Boogie.SMTLib
             varSubst[e.number] = dict;

             foreach (var s in subst.Arguments)

             {

-                if(s.Name != "=" || s.Arguments.Length != 2)

+                if (s.Name != "=" || s.Arguments.Length != 2)

                 {

                     HandleProverError("bad equation from prover: " + s.ToString());

                     return null;

@@ -573,6 +579,7 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

         {

@@ -588,7 +595,15 @@ namespace Microsoft.Boogie.SMTLib
             string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";

             ruleStrings.Add(ruleString);

         }

-        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n)";

+        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n";

+       

+#if true

+        if (CommandLineOptions.Clo.StratifiedInlining != 0)

+            queryString += "    :stratified-inlining true\n";

+        if (CommandLineOptions.Clo.RecursionBound > 0)

+            queryString += "    :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";

+#endif

+        queryString += ")";

         LineariserOptions.Default.LabelsBelowQuantifiers = false;

         FlushAxioms();

 

@@ -672,6 +687,8 @@ namespace Microsoft.Boogie.SMTLib
 #endif

         }

         SendThisVC("(fixedpoint-pop)");

+        Pop();

+        AxiomsAreSetup = false;

         return result;

     }

 

@@ -799,7 +816,11 @@ namespace Microsoft.Boogie.SMTLib
             if (!options.MultiTraces)

               posLabels = Enumerable.Empty<string>();

             var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

-            var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

+            string expr;

+            if (conjuncts.Length == 0)

+                expr = "false";

+            else 

+              expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

             SendThisVC("(assert " + expr + ")");

             SendThisVC("(check-sat)");

           }

@@ -956,7 +977,7 @@ namespace Microsoft.Boogie.SMTLib
                 result = Outcome.OutOfMemory;

                 Process.NeedsRestart = true;

                 break;

-              case "timeout":

+                case "timeout": case "canceled":

                 currentErrorHandler.OnResourceExceeded("timeout");

                 result = Outcome.TimeOut;

                 break;

@@ -1151,7 +1172,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void SetTimeOut(int ms)

     {

-        SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n");

+        SendThisVC("(set-option " + Z3.SetTimeoutOption() + "  " + ms.ToString() + ")\n");

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 81d5d5d1..bc9e6992 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -187,6 +187,16 @@ namespace Microsoft.Boogie.SMTLib
             minor = Z3MinorVersion;

         }

 

+        public static string SetTimeoutOption()

+        {

+            int major, minor;

+            GetVersion(out major, out minor);

+            if (major > 4 || major == 4 && minor >= 3)

+                return "TIMEOUT";

+            else

+                return "SOFT_TIMEOUT";

+        }

+

         // options that work only on the command line

         static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };

 

@@ -251,7 +261,7 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (options.TimeLimit > 0)

                 {

-                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+                    options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());

                     // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

                     // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

                 }

@@ -261,9 +271,8 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (CommandLineOptions.Clo.WeakArrayTheory)

                 {

-                    // TODO: these options don't seem to exist in recent Z3

-                    // options.AddWeakSmtOption("ARRAY_WEAK", "true");

-                    // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

+                    options.AddWeakSmtOption("smt.array.weak", "true");

+                    options.AddWeakSmtOption("smt.array.extensional", "false");

                 } 

             }

             else

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index d08a4d4b..2ff93c54 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -272,7 +272,10 @@ namespace Microsoft.Boogie.VCExprAST {
       // global variables, local variables, incarnations, etc. are

       // bound the first time they occur

       if (!UnboundVariables.TryGetValue(boogieVar, out res)) {

-        res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);

+        if (boogieVar is Constant)

+          res = new VCExprConstant(boogieVar.Name, boogieVar.TypedIdent.Type);

+        else 

+          res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);

         UnboundVariables.Bind(boogieVar, res);

       }

       return cce.NonNull(res);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 82bdebbe..f56b6978 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -1868,6 +1868,14 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprConstant : VCExprVar

+  {

+      internal VCExprConstant(string name, Type type) : base(name,type) {

+      Contract.Requires(type != null);

+      Contract.Requires(name != null);

+    }

+  }

+

   public abstract class VCExprBinder : VCExpr {

     public readonly VCExpr/*!*/ Body;

     public readonly List<TypeVariable/*!*/>/*!*/ TypeParameters;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e88c000e..6897a982 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -137,40 +137,7 @@ namespace Microsoft.Boogie {
       } else {

         if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

-        // set up the context

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          TypeCtorDecl t = decl as TypeCtorDecl;

-          if (t != null) {

-            ctx.DeclareType(t, null);

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          Constant c = decl as Constant;

-          if (c != null) {

-            ctx.DeclareConstant(c, c.Unique, null);

-          } else {

-            Function f = decl as Function;

-            if (f != null) {

-              ctx.DeclareFunction(f, null);

-            }

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          Axiom ax = decl as Axiom;

-          if (ax != null) {

-            ctx.AddAxiom(ax, null);

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          GlobalVariable v = decl as GlobalVariable;

-          if (v != null) {

-            ctx.DeclareGlobalVariable(v, null);

-          }

-        }

+        Setup(prog, ctx);

 

         // we first generate the prover and then store a clone of the

         // context in the cache, so that the prover can setup stuff in

@@ -184,6 +151,61 @@ namespace Microsoft.Boogie {
       this.gen = prover.VCExprGen;

     }

 

+    public void Retarget(Program prog, ProverContext ctx)

+    {

+        ctx.Clear();

+        Setup(prog, ctx);

+    }

+

+    private static void Setup(Program prog, ProverContext ctx)

+    {

+        // set up the context

+        foreach (Declaration decl in prog.TopLevelDeclarations)

+        {

+            Contract.Assert(decl != null);

+            TypeCtorDecl t = decl as TypeCtorDecl;

+            if (t != null)

+            {

+                ctx.DeclareType(t, null);

+            }

+        }

+        foreach (Declaration decl in prog.TopLevelDeclarations)

+        {

+            Contract.Assert(decl != null);

+            Constant c = decl as Constant;

+            if (c != null)

+            {

+                ctx.DeclareConstant(c, c.Unique, null);

+            }

+            else

+            {

+                Function f = decl as Function;

+                if (f != null)

+                {

+                    ctx.DeclareFunction(f, null);

+                }

+            }

+        }

+        foreach (Declaration decl in prog.TopLevelDeclarations)

+        {

+            Contract.Assert(decl != null);

+            Axiom ax = decl as Axiom;

+            if (ax != null)

+            {

+                ctx.AddAxiom(ax, null);

+            }

+        }

+        foreach (Declaration decl in prog.TopLevelDeclarations)

+        {

+            Contract.Assert(decl != null);

+            GlobalVariable v = decl as GlobalVariable;

+            if (v != null)

+            {

+                ctx.DeclareGlobalVariable(v, null);

+            }

+        }

+    }

+

 

     /// <summary>

     /// Clean-up.

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index bf27144b..484ce226 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Boogie
     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

     public abstract object Clone();

+    public abstract void Clear();

   }

   

 [ContractClassFor(typeof(ProverContext))]

@@ -114,6 +115,12 @@ public abstract class ProverContextContracts:ProverContext{
       exprTranslator = null;

     }

 

+    public override void Clear()

+    {

+        distincts = new List<Variable>();

+        axiomConjuncts = new List<VCExpr>();

+    }

+

     protected DeclFreeProverContext(DeclFreeProverContext ctxt) {

       Contract.Requires(ctxt != null);

       this.gen = ctxt.gen;

diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index d63f4fc2..7ebba061 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -21,6 +21,35 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie.ExprExtensions

 {

+    class ReferenceComparer<T> : IEqualityComparer<T> where T : class

+    {

+        private static ReferenceComparer<T> m_instance;

+

+        public static ReferenceComparer<T> Instance

+        {

+            get

+            {

+                return m_instance ?? (m_instance = new ReferenceComparer<T>());

+            }

+        }

+

+        public bool Equals(T x, T y)

+        {

+            return ReferenceEquals(x, y);

+        }

+

+        public int GetHashCode(T obj)

+        {

+            return System.Runtime.CompilerServices.RuntimeHelpers.GetHashCode(obj);

+        }

+    }

+

+    public class TermDict<T> : Dictionary<Term, T> 

+    {

+        public TermDict() : base(ReferenceComparer<Term>.Instance) { }

+    }

+

+        

 

     public enum TermKind { App, Other };

 

@@ -229,9 +258,9 @@ namespace Microsoft.Boogie.ExprExtensions
             {

                 public int cnt = 0;

             }

-            Dictionary<Term, counter> refcnt = new Dictionary<Term, counter>();

+            TermDict<counter> refcnt = new TermDict<counter>();

             List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-            Dictionary<Term, VCExprVar> bindingMap = new Dictionary<Term, VCExprVar>();

+            TermDict< VCExprVar> bindingMap = new TermDict< VCExprVar>();

             int letcnt = 0;

             Context ctx;

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index e96499fe..19feabe9 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -76,6 +76,8 @@ namespace Microsoft.Boogie
         Mode mode;

         AnnotationStyle style;

 

+        private static Checker old_checker = null;

+

         public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)

             : base(_program, logFilePath, appendLogFile) 

         {

@@ -106,7 +108,13 @@ namespace Microsoft.Boogie
             rpfp = new RPFP(RPFP.CreateLogicSolver(ctx));

             program = _program;

             gen = ctx;

-            checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);

+            if(old_checker == null)

+              checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);

+            else {

+                checker = old_checker;

+                checker.Retarget(program,checker.TheoremProver.Context);

+            }

+            old_checker = checker;

             boogieContext = checker.TheoremProver.Context;

             linOptions = null; //  new Microsoft.Boogie.Z3.Z3LineariserOptions(false, options, new List<VCExprVar>());

         }

@@ -660,7 +668,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small, Term lbl = null)

+        private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List<Term> small, Term lbl = null)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -733,7 +741,7 @@ namespace Microsoft.Boogie
         }

 

         private void ExtractSmallerVCs(Term t, List<Term> small){

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             Term top = ExtractSmallerVCsRec(memo, t, small);

             small.Add(top);

         }

@@ -763,7 +771,7 @@ namespace Microsoft.Boogie
             return ctx.MkImplies(ctx.MkAnd(eqns), ctx.MkApp(label, ctx.MkApp(f, tvars)));

         }

 

-        private Term MergeGoalsRec(Dictionary<Term, Term> memo, Term t)

+        private Term MergeGoalsRec(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -803,11 +811,11 @@ namespace Microsoft.Boogie
 

         private Term MergeGoals(Term t)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             return MergeGoalsRec(memo, t);

         }

 

-        private Term CollectGoalsRec(Dictionary<Term, Term> memo, Term t, List<Term> goals, List<Term> cruft)

+        private Term CollectGoalsRec(TermDict< Term> memo, Term t, List<Term> goals, List<Term> cruft)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -869,11 +877,11 @@ namespace Microsoft.Boogie
 

         private void CollectGoals(Term t, List<Term> goals, List<Term> cruft)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             CollectGoalsRec(memo, t.GetAppArgs()[1], goals, cruft);

         }

 

-        private Term SubstRec(Dictionary<Term, Term> memo, Term t)

+        private Term SubstRec(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -890,7 +898,7 @@ namespace Microsoft.Boogie
             return res;

         }

 

-        private Term SubstRecGoals(Dictionary<Term, Term> memo, Term t)

+        private Term SubstRecGoals(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -957,7 +965,7 @@ namespace Microsoft.Boogie
                 CollectGoals(sm, goals,cruft);

                 foreach (var goal in goals)

                 {

-                    Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+                    TermDict< Term> memo = new TermDict< Term>();

                     foreach (var othergoal in goals)

                         memo.Add(othergoal, othergoal.Equals(goal) ? ctx.MkFalse() : ctx.MkTrue());

                     foreach (var thing in cruft)

@@ -967,7 +975,7 @@ namespace Microsoft.Boogie
                     vcs.Add(vc);

                 }

                 {

-                    Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+                    TermDict< Term> memo = new TermDict< Term>();

                     foreach (var othergoal in goals)

                         memo.Add(othergoal, ctx.MkTrue());

                     var vc = SubstRecGoals(memo, sm);

@@ -1078,7 +1086,7 @@ namespace Microsoft.Boogie
 

         // Collect the relational paremeters

 

-        private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)

+        private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term,Term> done)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -1088,14 +1096,20 @@ namespace Microsoft.Boogie
             {

                 var f = t.GetAppDecl();

                 var args = t.GetAppArgs();

-                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

+                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();

                 StratifiedInliningInfo info;

                 if (relationToProc.TryGetValue(f, out info))

                 {

-                    f = SuffixFuncDecl(t, parms.Count);

-                    parms.Add(f);

-                    nodes.Add(info.node);

-                    res = ctx.MkApp(f, args);

+                    if (done.ContainsKey(t))

+                        res = done[t];

+                    else

+                    {

+                        f = SuffixFuncDecl(t, parms.Count);

+                        parms.Add(f);

+                        nodes.Add(info.node);

+                        res = ctx.MkApp(f, args);

+                        done.Add(t,res); // don't count same expression twice!

+                    }

                 }

                 else

                     res = ctx.CloneApp(t, args);

@@ -1111,8 +1125,9 @@ namespace Microsoft.Boogie
             Term[] paramTerms = info.interfaceExprVars.Select(x => boogieContext.VCExprToTerm(x, linOptions)).ToArray();

             var relParams = new List<FuncDecl>();

             var nodeParams = new List<RPFP.Node>();

-            var memo = new Dictionary<Term, Term>();

-            vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams);

+            var memo = new TermDict< Term>();

+            var done = new Dictionary<Term,Term>(); // note this hashes on equality, not reference!

+            vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams,done);

             // var ops = new Util.ContextOps(ctx);

             // var foo = ops.simplify_lhs(vcTerm);

             // vcTerm = foo.Item1;

@@ -1430,7 +1445,7 @@ namespace Microsoft.Boogie
                         // start = DateTime.Now;

                         Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);

                         // cexroot.owner.DisposeDualModel();

-                        cex.Print(0);  // TODO: just for testing

+                        // cex.Print(0);  // just for testing

                         collector.OnCounterexample(cex, "assertion failure");

                         Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);

                         return VC.ConditionGeneration.Outcome.Errors;

@@ -1471,7 +1486,7 @@ namespace Microsoft.Boogie
             labels = new Dictionary<string, Term>();

             foreach(var e in rpfp.edges){

                 int id = e.number;

-                HashSet<Term> memo = new HashSet<Term>();

+                HashSet<Term> memo = new HashSet<Term>(ReferenceComparer<Term>.Instance);

                 FindLabelsRec(memo, e.F.Formula, labels);

             }

         }

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index f6a42a43..e7df7be6 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -159,7 +159,7 @@ namespace Microsoft.Boogie
             public Edge map;

             public HashSet<string> labels;

             internal Term dual;

-            internal Dictionary<Term,Term> valuation;

+            internal TermDict<Term> valuation;

         }

 

         

@@ -263,7 +263,7 @@ namespace Microsoft.Boogie
         public Term Eval(Edge e, Term t)

         {

             if (e.valuation == null)

-                e.valuation = new Dictionary<Term, Term>();

+                e.valuation = new TermDict< Term>();

             if (e.valuation.ContainsKey(t))

                 return e.valuation[t];

             return null; // TODO

@@ -275,7 +275,7 @@ namespace Microsoft.Boogie
         public void SetValue(Edge e, Term variable, Term value)

         {

             if (e.valuation == null)

-                e.valuation = new Dictionary<Term, Term>(); 

+                e.valuation = new TermDict< Term>(); 

             e.valuation.Add(variable, value);

         }

 

@@ -369,8 +369,8 @@ namespace Microsoft.Boogie
         // Collect the relational paremeters

 

         Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();

-        

-        private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)

+

+        private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term, Term> done)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -381,12 +381,18 @@ namespace Microsoft.Boogie
                 Node node;

                 if (relationToNode.TryGetValue(f, out node))

                 {

-                    f = SuffixFuncDecl(t, parms.Count);

-                    parms.Add(f);

-                    nodes.Add(node);

+                    if (done.ContainsKey(t))

+                        res = done[t];

+                    else

+                    {

+                        f = SuffixFuncDecl(t, parms.Count);

+                        parms.Add(f);

+                        nodes.Add(node);

+                        done.Add(t,res); // don't count same expression twice!

+                    }

                 }

                 var args = t.GetAppArgs();

-                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

+                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();

                 res = ctx.CloneApp(t, args);

             } // TODO: handle quantifiers

             else

@@ -399,7 +405,7 @@ namespace Microsoft.Boogie
         {

             // TODO: is this right?

             // return t.IsFunctionApp() && t.GetAppArgs().Length == 0;

-            return t is VCExprVar;

+            return t is VCExprVar && !(t is VCExprConstant);

         }

 

         private Edge GetEdgeFromClause(Term t, FuncDecl failName)

@@ -428,8 +434,9 @@ namespace Microsoft.Boogie
                 }

             var relParams = new List<FuncDecl>();

             var nodeParams = new List<RPFP.Node>();

-            var memo = new Dictionary<Term, Term>();

-            body = CollectParamsRec(memo, body, relParams, nodeParams);

+            var memo = new TermDict< Term>();

+            var done = new Dictionary<Term, Term>(); // note this hashes on equality, not reference!

+            body = CollectParamsRec(memo, body, relParams, nodeParams,done);

             Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);

             Node parent = relationToNode[Name];

             return CreateEdge(parent, F, nodeParams.ToArray());

@@ -504,7 +511,7 @@ namespace Microsoft.Boogie
             return query;

         }

 

-        private void CollectVariables(Dictionary<Term, bool> memo, Term t, List<Term> vars)

+        private void CollectVariables(TermDict< bool> memo, Term t, List<Term> vars)

         {

             if (memo.ContainsKey(t))

                 return;

@@ -520,13 +527,13 @@ namespace Microsoft.Boogie
 

         private Term BindVariables(Term t, bool universal = true)

         {

-            Dictionary<Term, bool> memo = new Dictionary<Term,bool>();

+            TermDict< bool> memo = new TermDict<bool>();

             List<Term> vars = new List<Term>();

             CollectVariables(memo,t,vars);

             return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);

         }

 

-        private Term SubstPredsRec(Dictionary<Term, Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)

+        private Term SubstPredsRec(TermDict< Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -554,7 +561,7 @@ namespace Microsoft.Boogie
 

         private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             return SubstPredsRec(memo, subst, t);

         }