using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
using VC;
using Outcome = VC.VCGen.Outcome;
using Bpl = Microsoft.Boogie;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie.GraphUtil;

namespace Microsoft.Boogie.Houdini {

    public class AbsHoudini
    {
        Dictionary<string, Function> existentialFunctions;
        Program program;
        Dictionary<string, Implementation> name2Impl;
        Dictionary<string, VCExpr> impl2VC;
        Dictionary<string, List<Tuple<string, Function, NAryExpr>>> impl2FuncCalls;
        // constant -> the naryexpr that it replaced
        Dictionary<string, NAryExpr> constant2FuncCall;

        // function -> its abstract value
        Dictionary<string, IAbstractDomain> function2Value;

        // impl -> functions assumed/asserted
        Dictionary<string, HashSet<string>> impl2functionsAsserted, impl2functionsAssumed;

        // funtions -> impls where assumed/asserted
        Dictionary<string, HashSet<string>> function2implAssumed, function2implAsserted;

        // impl -> handler, collector
        Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>> impl2ErrorHandler;

        // Essentials: VCGen, Prover
        VCGen vcgen;
        ProverInterface prover;

        // Stats
        TimeSpan proverTime;
        int numProverQueries;

        public AbsHoudini(Program program, IAbstractDomain defaultElem)
        {
            this.program = program;
            this.impl2VC = new Dictionary<string, VCExpr>();
            this.impl2FuncCalls = new Dictionary<string, List<Tuple<string, Function, NAryExpr>>>();
            this.existentialFunctions = new Dictionary<string, Function>();
            this.name2Impl = new Dictionary<string, Implementation>();
            this.impl2functionsAsserted = new Dictionary<string, HashSet<string>>();
            this.impl2functionsAssumed = new Dictionary<string, HashSet<string>>();
            this.function2implAsserted = new Dictionary<string, HashSet<string>>();
            this.function2implAssumed = new Dictionary<string, HashSet<string>>();
            this.impl2ErrorHandler = new Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>>();
            this.constant2FuncCall = new Dictionary<string, NAryExpr>();

            // Find the existential functions
            foreach (var func in program.TopLevelDeclarations.OfType<Function>()
                .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))
                existentialFunctions.Add(func.Name, func);

            this.function2Value = new Dictionary<string, IAbstractDomain>();
            foreach (var func in existentialFunctions.Values)
            {
                // Find if the function wishes to use a specific abstract domain
                var domain = QKeyValue.FindStringAttribute(func.Attributes, "absdomain");
                if (domain == null)
                {
                    function2Value[func.Name] = defaultElem.Bottom();
                }
                else
                {
                    function2Value[func.Name] = AbstractDomainFactory.GetInstance(domain);
                }
            }
            existentialFunctions.Keys.Iter(f => function2implAssumed.Add(f, new HashSet<string>()));
            existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet<string>()));

            // type check
            existentialFunctions.Values.Iter(func =>
                {
                    if (func.OutParams.Count != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)
                        throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name));
                    if(func.Body != null)
                        throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name));
                    var args = new List<Type>();
                    func.InParams.Iter(v => args.Add(v.TypedIdent.Type));
                    string msg = "";
                    if (!function2Value[func.Name].TypeCheck(args, out msg))
                        throw new AbsHoudiniInternalError("TypeError: " + msg);
                });

            //if (CommandLineOptions.Clo.ProverKillTime > 0)
            //    CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));

            Inline();

            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

            this.proverTime = TimeSpan.Zero;
            this.numProverQueries = 0;

            program.TopLevelDeclarations.OfType<Implementation>()
                .Where(impl => !impl.SkipVerification)
                .Iter(impl => name2Impl.Add(impl.Name, impl));

            // Let's do VC Gen (and also build dependencies)
            name2Impl.Values.Iter(GenVC);
        }

        public VCGenOutcome ComputeSummaries()
        {
            var overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Valid, new List<Counterexample>());

            // Compute SCCs and determine a priority order for impls
            var Succ = new Dictionary<string, HashSet<string>>();
            var Pred = new Dictionary<string, HashSet<string>>();
            name2Impl.Keys.Iter(s => Succ[s] = new HashSet<string>());
            name2Impl.Keys.Iter(s => Pred[s] = new HashSet<string>());

            foreach(var impl in name2Impl.Keys) {
                Succ[impl] = new HashSet<string>();
                impl2functionsAsserted[impl].Iter(f => 
                    function2implAssumed[f].Iter(succ =>
                        {
                            Succ[impl].Add(succ);
                            Pred[succ].Add(impl);
                        }));
            }

            var sccs = new StronglyConnectedComponents<string>(name2Impl.Keys,
                new Adjacency<string>(n => Pred[n]),
                new Adjacency<string>(n => Succ[n]));
            sccs.Compute();
            
            // impl -> priority
            var impl2Priority = new Dictionary<string, int>();
            int p = 0;
            foreach (var scc in sccs)
            {
                foreach (var impl in scc)
                {
                    impl2Priority.Add(impl, p);
                    p++;
                }
            }

            var worklist = new SortedSet<Tuple<int, string>>();
            name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k)));

            while (worklist.Any())
            {
                var impl = worklist.First().Item2;
                worklist.Remove(worklist.First());

                var gen = prover.VCExprGen;
                var terms = new List<Expr>();
                foreach (var tup in impl2FuncCalls[impl])
                {
                    var controlVar = tup.Item2;
                    var exprVars = tup.Item3;
                    var varList = new List<Expr>();
                    exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v));
                    
                    var args = new List<Expr>();
                    controlVar.InParams.Iter(v => args.Add(Expr.Ident(v)));
                    Expr term = Expr.Eq(new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args),
                                 function2Value[tup.Item1].Gamma(varList));

                    if (controlVar.InParams.Count != 0)
                    {
                        term = new ForallExpr(Token.NoToken, new List<Variable>(controlVar.InParams.ToArray()),
                            new Trigger(Token.NoToken, true, new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args) }),
                            term);
                    }
                    terms.Add(term);
                }
                var env = Expr.BinaryTreeAnd(terms);

                env.Typecheck(new TypecheckingContext((IErrorSink)null));
                var envVC = prover.Context.BoogieExprTranslator.Translate(env);

                var vc = gen.Implies(envVC, impl2VC[impl]);

                if (CommandLineOptions.Clo.Trace)
                {
                    Console.WriteLine("Verifying {0}: ", impl);
                    //Console.WriteLine("env: {0}", envVC);
                    var envFuncs = new HashSet<string>();
                    impl2FuncCalls[impl].Iter(tup => envFuncs.Add(tup.Item1));
                    envFuncs.Iter(f => PrintFunction(existentialFunctions[f]));
                }

                var handler = impl2ErrorHandler[impl].Item1;
                var collector = impl2ErrorHandler[impl].Item2;
                collector.Reset(impl);

                var start = DateTime.Now;

                prover.Push();
                prover.Assert(gen.Not(vc), true);
                prover.FlushAxiomsToTheoremProver();
                prover.Check();
                ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);

                //prover.BeginCheck(impl, vc, handler);
                //ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);

                var inc = (DateTime.Now - start);
                proverTime += inc;
                numProverQueries++;

                if (CommandLineOptions.Clo.Trace)
                    Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());

                if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
                {
                    // pick some function; make it true and keep going
                    bool changed = false;
                    foreach (var f in impl2functionsAsserted[impl])
                    {
                        function2Value[f] = function2Value[f].MakeTop(out changed);
                        if (changed) break;
                    }
                    if(!changed)
                        return new VCGenOutcome(proverOutcome, new List<Counterexample>());
                }

                if (CommandLineOptions.Clo.Trace)
                    Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT");

                if (collector.numErrors > 0)
                {
                    var funcsChanged = collector.funcsChanged;
                    if (funcsChanged.Count == 0)
                    {
                        overallOutcome = new VCGenOutcome(ProverInterface.Outcome.Invalid, collector.errors);
                        break;
                    }

                    // propagate dependent guys back into the worklist, including self
                    var deps = new HashSet<string>();
                    deps.Add(impl);
                    funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f]));

                    deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s)));
                }

                prover.Pop();
            }

            if (CommandLineOptions.Clo.Trace)
            {
                Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2"));
                Console.WriteLine("Number of prover queries = " + numProverQueries);
            }

            if (CommandLineOptions.Clo.PrintAssignment)
            {
                // Print the answer
                existentialFunctions.Values.Iter(PrintFunction);
            }

            return overallOutcome;
        }


        public IEnumerable<Function> GetAssignment()
        {
            var ret = new List<Function>();
            foreach (var func in existentialFunctions.Values)
            {
                var invars = new List<Expr>(func.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));
                func.Body = function2Value[func.Name].Gamma(invars);
                ret.Add(func);
            }
            return ret;
        }

        private void PrintFunction(Function function)
        {
            var tt = new TokenTextWriter(Console.Out, /*pretty=*/ false);
            var invars = new List<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));
            function.Body = function2Value[function.Name].Gamma(invars);
            function.Emit(tt, 0);
            tt.Close();
        }

        public HashSet<string> HandleCounterExample(string impl, Counterexample error)
        {
            var funcsChanged = new HashSet<string>();
            // Find the failing assert -- need to do a join there
            // return the set of functions whose definition has changed
            var cex = ExtractState(impl, error);
            foreach (var tup in cex)
            {
                function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2);
                funcsChanged.Add(tup.Item1);
            }
            return funcsChanged;
        }

        private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Counterexample error)
        {
            var lastBlock = error.Trace.Last() as Block;
            AssertCmd failingAssert = null;

            CallCounterexample callCounterexample = error as CallCounterexample;
            if (callCounterexample != null)
            {
                Procedure failingProcedure = callCounterexample.FailingCall.Proc;
                Requires failingRequires = callCounterexample.FailingRequires;
                failingAssert = lastBlock.Cmds.OfType<AssertRequiresCmd>().FirstOrDefault(ac => ac.Requires == failingRequires);
            }
            ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
            if (returnCounterexample != null)
            {
                Ensures failingEnsures = returnCounterexample.FailingEnsures;
                failingAssert = lastBlock.Cmds.OfType<AssertEnsuresCmd>().FirstOrDefault(ac => ac.Ensures == failingEnsures);
            }
            AssertCounterexample assertCounterexample = error as AssertCounterexample;
            if (assertCounterexample != null)
            {
                failingAssert = lastBlock.Cmds.OfType<AssertCmd>().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert);
            }

            Debug.Assert(failingAssert != null);
            return ExtractState(impl, failingAssert.Expr, error.Model);
        }

        private static int existentialConstCounter = 0;

        private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Expr expr, Model model)
        {
            var funcsUsed = FunctionCollector.Collect(expr);

            var ret = new List<Tuple<string, List<Model.Element>>>();

            foreach (var tup in funcsUsed.Where(t => t.Item2 == null))
            {
                var constant = tup.Item1;
                if (!constant2FuncCall.ContainsKey(constant.Name))
                    continue;

                var func = constant2FuncCall[constant.Name];
                var funcName = (func.Fun as FunctionCall).FunctionName;
                var vals = new List<Model.Element>();
                prover.Context.BoogieExprTranslator.Translate(func.Args).Iter(ve => vals.Add(getValue(ve, model)));
                ret.Add(Tuple.Create(funcName, vals));
            }

            foreach (var tup in funcsUsed.Where(t => t.Item2 != null))
            {
                var constant = tup.Item1;
                var boundExpr = tup.Item2;

                if (!constant2FuncCall.ContainsKey(constant.Name))
                    continue;

                // There are some bound variables (because the existential function was inside an \exists).
                // We must find an assignment for bound varibles 

                // First, peice apart the existential functions
                var cd = new Duplicator();
                var tup2 = ExistentialExprModelMassage.Massage(cd.VisitExpr(boundExpr.Body));
                var be = tup2.Item1;
                Expr env = Expr.True;
                foreach (var ahFunc in tup2.Item2)
                {
                    var tup3 = impl2FuncCalls[impl].First(t => t.Item2.Name == ahFunc.Name);
                    var varList = new List<Expr>();
                    tup3.Item3.Args.OfType<Expr>().Iter(v => varList.Add(v));

                    env = Expr.And(env, function2Value[tup3.Item1].Gamma(varList));
                }
                be = Expr.And(be, Expr.Not(env));

                // map formals to constants
                var formalToConstant = new Dictionary<string, Constant>();
                foreach (var f in boundExpr.Dummies.OfType<Variable>())
                    formalToConstant.Add(f.Name, new Constant(Token.NoToken, new TypedIdent(Token.NoToken, f.Name + "@subst@" + (existentialConstCounter++), f.TypedIdent.Type), false));
                be = Substituter.Apply(new Substitution(v => formalToConstant.ContainsKey(v.Name) ? Expr.Ident(formalToConstant[v.Name]) : Expr.Ident(v)), be);
                formalToConstant.Values.Iter(v => prover.Context.DeclareConstant(v, false, null));

                var reporter = new AbstractHoudiniErrorReporter();
                var ve = prover.Context.BoogieExprTranslator.Translate(be);
                prover.Assert(ve, true);
                prover.Check();
                var proverOutcome = prover.CheckOutcomeCore(reporter);
                if (proverOutcome != ProverInterface.Outcome.Invalid)
                    continue;
                model = reporter.model;

                var func = constant2FuncCall[constant.Name];
                var funcName = (func.Fun as FunctionCall).FunctionName;
                var vals = new List<Model.Element>();
                foreach (var funcArg in func.Args.OfType<Expr>())
                {
                    var arg = Substituter.Apply(new Substitution(v => formalToConstant.ContainsKey(v.Name) ? Expr.Ident(formalToConstant[v.Name]) : Expr.Ident(v)), funcArg);
                    vals.Add(getValue(prover.Context.BoogieExprTranslator.Translate(arg), model));
                }
                ret.Add(Tuple.Create(funcName, vals));

            }

            return ret;
        }

        private Model.Element getValue(VCExpr arg, Model model)
        {


            if (arg is VCExprLiteral)
            {
                //return model.GetElement(arg.ToString());
                return model.MkElement(arg.ToString());
            }

            else if (arg is VCExprVar)
            {
                var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
                if (el != null)
                {
                    Debug.Assert(el.Arity == 0 && el.AppCount == 1);
                    return el.Apps.First().Result;
                }
                else
                {
                    // Variable not defined; assign arbitrary value
                    if (arg.Type.IsBool)
                        return model.MkElement("false");
                    else if (arg.Type.IsInt)
                        return model.MkIntElement(0);
                    else
                        return null;
                }
            }
            else if (arg is VCExprNAry && (arg as VCExprNAry).Op is VCExprBvOp)
            {
                // support for BV constants
                var bvc = (arg as VCExprNAry)[0] as VCExprLiteral;
                if (bvc != null)
                {
                    var ret = model.TryMkElement(bvc.ToString() + arg.Type.ToString());
                    if (ret != null && (ret is Model.BitVector)) return ret;
                }
            }

            var val = prover.Evaluate(arg);
            if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
            {
                return model.MkElement(val.ToString());
            }
            else
            {
                Debug.Assert(false);
            }
            return null;
        }

        // Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"
        class ExistentialExprModelMassage : StandardVisitor
        {
            List<Function> ahFuncs;

            public ExistentialExprModelMassage()
            {
                ahFuncs = new List<Function>();
            }

            public static Tuple<Expr, List<Function>> Massage(Expr expr)
            {
                var ee = new ExistentialExprModelMassage();
                expr = ee.VisitExpr(expr);
                return Tuple.Create(expr, ee.ahFuncs);
            }

            public override Expr VisitNAryExpr(NAryExpr node)
            {
                if (node.Fun is FunctionCall && (node.Fun as FunctionCall).FunctionName.StartsWith("AbsHoudiniConstant"))
                {
                    ahFuncs.Add((node.Fun as FunctionCall).Func);
                    return Expr.True;
                }

                return base.VisitNAryExpr(node);
            }
        }

        class FunctionCollector : ReadOnlyVisitor
        {
            public List<Tuple<Function, ExistsExpr>> functionsUsed;
            ExistsExpr existentialExpr;

            public FunctionCollector()
            {
                functionsUsed = new List<Tuple<Function, ExistsExpr>>();
                existentialExpr = null;
            }

            public static List<Tuple<Function, ExistsExpr>> Collect(Expr expr)
            {
                var fv = new FunctionCollector();
                fv.VisitExpr(expr);
                return fv.functionsUsed;
            }

            public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
            {
                var oldE = existentialExpr;

                if (node is ExistsExpr)
                    existentialExpr = (node as ExistsExpr);

                node = base.VisitQuantifierExpr(node);

                existentialExpr = oldE;
                return node;
            }

            public override Expr VisitNAryExpr(NAryExpr node)
            {
                if (node.Fun is FunctionCall)
                {
                    var collector = new VariableCollector();
                    collector.Visit(node);

                    if(existentialExpr != null && existentialExpr.Dummies.Intersect(collector.usedVars).Any())
                        functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).Func, existentialExpr));
                    else
                        functionsUsed.Add(Tuple.Create<Function, ExistsExpr>((node.Fun as FunctionCall).Func, null));
                }

                return base.VisitNAryExpr(node);
            }
        }

        class AbsHoudiniCounterexampleCollector : VerifierCallback
        {
            public HashSet<string> funcsChanged;
            public string currImpl;
            public int numErrors;
            public List<Counterexample> errors;

            AbsHoudini container;

            public AbsHoudiniCounterexampleCollector(AbsHoudini container)
            {
                this.container = container;
                Reset(null);
            }

            public void Reset(string impl)
            {
                funcsChanged = new HashSet<string>();
                currImpl = impl;
                numErrors = 0;
                errors = new List<Counterexample>();
            }

            public override void OnCounterexample(Counterexample ce, string reason)
            {
                numErrors++;
                errors.Add(ce);

                funcsChanged.UnionWith(
                    container.HandleCounterExample(currImpl, ce));
            }
        }

        private void GenVC(Implementation impl)
        {
            ModelViewInfo mvInfo;
            Dictionary<int, Absy> label2absy;
            var collector = new AbsHoudiniCounterexampleCollector(this);
            collector.OnProgress("HdnVCGen", 0, 0, 0.0);

            if (CommandLineOptions.Clo.Trace)
            {
                Console.WriteLine("Generating VC of {0}", impl.Name);
            }

            vcgen.ConvertCFG2DAG(impl);
            var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

            // Inline functions
            (new InlineFunctionCalls()).VisitBlockList(impl.Blocks);

            ExtractQuantifiedExprs(impl);
            StripOutermostForall(impl);

            //CommandLineOptions.Clo.PrintInstrumented = true;
            //var tt = new TokenTextWriter(Console.Out);
            //impl.Emit(tt, 0);
            //tt.Close();

            // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants
            var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);
            var fv = new ReplaceFunctionCalls(existentialFunctionNames);
            fv.VisitBlockList(impl.Blocks);

            impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);
            impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);

            fv.functionsAssumed.Iter(f => function2implAssumed[f].Add(impl.Name));
            fv.functionsAsserted.Iter(f => function2implAsserted[f].Add(impl.Name));

            impl2FuncCalls.Add(impl.Name, fv.functionsUsed);
            fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3));

            var gen = prover.VCExprGen;
            VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO);

            var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context);
            if (!CommandLineOptions.Clo.UseLabels)
            {
                VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO));
                VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId)));
                vcexpr = gen.Implies(eqExpr, vcexpr);
            }

            ProverInterface.ErrorHandler handler = null;
            if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
                handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
            else
                handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);

            impl2ErrorHandler.Add(impl.Name, Tuple.Create(handler, collector));

            //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);

            // Create a macro so that the VC can sit with the theorem prover
            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
            prover.DefineMacro(macro, vcexpr);

            // Store VC
            impl2VC.Add(impl.Name, gen.Function(macro));

            // HACK: push the definitions of constants involved in function calls
            // It is possible that some constants only appear in function calls. Thus, when
            // they are replaced by Boolean constants, it is possible that (get-value) will 
            // fail if the expression involves such constants. All we need to do is make sure
            // these constants are declared, because otherwise, semantically we are doing
            // the right thing.
            foreach (var tup in fv.functionsUsed)
            {
                // Ignore ones with bound varibles
                if (tup.Item2.InParams.Count > 0) continue;
                var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
                tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
                prover.Assert(tt, true);
            }
        }

        // convert "foo(... forall e ...) to:
        //    (p iff forall e) ==> foo(... p ...) 
        // where p is a fresh boolean variable and foo is an existential constant
        private void ExtractQuantifiedExprs(Implementation impl)
        {
            var funcs = new HashSet<string>(existentialFunctions.Keys);
            foreach (var blk in impl.Blocks)
            {
                foreach (var acmd in blk.Cmds.OfType<AssertCmd>())
                {
                    var ret = ExtractQuantifiers.Extract(acmd.Expr, funcs);
                    acmd.Expr = ret.Item1;
                    impl.LocVars.AddRange(ret.Item2);
                }
            }
        }

        // convert "assert e1 && forall x: e2" to
        //    assert e1 && e2[x <- x@bound]
        private void StripOutermostForall(Implementation impl)
        {
            var funcs = new HashSet<string>(existentialFunctions.Keys);
            foreach (var blk in impl.Blocks)
            {
                foreach (var acmd in blk.Cmds.OfType<AssertCmd>())
                {
                    var ret = StripQuantifiers.Run(acmd.Expr, funcs);
                    acmd.Expr = ret.Item1;
                    impl.LocVars.AddRange(ret.Item2);
                }
            }
        }

        private void Inline()
        {
            if (CommandLineOptions.Clo.InlineDepth < 0)
                return;

            var callGraph = BuildCallGraph();

            foreach (Implementation impl in callGraph.Nodes)
            {
                InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
                inlineEnsuresVisitor.Visit(impl);
            }

            foreach (Implementation impl in callGraph.Nodes)
            {
                impl.OriginalBlocks = impl.Blocks;
                impl.OriginalLocVars = impl.LocVars;
            }
            foreach (Implementation impl in callGraph.Nodes)
            {
                CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
                CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
                Inliner.ProcessImplementationForHoudini(program, impl);
                CommandLineOptions.Clo.ProcedureInlining = savedOption;
            }
            foreach (Implementation impl in callGraph.Nodes)
            {
                impl.OriginalBlocks = null;
                impl.OriginalLocVars = null;
            }

            Graph<Implementation> oldCallGraph = callGraph;
            callGraph = new Graph<Implementation>();
            foreach (Implementation impl in oldCallGraph.Nodes)
            {
                callGraph.AddSource(impl);
            }
            foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
            {
                callGraph.AddEdge(edge.Item1, edge.Item2);
            }
            int count = CommandLineOptions.Clo.InlineDepth;
            while (count > 0)
            {
                foreach (Implementation impl in oldCallGraph.Nodes)
                {
                    List<Implementation> newNodes = new List<Implementation>();
                    foreach (Implementation succ in callGraph.Successors(impl))
                    {
                        newNodes.AddRange(oldCallGraph.Successors(succ));
                    }
                    foreach (Implementation newNode in newNodes)
                    {
                        callGraph.AddEdge(impl, newNode);
                    }
                }
                count--;
            }
        }

        private Graph<Implementation> BuildCallGraph()
        {
            Graph<Implementation> callGraph = new Graph<Implementation>();
            Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Procedure proc = decl as Procedure;
                if (proc == null) continue;
                procToImpls[proc] = new HashSet<Implementation>();
            }
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Implementation impl = decl as Implementation;
                if (impl == null || impl.SkipVerification) continue;
                callGraph.AddSource(impl);
                procToImpls[impl.Proc].Add(impl);
            }
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Implementation impl = decl as Implementation;
                if (impl == null || impl.SkipVerification) continue;
                foreach (Block b in impl.Blocks)
                {
                    foreach (Cmd c in b.Cmds)
                    {
                        CallCmd cc = c as CallCmd;
                        if (cc == null) continue;
                        foreach (Implementation callee in procToImpls[cc.Proc])
                        {
                            callGraph.AddEdge(impl, callee);
                        }
                    }
                }
            }
            return callGraph;
        }

    }

    class InlineFunctionCalls : StandardVisitor
    {
        public Stack<string> inlinedFunctionsStack;

        public InlineFunctionCalls()
        {
            inlinedFunctionsStack = new Stack<string>();
        }

        public override Expr VisitNAryExpr(NAryExpr node)
        {
            var fc = node.Fun as FunctionCall;
            if (fc != null && fc.Func.Body != null && QKeyValue.FindBoolAttribute(fc.Func.Attributes, "inline"))
            {
                if (inlinedFunctionsStack.Contains(fc.Func.Name))
                {
                    // recursion detected
                    throw new AbsHoudiniInternalError("Recursion detected in function declarations");
                }

                // create a substitution
                var subst = new Dictionary<Variable, Expr>();
                for (int i = 0; i < node.Args.Count; i++)
                {
                    subst.Add(fc.Func.InParams[i], node.Args[i]);
                }

                var e =
                    Substituter.Apply(new Substitution(v => subst.ContainsKey(v) ? subst[v] : Expr.Ident(v)), fc.Func.Body);

                inlinedFunctionsStack.Push(fc.Func.Name);

                e = base.VisitExpr(e);

                inlinedFunctionsStack.Pop();

                return e;
            }
            return base.VisitNAryExpr(node);
        }
    }

    class ReplaceFunctionCalls : StandardVisitor
    {
        public List<Tuple<string, Function, NAryExpr>> functionsUsed;
        public List<Function> boolConstants;

        public HashSet<string> functionsAssumed;
        public HashSet<string> functionsAsserted;
        HashSet<string> functionsToReplace;

        private bool inAssume;
        private bool inAssert;
        private bool inFunction;
        private List<Dictionary<string, Variable>> boundVars;
        private static int IdCounter = 0;

        public ReplaceFunctionCalls(HashSet<string> functionsToReplace)
        {
            this.functionsUsed = new List<Tuple<string, Function, NAryExpr>>();
            this.functionsToReplace = functionsToReplace;
            this.functionsAsserted = new HashSet<string>();
            this.functionsAssumed = new HashSet<string>();
            this.boolConstants = new List<Function>();
            this.boundVars = new List<Dictionary<string, Variable>>();

            inAssume = false;
            inAssert = false;
            inFunction = false;
        }

        public override Cmd VisitAssertCmd(AssertCmd node)
        {
            inAssert = true;
            var ret = base.VisitAssertCmd(node);
            inAssert = false;
            return ret;
        }

        public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
        {
            return this.VisitAssertCmd(node);
        }

        public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
        {
            return this.VisitAssertCmd(node);
        }

        public override Cmd VisitAssumeCmd(AssumeCmd node)
        {
            inAssume = true;
            var ret = base.VisitAssumeCmd(node);
            inAssume = false;
            return ret;
        }

        public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
        {
            // gather the quantified variables
            var dummies = new Dictionary<string, Variable>();
            node.Dummies.Iter(v => dummies.Add(v.Name, v));

            boundVars.Add(dummies);

            node = base.VisitQuantifierExpr(node);

            boundVars.RemoveAt(boundVars.Count - 1);

            return node;
        }

        public override Expr VisitNAryExpr(NAryExpr node)
        {
            var inF = inFunction;

            if (node.Fun is FunctionCall && functionsToReplace.Contains((node.Fun as FunctionCall).FunctionName))
            {                
                found((node.Fun as FunctionCall).FunctionName);
                inFunction = true;

                // collect all the variables used by this function
                var collector = new VariableCollector();
                collector.VisitExpr(node);

                // Find the outermost bound variables
                var bound = new List<Variable>();
                if(boundVars.Count > 0) 
                    bound.AddRange(collector.usedVars.Intersect(boundVars[0].Values));

                // create boolean function to replace this guy
                var constant = new Function(Token.NoToken, "AbsHoudiniConstant" + IdCounter, bound,
                    new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "r", Microsoft.Boogie.Type.Bool), false));
                IdCounter++;
                
                functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).FunctionName, constant, node));
                boolConstants.Add(constant);

                var args = new List<Expr>();
                bound.OfType<Variable>().Select(v => Expr.Ident(v)).Iter(v => args.Add(v));
                return new NAryExpr(Token.NoToken, new FunctionCall(constant), args);
            }
            var ret = base.VisitNAryExpr(node);

            inFunction = inF;

            return ret;
        }

        public override Expr VisitIdentifierExpr(IdentifierExpr node)
        {
            if (inFunction)
            {
                // Inside functions we can only refer to the outermost bound variables
                for (int i = boundVars.Count - 1; i >= 1; i--)
                {
                    if (boundVars[i].ContainsKey(node.Name))
                        throw new AbsHoudiniInternalError("Existential functions can only refer to outermost bound variables in an expression");
                }
            }

            return base.VisitIdentifierExpr(node);
        }

        private void found(string func)
        {
            if (inAssume) functionsAssumed.Add(func);
            if (inAssert) functionsAsserted.Add(func);
        }

    }

    // convert "foo(... forall e ...) to:
    //    (p iff forall e) ==> foo(... p ...) 
    // where p is a fresh boolean variable and foo is an existential constant
    class ExtractQuantifiers : StandardVisitor
    {
        static int freshConstCounter = 0;
        HashSet<string> existentialFunctions;
        bool insideExistential;
        Dictionary<Constant, Expr> newConstants;

        private ExtractQuantifiers(HashSet<string> existentialFunctions)
        {
            this.existentialFunctions = existentialFunctions;
            insideExistential = false;
            newConstants = new Dictionary<Constant, Expr>();
        }

        public static Tuple<Expr, IEnumerable<Constant>> Extract(Expr expr, HashSet<string> existentialFunctions)
        {
            var eq = new ExtractQuantifiers(existentialFunctions);
            expr = eq.VisitExpr(expr);
            Expr ret = Expr.True;
            foreach (var tup in eq.newConstants)
            {
                ret = Expr.And(ret, Expr.Eq(Expr.Ident(tup.Key), tup.Value));
            }
            ret = Expr.Imp(ret, expr);
            return Tuple.Create(ret, eq.newConstants.Keys.AsEnumerable());
        }

        public override Expr VisitNAryExpr(NAryExpr node)
        {
            var oldIE = insideExistential;

            if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName))
                insideExistential = true;

            var ret = base.VisitNAryExpr(node);

            insideExistential = oldIE;
            return ret;
        }

        public override Expr VisitExpr(Expr node)
        {
            if (node is QuantifierExpr)
            {
                return MyVisitQuantifierExpr(node as QuantifierExpr);
            }
            return base.VisitExpr(node);
        }

        public Expr MyVisitQuantifierExpr(QuantifierExpr node)
        {
            node = base.VisitQuantifierExpr(node);

            if (insideExistential)
            {
                var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken,
                    "quant@const" + freshConstCounter, Microsoft.Boogie.Type.Bool), false);
                freshConstCounter++;

                newConstants.Add(constant, node);

                return Expr.Ident(constant);                
            }

            return node;
        }
    }

    // convert "assert e1 && forall x: e2" to
    //    assert e1 && e2[x <- x@bound]
    // only if e2 has an existential function
    class StripQuantifiers : StandardVisitor
    {
        static int boundVarCounter = 0;
        
        // 0 -> None, 1 -> Forall, 2 -> Exists, 3 -> Nested
        int insideQuantifier; 

        bool searchExistentialFunction;
        bool foundExistentialFunction;

        HashSet<string> existentialFunctions;
        Dictionary<string, LocalVariable> subst;
        List<LocalVariable> LocalsToAdd;

        private StripQuantifiers(HashSet<string> existentialFunctions)
        {
            this.existentialFunctions = existentialFunctions;
            insideQuantifier = 0;
            searchExistentialFunction = false;
            foundExistentialFunction = false;
            LocalsToAdd = new List<LocalVariable>();
            subst = null;
        }

        public static Tuple<Expr,List<LocalVariable>> Run(Expr expr, HashSet<string> existentialFunctions)
        {
            // check for type errors first
            var sq = new StripQuantifiers(existentialFunctions);
            var ret = sq.VisitExpr(expr);

            return Tuple.Create(ret, sq.LocalsToAdd);
        }

        public override Expr VisitExpr(Expr node)
        {
            if (node is QuantifierExpr)
            {
                return MyVisitQuantifierExpr(node as QuantifierExpr);
            }

            return base.VisitExpr(node);
        }

        private Expr MyVisitQuantifierExpr(QuantifierExpr node)
        {
            var oldIQ = insideQuantifier;
            Expr ret = node;

            // update "insideQuantifier"
            if (insideQuantifier == 0)
            {
                if (node is ForallExpr) insideQuantifier = 1;
                else insideQuantifier = 2;
            }
            else if (insideQuantifier > 0)
            {
                insideQuantifier = 3;
            }

            // Going inside Forall?
            if (insideQuantifier == 1)
            {
                // see if there is any existential function inside
                searchExistentialFunction = true;
                foundExistentialFunction = false;
                base.VisitQuantifierExpr(node);

                if (foundExistentialFunction)
                {
                    // create substitution to apply
                    subst = new Dictionary<string, LocalVariable>();
                    foreach (var bv in node.Dummies.OfType<Variable>())
                    {
                        var lv = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken,
                            bv + "@bound" + boundVarCounter, bv.TypedIdent.Type));
                        boundVarCounter++;
                        subst.Add(bv.Name, lv);
                        LocalsToAdd.Add(lv);
                    }

                    // apply the subst
                    var body = base.VisitExpr(node.Body);
                    ret = body;

                    subst = null;
                }
                else
                {
                    ret = base.VisitQuantifierExpr(node);
                }

                searchExistentialFunction = false;
                foundExistentialFunction = false;
            }
            else
            {
                ret = base.VisitQuantifierExpr(node);
            }

            insideQuantifier = oldIQ;
            return ret;
        }

        public override Expr VisitNAryExpr(NAryExpr node)
        {
            if (node.Fun is FunctionCall && existentialFunctions.Contains((node.Fun as FunctionCall).FunctionName))
            {
                if (insideQuantifier == 3)
                    throw new AbsHoudiniInternalError("Existential function found inside exists, or nested foralls");

                if (searchExistentialFunction)
                    foundExistentialFunction = true;

            }

            return base.VisitNAryExpr(node);
        }

        public override Expr VisitIdentifierExpr(IdentifierExpr node)
        {
            if (subst != null && subst.ContainsKey(node.Name))
                return Expr.Ident(subst[node.Name]);
            return base.VisitIdentifierExpr(node);
        }

    }

    public class Intervals : IAbstractDomain
    {
        // [lower, upper]
        int upper;
        int lower;
        // or: \bot
        bool isBottom;
        // number of times join has been performed
        int nJoin;
        // number of times before we widen
        readonly static int maxJoin = 5;

        public Intervals()
        {
            this.upper = 0;
            this.lower = 0;
            this.nJoin = 0;
            this.isBottom = true;
        }

        private Intervals(int lower, int upper, int nJoin)
        {
            this.upper = upper;
            this.lower = lower;
            this.nJoin = nJoin;
        }

        public IAbstractDomain Bottom()
        {
            return new Intervals();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            if (lower == Int32.MinValue && upper == Int32.MaxValue)
            {
                changed = false;
                return this;
            }
            changed = true;
            return new Intervals(Int32.MinValue, Int32.MaxValue, 0);
        }

        public IAbstractDomain Join(List<Model.Element> states)
        {
            Debug.Assert(states.Count == 1);
            var state = states[0] as Model.Integer;
            if (state == null)
                throw new AbsHoudiniInternalError("Incorrect type, expected int");
            var intval = state.AsInt();

            if (isBottom)
            {
                return new Intervals(intval, intval, 1);
            }

            if(intval >= lower && intval <= upper)
                return this;

            if (nJoin > maxJoin)
            {
                // widen
                if (intval > upper)
                    return new Intervals(lower, Int32.MaxValue, 1);
                if(intval < lower)
                    return new Intervals(Int32.MinValue, upper, 1);

                Debug.Assert(false);
            }

            if (intval > upper)
                return new Intervals(lower, intval, nJoin + 1);
            if (intval < lower)
                return new Intervals(intval, upper, nJoin + 1);

            Debug.Assert(false);
            return null;
        }

        public Expr Gamma(List<Expr> vars)
        {
            Debug.Assert(vars.Count == 1);
            var v = vars[0];
            if (isBottom) return Expr.False;
            Expr ret = Expr.True;
            if (lower != Int32.MinValue)
                ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower)));
            if (upper != Int32.MaxValue)
                ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper)));
            return ret;
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count != 1)
            {
                msg = "Illegal number of arguments";
                return false;
            }
            if (!argTypes[0].IsInt)
            {
                msg = "Illegal type, expecting int";
                return false;
            }
            return true;
        }
    }

    public class PredicateAbsElem : IAbstractDomain
    {
        public static class ExprExt
        {
            public static Expr AndSimp(Expr e1, Expr e2)
            {
                if (e1 == Expr.True) return e2;
                if (e2 == Expr.True) return e1;
                if (e1 == Expr.False || e2 == Expr.False) return Expr.False;
                return Expr.And(e1, e2);
            }

            public static Expr OrSimp(Expr e1, Expr e2)
            {
                if (e1 == Expr.False) return e2;
                if (e2 == Expr.False) return e1;
                if (e1 == Expr.True || e2 == Expr.True) return Expr.True;
                return Expr.Or(e1, e2); 
            }
        }

        class Disjunct
        {
            public static int DisjunctBound = 3;
            HashSet<int> pos;
            HashSet<int> neg;
            bool isTrue;

            public Disjunct()
            {
                isTrue = true;
                pos = new HashSet<int>();
                neg = new HashSet<int>();
            }

            public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
            {
                this.isTrue = false;
                this.pos = new HashSet<int>(pos);
                this.neg = new HashSet<int>(neg);
                if (this.pos.Overlaps(this.neg))
                {
                    this.isTrue = true;
                    this.pos = new HashSet<int>();
                    this.neg = new HashSet<int>();
                }
                if (this.pos.Count + this.neg.Count > DisjunctBound)
                {
                    // Set to true
                    this.isTrue = true;
                    this.pos = new HashSet<int>();
                    this.neg = new HashSet<int>();
                }

            }

            public Disjunct OR(Disjunct that)
            {
                if (isTrue)
                    return this;
                if (that.isTrue)
                    return that;

                return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
            }

            public bool Implies(Disjunct that)
            {
                if (isTrue) return that.isTrue;
                if (that.isTrue) return true;

                return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg);
            }

            public Expr Gamma(List<Expr> vars)
            {
                if (isTrue) return Expr.True;
                Expr ret = Expr.False;
                pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i]));
                neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i])));
                return ret;
            }
        }

        // Conjunction of Disjuncts
        List<Disjunct> conjuncts;
        bool isFalse;

        public PredicateAbsElem()
        {
            this.conjuncts = new List<Disjunct>();
            this.isFalse = true;
        }

        public IAbstractDomain Bottom()
        {
            return new PredicateAbsElem();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            if (conjuncts.Count == 0)
            {
                changed = false;
                return this;
            }
            changed = true;
            var ret = new PredicateAbsElem();
            ret.isFalse = false;
            return ret;
        }

        public IAbstractDomain Join(List<Model.Element> state)
        {
            if (state.Any(me => !(me is Model.Boolean)))
                throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool");

            // quick return if this == true
            if (!this.isFalse && conjuncts.Count == 0)
                return this;

            var ret = new PredicateAbsElem();
            ret.isFalse = false;

            for (int i = 0; i < state.Count; i++)
            {
                var b = (state[i] as Model.Boolean).Value;
                Disjunct d = null;
                if (b) d = new Disjunct(new int[] { i }, new int[] { });
                else d = new Disjunct(new int[] { }, new int[] { i });

                if (isFalse)
                    ret.AddDisjunct(d);
                else
                {
                    conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
                }
            }

            return ret;

        }

        public Expr Gamma(List<Expr> vars)
        {
            if (isFalse) return Expr.False;
            Expr ret = Expr.True;

            foreach (var c in conjuncts)
            {
                ret = ExprExt.AndSimp(ret, c.Gamma(vars));
            }

            return ret;
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Any(t => !t.IsBool))
            {
                msg = "Illegal type, expecting bool";
                return false;
            }
            return true;
        }

        private void AddDisjunct(Disjunct d)
        {
            if (conjuncts.Any(c => c.Implies(d)))
                return;

            conjuncts.RemoveAll(c => d.Implies(c));
            conjuncts.Add(d);
        }
    }

    // [false -- (x == true) -- true]
    public class HoudiniConst : IAbstractDomain
    {
        bool isBottom;
        bool isTop;

        private HoudiniConst(bool isTop, bool isBottom)
        {
            this.isBottom = isBottom;
            this.isTop = isTop;
            Debug.Assert(!(isTop && isBottom));
        }

        public static HoudiniConst GetExtObj()
        {
            return new HoudiniConst(false, false);
        }

        public static HoudiniConst GetTop()
        {
            return new HoudiniConst(true, false);
        }

        public static HoudiniConst GetBottom()
        {
            return new HoudiniConst(false, true);
        }

        public IAbstractDomain Bottom()
        {
            return GetBottom();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            changed = false;
            if (isTop) return this;
            changed = true;
            return GetTop();
        }

        public IAbstractDomain Join(List<Model.Element> states)
        {
            Debug.Assert(states.Count == 1);
            var state = states[0];

            if (isTop) return this;

            if (state is Model.Boolean)
            {
                if ((state as Model.Boolean).Value)
                    return GetExtObj();
            }

            return GetTop();
        }

        public Expr Gamma(List<Expr> vars)
        {
            Debug.Assert(vars.Count == 1);
            var v = vars[0];
            if (isBottom) return Expr.False;
            if (isTop) return Expr.True;
            return v;
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count != 1)
            {
                msg = "Illegal number of arguments, expecting 1";
                return false;
            }
            if (!argTypes[0].IsBool)
            {
                msg = "Illegal type, expecting bool";
                return false;
            }
            return true;
        }
    }

    // foo(x) = x < 2^j for some j <= 16
    public class PowDomain : IAbstractDomain
    {
        enum Val { FALSE, NEITHER, TRUE };
        Val tlevel;
        bool isBottom { get { return tlevel == Val.FALSE; } }
        bool isTop { get { return tlevel == Val.TRUE; } }

        readonly int Max = 16;

        int upper; // <= Max

        private PowDomain(Val tlevel) :
            this(tlevel, 0) { }

        private PowDomain(Val tlevel, int upper)
        {
            this.tlevel = tlevel;
            this.upper = upper;
        }

        public static IAbstractDomain GetBottom()
        {
            return new PowDomain(Val.FALSE) as IAbstractDomain;
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            if (isTop)
            {
                changed = false;
                return this;
            }
            changed = true;
            return new PowDomain(Val.TRUE);
        }

        IAbstractDomain IAbstractDomain.Bottom()
        {
            return GetBottom();
        }

        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
        {
            if (isTop) return this;
            
            int v = 0;
            if (state[0] is Model.BitVector)
                v = (state[0] as Model.BitVector).AsInt();
            else if (state[0] is Model.Integer)
                v = (state[0] as Model.Integer).AsInt();
            else Debug.Assert(false);

            var nupper = upper;
            while ((1 << nupper) < v) nupper++;
            var ntlevel = Val.NEITHER;
            if (nupper > Max) ntlevel = Val.TRUE;
            return new PowDomain(ntlevel, nupper);
        }

        Expr IAbstractDomain.Gamma(List<Expr> vars)
        {
            if (isBottom) return Expr.False;
            if (isTop) return Expr.True;
            var v = vars[0];
            if (v.Type.IsBv)
            {
                var bits = v.Type.BvBits;
                if (!AbstractDomainFactory.bvslt.ContainsKey(bits))
                    throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString());
                var bvslt = AbstractDomainFactory.bvslt[bits];
                return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new List<Expr> { v,
                    new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32) });
            }
            else
            {
                return Expr.Lt(v, Expr.Literal(1 << (upper+1)));
            }
        }

        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count != 1)
            {
                msg = "Illegal number of arguments, expecting 1";
                return false;
            }
            if (argTypes.Any(tt => !tt.IsInt && !tt.IsBv))
            {
                msg = "Illegal type, expecting int or bv";
                return false;
            }
            return true;
        }
    }

    // foo(x_i) = all equalities that hold
    public class EqualitiesDomain : IAbstractDomain
    {
        bool isBottom;
        List<HashSet<int>> equalities;

        public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq)
        {
            this.isBottom = isBottom;
            this.equalities = eq;
        }

        public static IAbstractDomain GetBottom()
        {
            return new EqualitiesDomain(true, new List<HashSet<int>>());
        }

        IAbstractDomain IAbstractDomain.Bottom()
        {
            return GetBottom();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            if (equalities.Count == 0)
            {
                changed = false;
                return this;
            }
            changed = true;
            return new EqualitiesDomain(false, new List<HashSet<int>>());
        }

        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
        {
            // find the guys that are equal
            var eq = new List<HashSet<int>>();
            for (int i = 0; i < state.Count; i++)
            {
                var added = false;
                foreach (var s in eq)
                {
                    var sv = s.First();
                    if (state[i].ToString() == state[sv].ToString())
                    {
                        s.Add(i);
                        added = true;
                        break;
                    }
                }
                if (!added) eq.Add(new HashSet<int>(new int[] { i }));
            }
            
            if (isBottom)
            {
                return new EqualitiesDomain(false, eq);
            }

            // intersect two partitions equalities and eq
            var m1 = GetMap(equalities, state.Count);
            var m2 = GetMap(eq, state.Count);

            for (int i = 0; i < state.Count; i++)
                m2[i] = new HashSet<int>(m2[i].Intersect(m1[i]));


            // map from representative to set
            var repToSet = new Dictionary<int, HashSet<int>>();

            for (int i = 0; i < state.Count; i++)
            {
                var rep = m2[i].Min();
                if (!repToSet.ContainsKey(rep))
                    repToSet[rep] = m2[i];
            }

            var ret = new List<HashSet<int>>();
            repToSet.Values.Iter(s => ret.Add(s));

            return new EqualitiesDomain(false, ret);
        }

        Expr IAbstractDomain.Gamma(List<Expr> vars)
        {
            if (isBottom) return Expr.False;
            Expr ret = Expr.True;
            foreach (var eq in equalities.Select(hs => hs.ToList()))
            {
                if (eq.Count == 1) continue;
                var prev = eq[0];
                for (int i = 1; i < eq.Count; i++)
                {
                    ret = Expr.And(ret, Expr.Eq(vars[prev], vars[eq[i]]));
                    prev = eq[i];
                }
            }
            return ret;
        }

        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count == 0) return true;
            var ot = argTypes[0];

            if (argTypes.Any(tt => !tt.Equals(ot)))
            {
                msg = string.Format("Illegal type, expecting type {0}, got {1}", ot, argTypes.First(tt => !tt.Equals(ot)));
                return false;
            }
            return true;
        }

        private HashSet<int>[] GetMap(List<HashSet<int>> eq, int n)
        {
            var ret = new HashSet<int>[n];
            foreach (var s in eq)
            {
                foreach (var i in s)
                    ret[i] = s;
            }
            return ret;
        }
    }

    // foo(a,b) \in {false, \not a, a ==> b, true}
    public class ImplicationDomain : IAbstractDomain
    {
        enum Val {FALSE, NOT_A, A_IMP_B, TRUE};
        Val val;

        private ImplicationDomain(Val val)
        {
            this.val = val;
        }

        public static ImplicationDomain GetBottom()
        {
            return new ImplicationDomain(Val.FALSE);
        }

        public IAbstractDomain Bottom()
        {
            return GetBottom();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            if(val == Val.TRUE) {
                changed = false;
                return this;
            }
            changed = true;
            return new ImplicationDomain(Val.TRUE);
        }

        public IAbstractDomain Join(List<Model.Element> states)
        {
            Debug.Assert(states.Count == 2);
            var v1 = (states[0] as Model.Boolean).Value;
            var v2 = (states[1] as Model.Boolean).Value;

            if (val == Val.TRUE) return this;

            var that = Val.TRUE;
            if (!v1) that = Val.NOT_A;
            else if (!v1 || v2) that = Val.A_IMP_B;

            if (that == Val.TRUE || val == Val.FALSE)
                return new ImplicationDomain(that);

            // Now, neither this or that is FALSE or TRUE
            if (val == that)
                return this;

            Debug.Assert(val == Val.A_IMP_B || that == Val.A_IMP_B);
            return new ImplicationDomain(Val.A_IMP_B);
        }

        public Expr Gamma(List<Expr> vars)
        {
            Debug.Assert(vars.Count == 2);

            var v1 = vars[0];
            var v2 = vars[1];

            if (val == Val.FALSE) return Expr.False;
            if (val == Val.TRUE) return Expr.True;
            if (val == Val.NOT_A) return Expr.Not(v1);
            return Expr.Imp(v1, v2);
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count != 2)
            {
                msg = "Illegal number of arguments, expecting 2";
                return false;
            }
            if (argTypes.Any(tt => !tt.IsBool))
            {
                msg = "Illegal type, expecting bool";
                return false;
            }
            return true;
        }
    }

    public class ConstantProp : IAbstractDomain
    {
        object val;
        bool isBottom;
        bool isTop;

        private ConstantProp(object val, bool isTop, bool isBottom)
        {
            this.val = val;
            this.isBottom = isBottom;
            this.isTop = isTop;
            Debug.Assert(!(isTop && isBottom));
            Debug.Assert(val == null || (val is int) || (val is bool));
        }

        public static ConstantProp GetExtObj(object val)
        {
            Debug.Assert(val != null);
            return new ConstantProp(val, false, false);
        }

        public static ConstantProp GetTop()
        {
            return new ConstantProp(null, true, false);
        }

        public static ConstantProp GetBottom()
        {
            return new ConstantProp(null, false, true);
        }

        public IAbstractDomain MakeTop(out bool changed) {
            if (isTop)
            {
                changed = false;
                return this;
            }
            changed = true;
            return GetTop();
        }

        private ConstantProp Join(ConstantProp that)
        {
            if (isBottom) return that;
            if (isTop) return this;
            if (that.isBottom) return this;
            if (that.isTop) return that;

            if ((val is int) && !(that.val is int))
                throw new AbsHoudiniInternalError("Type mismatch in ExtObj");

            if ((val is bool) && !(that.val is bool))
                throw new AbsHoudiniInternalError("Type mismatch in ExtObj");

            if (val is int)
            {
                var v1 = (int)val;
                var v2 = (int)that.val;
                if (v1 != v2) return GetTop();
                return this;
            }
            else if (val is bool)
            {
                var v1 = (bool)val;
                var v2 = (bool)that.val;
                if (v1 != v2) return GetTop();
                return this;
            }
            throw new AbsHoudiniInternalError("Illegal val type in ExtObj");
        }

        public IAbstractDomain Bottom()
        {
            return GetBottom();
        }

        public IAbstractDomain Join(List<Model.Element> states)
        {
            Debug.Assert(states.Count == 1);
            var state = states[0];
            ConstantProp that = null;

            if (state is Model.Integer)
            {
                that = GetExtObj((state as Model.Integer).AsInt());
            }
            else if (state is Model.Boolean)
            {
                that = GetExtObj((state as Model.Boolean).Value);
            }
            else
            {
                throw new AbsHoudiniInternalError("Illegal type " + state.GetType().ToString());
            }

            return Join(that);
        }

        public Expr Gamma(List<Expr> vars)
        {
            Debug.Assert(vars.Count == 1);
            var v = vars[0];
            if (isBottom) return Expr.False;
            if (isTop) return Expr.True;
            if (val is int)
                return Expr.Eq(v, Expr.Literal((int)val));
            if (val is bool && (bool)val)
                return v;
            if (val is bool && !(bool)val)
                return Expr.Not(v);

            return null;
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            msg = "";
            if (argTypes.Count != 1)
            {
                msg = "Illegal number of arguments, expecting 1";
                return false;
            }
            if (!argTypes[0].IsInt && ! argTypes[0].IsBool)
            {
                msg = "Illegal type, expecting int or bool";
                return false;
            }
            return true;
        }
    }


    public class IndependentAttribute<T> : IAbstractDomain where T : class, IAbstractDomain
    {
        bool isBottom;
        int numVars;
        List<T> varVal;
        T underlyingInstance;

        public IndependentAttribute()
        {
            isBottom = true;
            numVars = 0;
            varVal = new List<T>();
            underlyingInstance = null;
        }

        public IAbstractDomain Bottom()
        {
            return new IndependentAttribute<T>();
        }

        public IAbstractDomain MakeTop(out bool changed)
        {
            var mt = new Func<IAbstractDomain>(() =>
                {
                    var ret = new IndependentAttribute<T>();
                    ret.isBottom = true;
                    ret.numVars = numVars;
                    ret.underlyingInstance = underlyingInstance;
                    ret.varVal = new List<T>();
                    bool tmp;
                    for (int i = 0; i < varVal.Count; i++)
                        ret.varVal.Add(varVal[i].MakeTop(out tmp) as T);
                    return ret;
                });

            if (!isBottom)
            {
                foreach (var t in varVal)
                {
                    var top = t.MakeTop(out changed);
                    if (changed)
                    {
                        return mt();
                    }
                }
            }
            else
            {
                changed = true;
                return mt();
            }

            changed = false;
            return this;
        }
        public IAbstractDomain Join(List<Model.Element> state)
        {
            SetUnderlyingInstance();

            if (!isBottom && numVars != state.Count)
            {
                throw new AbsHoudiniInternalError(
                    string.Format("Got illegal number of arguments ({0}), expected {1}", state.Count, numVars));
            }

            var ret = new IndependentAttribute<T>();
            ret.isBottom = false;
            ret.numVars = state.Count;
            for(int i = 0; i < state.Count; i++)
            {
                var sl = new List<Model.Element>();
                sl.Add(state[i]);
                T prev = isBottom ? underlyingInstance.Bottom() as T : varVal[i];
                ret.varVal.Add(prev.Join(sl) as T);
            }

            return ret;
        }

        public Expr Gamma(List<Expr> vars)
        {
            if (isBottom) return Expr.False;
            if (numVars != vars.Count)
                throw new AbsHoudiniInternalError(
                    string.Format("Got illegal number of arguments ({0}), expected {1}", vars.Count, numVars));

            Expr ret = Expr.True;
            for (int i = 0; i < numVars; i++)
            {
                var sl = new List<Expr>(); sl.Add(vars[i]);
                ret = Expr.And(ret, varVal[i].Gamma(sl));
            }

            return ret;
        }

        private void SetUnderlyingInstance()
        {
            if (underlyingInstance != null) return;
            var tt = typeof(T);
            underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T;
        }

        public bool TypeCheck(List<Type> argTypes, out string msg)
        {
            SetUnderlyingInstance();

            msg = "";
            foreach(var t in argTypes) 
            {
                if(!underlyingInstance.TypeCheck(new List<Type>(new Type[] { t }), out msg))
                    return false;
            }
            return true;
        }
    }

    public class AbstractDomainFactory
    {
        // Type name -> Instance
        private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();
        private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>();
        
        // bitvector operations
        public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>();

        public static void Register(string friendlyName, IAbstractDomain instance)
        {
            var Name = instance.GetType().FullName;
            Debug.Assert(!abstractDomainInstances.ContainsKey(Name));
            abstractDomainInstances.Add(Name, instance);
            abstractDomainInstancesFriendly.Add(friendlyName, instance);
        }

        public static IAbstractDomain GetInstance(System.Type type)
        {
            var Name = type.FullName;
            Debug.Assert(abstractDomainInstances.ContainsKey(Name));
            return abstractDomainInstances[Name] as IAbstractDomain;
        }

        public static IAbstractDomain GetInstance(string friendlyName)
        {
            if (!abstractDomainInstancesFriendly.ContainsKey(friendlyName))
            {
                Console.WriteLine("Domain {0} not found", friendlyName);
                Console.WriteLine("Supported domains are:");
                abstractDomainInstancesFriendly.Keys.Iter(tup => Console.WriteLine("  {0}", tup));
                throw new AbsHoudiniInternalError("Domain not found");
            }
            return abstractDomainInstancesFriendly[friendlyName] as IAbstractDomain;
        }

        public static void Initialize(Program program)
        {
            // Declare abstract domains
            var domains = new List<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {
                  System.Tuple.Create("HoudiniConst", HoudiniConst.GetBottom() as IAbstractDomain),
                  System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),
                  System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),
                  System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),
                  System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),
                  System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),
                  System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),
                  System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute<HoudiniConst>()  as IAbstractDomain),
                  System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>()  as IAbstractDomain),
                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain),
                  System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() as IAbstractDomain),
              });

            domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));
            program.TopLevelDeclarations.OfType<Function>()
                .Iter(RegisterFunction);
        }

        private static void RegisterFunction(Function func)
        {
            var attr = QKeyValue.FindStringAttribute(func.Attributes, "bvbuiltin");
            if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv)
                bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func);
        }
    }

    public interface IAbstractDomain
    {
        IAbstractDomain Bottom();
        IAbstractDomain MakeTop(out bool changed);
        IAbstractDomain Join(List<Model.Element> state);
        Expr Gamma(List<Expr> vars);
        bool TypeCheck(List<Type> argTypes, out string msg);
    }

    public class AbstractHoudini
    {
        // Input Program
        Program program;
        // Impl -> VC
        Dictionary<string, VCExpr> impl2VC;
        // Impl -> Vars at end of the impl
        Dictionary<string, List<VCExpr>> impl2EndStateVars;
        // Impl -> (callee,summary pred)
        Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>> impl2CalleeSummaries;
        // pointer to summary class
        ISummaryElement summaryClass;
        // impl -> summary
        Dictionary<string, ISummaryElement> impl2Summary;
        // name -> impl
        Dictionary<string, Implementation> name2Impl;
        // Use Bilateral algorithm
        public static bool UseBilateralAlgo = true;
        public static int iterTimeLimit = -1; // ms

        public static readonly string summaryPredSuffix = "SummaryPred";

        // Essentials: VCGen, Prover, and reporter
        VCGen vcgen;
        ProverInterface prover;
        AbstractHoudiniErrorReporter reporter;

        // Stats
        TimeSpan proverTime;
        int numProverQueries;

        // Produce witness for correctness: can be set programmatically
        public static string WitnessFile = "absHoudiniWitness.bpl";

        public AbstractHoudini(Program program)
        {
            this.program = program;
            this.impl2VC = new Dictionary<string, VCExpr>();
            this.impl2EndStateVars = new Dictionary<string, List<VCExpr>>();
            this.impl2CalleeSummaries = new Dictionary<string, List<Tuple<string, bool, VCExprVar, VCExprNAry>>>();
            this.impl2Summary = new Dictionary<string, ISummaryElement>();
            this.name2Impl = SimpleUtil.nameImplMapping(program);

            if (CommandLineOptions.Clo.ProverKillTime > 0)
                CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));

            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

            this.reporter = new AbstractHoudiniErrorReporter();

            this.proverTime = TimeSpan.Zero;
            this.numProverQueries = 0;

            if (CommandLineOptions.Clo.AbstractHoudini == "0")
                UseBilateralAlgo = false;
        }

        public void computeSummaries(ISummaryElement summaryClass)
        {
            // TODO: move this some place else
            PredicateAbs.FindUnsatPairs(prover.VCExprGen, prover);

            this.summaryClass = summaryClass;

            name2Impl.Values.Iter(attachEnsures);

            program.TopLevelDeclarations
                .OfType<Implementation>()
                .Iter(impl => impl2Summary.Add(impl.Name, summaryClass.GetFlaseSummary(program, impl)));

            // Build call graph
            var Succ = new Dictionary<Implementation, HashSet<Implementation>>();
            var Pred = new Dictionary<Implementation, HashSet<Implementation>>();
            name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet<Implementation>()));
            name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>()));

            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
            {
                foreach (var blk in impl.Blocks)
                {
                    foreach (var cmd in blk.Cmds.OfType<CallCmd>())
                    {
                        if (!name2Impl.ContainsKey(cmd.callee)) continue;
                        Succ[impl].Add(name2Impl[cmd.callee]);
                        Pred[name2Impl[cmd.callee]].Add(impl);
                    }
                }
            }

            // Build SCC
            var sccs = new StronglyConnectedComponents<Implementation>(name2Impl.Values,
                new Adjacency<Implementation>(n => Pred[n]),
                new Adjacency<Implementation>(n => Succ[n]));
            sccs.Compute();

            // impl -> priority
            var impl2Priority = new Dictionary<string, int>();
            int p = 0;
            foreach (var scc in sccs)
            {
                foreach (var impl in scc)
                {
                    impl2Priority.Add(impl.Name, p);
                    p++;
                }
            }


            Inline();

            #region Witness generation setup
            // Create a copy of the program
            var copy = new Dictionary<string, Implementation>();
            if (WitnessFile != null)
            {
                foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
                {
                    var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,
                        impl.InParams, impl.OutParams, new List<Variable>(impl.LocVars), new List<Block>());
                    foreach (var blk in impl.Blocks)
                    {
                        var cd = new CodeCopier();
                        nimpl.Blocks.Add(new Block(Token.NoToken, blk.Label,
                            cd.CopyCmdSeq(blk.Cmds), cd.CopyTransferCmd(blk.TransferCmd)));
                    }

                    copy.Add(impl.Name, nimpl);
                }
            }
            #endregion

            // Turn off subsumption. Why? Because then I see multiple occurences of the
            // attached ensures in the VC
            CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never;

            // Create all VCs
            name2Impl.Values
                .Iter(GenVC);

            // Start the iteration
            var worklist = new SortedSet<Tuple<int, Implementation>>();
            name2Impl.Values
                .Iter(impl => worklist.Add(Tuple.Create(impl2Priority[impl.Name], impl)));

            while (worklist.Any())
            {
                var impl = worklist.First().Item2;
                worklist.Remove(worklist.First());

                var changed = ProcessImpl(impl);

                if (changed)
                {
                    Pred[impl].Where(pred => UseBilateralAlgo || pred != impl).Iter(pred => worklist.Add(Tuple.Create(impl2Priority[pred.Name], pred)));
                }
            }

            var allImpls = new SortedSet<Tuple<int, string>>();
            name2Impl.Values.Iter(impl => allImpls.Add(Tuple.Create(impl2Priority[impl.Name], impl.Name)));
            if (CommandLineOptions.Clo.Trace)
            {
                foreach (var tup in allImpls)
                {
                    Console.WriteLine("Summary of {0}:", tup.Item2);
                    Console.WriteLine("{0}", impl2Summary[tup.Item2]);
                }
                Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2"));
                Console.WriteLine("Number of prover queries = " + numProverQueries);
            }

            ProduceWitness(copy);

            prover.Close();
            CommandLineOptions.Clo.TheProverFactory.Close();
        }

        public HashSet<string> GetPredicates()
        {
            var ret = new HashSet<string>();
            prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

            foreach (var tup in impl2Summary)
            {
                var s = tup.Value as PredicateAbs;
                if (s == null) continue;
                ret.UnionWith(s.GetPredicates(program, prover.VCExprGen, prover));
                // debug output
                //Console.WriteLine("Summary of {0}:", tup.Key);
                //Console.WriteLine("{0}", tup.Value);
            }

            prover.Close();
            CommandLineOptions.Clo.TheProverFactory.Close();
            return ret;
        }

        // Obtain the summary expression for a procedure: used programmatically by clients
        // of AbstractHoudini
        public Expr GetSummary(Program program, Procedure proc)
        {
            if (!impl2Summary.ContainsKey(proc.Name))
                return Expr.True;

            var vars = new Dictionary<string, Expr>();
            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
                vars.Add(g.Name, Expr.Ident(g));
            foreach (var v in proc.InParams.OfType<Variable>())
                vars.Add(v.Name, Expr.Ident(v));
            foreach (var v in proc.OutParams.OfType<Variable>())
                vars.Add(v.Name, Expr.Ident(v));

            return impl2Summary[proc.Name].GetSummaryExpr(
                v => { if (vars.ContainsKey(v)) return vars[v]; else return null; },
                v => { if (vars.ContainsKey(v)) return new OldExpr(Token.NoToken, vars[v]); else return null; });
        }

        public ISummaryElement GetSummaryLowLevel(Procedure proc)
        {
            if (!impl2Summary.ContainsKey(proc.Name)) return null;
            return impl2Summary[proc.Name];
        }

        // Produce a witness that proves that the inferred annotations are correct
        private void ProduceWitness(Dictionary<string, Implementation> copy)
        {
            if (WitnessFile == null)
                return;

            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
            {
                var nensures = new List<Ensures>();
                proc.Ensures.OfType<Ensures>()
                .Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") &&
                    !QKeyValue.FindBoolAttribute(ens.Attributes, "pre") &&
                    !QKeyValue.FindBoolAttribute(ens.Attributes, "post") &&
                    QKeyValue.FindStringAttribute(ens.Attributes, "pre") == null &&
                    QKeyValue.FindStringAttribute(ens.Attributes, "post") == null)
                .Iter(ens => nensures.Add(ens));
                foreach (Ensures en in nensures)
                    en.Attributes = removeAttr("InlineAssume", en.Attributes);

                proc.Ensures = nensures;
            }

            var decls = new List<Declaration>();
            copy.Values.Iter(impl => decls.Add(impl));
            program.TopLevelDeclarations.Where(decl => !(decl is Implementation))
                .Iter(decl => decls.Add(decl));
            program.TopLevelDeclarations = decls;
            var name2Proc = new Dictionary<string, Procedure>();
            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
            {
                name2Proc.Add(proc.Name, proc);
                if (impl2Summary.ContainsKey(proc.Name))
                {
                    var ens = new Ensures(false, 
                        impl2Summary[proc.Name].GetSummaryExpr(
                        new Func<string, Expr>(s => null), new Func<string, Expr>(s => null)));
                    ens.Attributes = new QKeyValue(Token.NoToken, "inferred", new List<object>(), ens.Attributes);
                    proc.Ensures.Add(ens);
                }
            }

            using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false))
            {
                program.Emit(wt);
            }

            // Replace SummaryPreds with their definition
            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
            {
                foreach (var blk in impl.Blocks)
                {
                    foreach (var cmd in blk.Cmds.OfType<AssumeCmd>())
                    {
                        var expr = cmd.Expr as NAryExpr;
                        if (expr == null) continue;
                        var op = expr.Fun as FunctionCall;
                        if (op == null || !op.FunctionName.EndsWith(summaryPredSuffix)) continue;
                        var calleeName = op.FunctionName.Substring(0, op.FunctionName.Length - summaryPredSuffix.Length);
                        if (!impl2Summary.ContainsKey(calleeName)) continue;
                        var callee = name2Impl[calleeName];

                        // variable order: globals, ins, outs, modifies
                        var forold = new Dictionary<string, Expr>();
                        var always = new Dictionary<string, Expr>();
                        int i = 0;
                        foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
                        {
                            forold.Add(g.Name, expr.Args[i]);
                            always.Add(g.Name, expr.Args[i]);
                            i++;
                        }
                        foreach (var v in callee.InParams.OfType<Variable>())
                        {
                            always.Add(v.Name, expr.Args[i]);
                            i++;
                        }
                        foreach (var v in callee.OutParams.OfType<Variable>())
                        {
                            always.Add(v.Name, expr.Args[i]);
                            i++;
                        }
                        foreach (var ie in name2Proc[calleeName].Modifies.OfType<IdentifierExpr>())
                        {
                            always[ie.Name] = expr.Args[i];
                            i++;
                        }

                        cmd.Expr = impl2Summary[calleeName].GetSummaryExpr(
                            v => { if (always.ContainsKey(v)) return always[v]; else return null; },
                            v => { if (forold.ContainsKey(v)) return forold[v]; else return null; });
                    }
                }
            }

            using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false))
            {
                program.Emit(wt);
            }
            if (CommandLineOptions.Clo.Trace) Console.WriteLine("Witness written to {0}", WitnessFile);
        }

        private QKeyValue removeAttr(string key, QKeyValue attr)
        {
            if (attr == null) return attr;
            if (attr.Key == key) return removeAttr(key, attr.Next);
            attr.Next = removeAttr(key, attr.Next);
            return attr;
        }

        private void Inline()
        {
            if (CommandLineOptions.Clo.InlineDepth < 0)
                return;

            var callGraph = BuildCallGraph();

            foreach (Implementation impl in callGraph.Nodes)
            {
                InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
                inlineEnsuresVisitor.Visit(impl);
            }

            foreach (Implementation impl in callGraph.Nodes)
            {
                impl.OriginalBlocks = impl.Blocks;
                impl.OriginalLocVars = impl.LocVars;
            }
            foreach (Implementation impl in callGraph.Nodes)
            {
                CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
                CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
                Inliner.ProcessImplementationForHoudini(program, impl);
                CommandLineOptions.Clo.ProcedureInlining = savedOption;
            }
            foreach (Implementation impl in callGraph.Nodes)
            {
                impl.OriginalBlocks = null;
                impl.OriginalLocVars = null;
            }

            Graph<Implementation> oldCallGraph = callGraph;
            callGraph = new Graph<Implementation>();
            foreach (Implementation impl in oldCallGraph.Nodes)
            {
                callGraph.AddSource(impl);
            }
            foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
            {
                callGraph.AddEdge(edge.Item1, edge.Item2);
            }
            int count = CommandLineOptions.Clo.InlineDepth;
            while (count > 0)
            {
                foreach (Implementation impl in oldCallGraph.Nodes)
                {
                    List<Implementation> newNodes = new List<Implementation>();
                    foreach (Implementation succ in callGraph.Successors(impl))
                    {
                        newNodes.AddRange(oldCallGraph.Successors(succ));
                    }
                    foreach (Implementation newNode in newNodes)
                    {
                        callGraph.AddEdge(impl, newNode);
                    }
                }
                count--;
            }
        }

        private Graph<Implementation> BuildCallGraph()
        {
            Graph<Implementation> callGraph = new Graph<Implementation>();
            Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Procedure proc = decl as Procedure;
                if (proc == null) continue;
                procToImpls[proc] = new HashSet<Implementation>();
            }
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Implementation impl = decl as Implementation;
                if (impl == null || impl.SkipVerification) continue;
                callGraph.AddSource(impl);
                procToImpls[impl.Proc].Add(impl);
            }
            foreach (Declaration decl in program.TopLevelDeclarations)
            {
                Implementation impl = decl as Implementation;
                if (impl == null || impl.SkipVerification) continue;
                foreach (Block b in impl.Blocks)
                {
                    foreach (Cmd c in b.Cmds)
                    {
                        CallCmd cc = c as CallCmd;
                        if (cc == null) continue;
                        foreach (Implementation callee in procToImpls[cc.Proc])
                        {
                            callGraph.AddEdge(impl, callee);
                        }
                    }
                }
            }
            return callGraph;
        }


        private bool ProcessImpl(Implementation impl)
        {
            var ret = false;
            var gen = prover.VCExprGen;

            // construct summaries
            var env = VCExpressionGenerator.True;
            foreach (var tup in impl2CalleeSummaries[impl.Name])
            {
                // Not Bilateral: then reject self predicates
                if (UseBilateralAlgo == false && tup.Item1 == impl.Name)
                    continue;

                // Bilateral: only reject self summary
                if (UseBilateralAlgo == true && tup.Item1 == impl.Name && tup.Item2)
                    continue;

                var calleeSummary = 
                    impl2Summary[tup.Item1].GetSummaryExpr(
                       GetVarMapping(name2Impl[tup.Item1], tup.Item4), prover.VCExprGen);
                env = gen.AndSimp(env, gen.Eq(tup.Item3, calleeSummary));
            }

            var prev = impl2Summary[impl.Name].Copy();
            var upper = impl2Summary[impl.Name].GetTrueSummary(program, impl);
            var sw = new Stopwatch();
            sw.Start();
            var lowerTime = TimeSpan.Zero;

            while(true)
            {
                var usedLower = true;
                var query = impl2Summary[impl.Name];
                sw.Restart();

                // construct self summaries
                var summaryExpr = VCExpressionGenerator.True;
                foreach (var tup in impl2CalleeSummaries[impl.Name])
                {
                    if (UseBilateralAlgo == false && tup.Item1 != impl.Name)
                        continue;
                    if (UseBilateralAlgo == true && (tup.Item1 != impl.Name || !tup.Item2))
                        continue;
                    
                    if (UseBilateralAlgo)
                    {
                        query = query.AbstractConsequence(upper);
                        if (query == null) query = impl2Summary[tup.Item1];
                        else usedLower = false;
                    }

                    var ts =
                        query.GetSummaryExpr(
                           GetVarMapping(name2Impl[tup.Item1], tup.Item4), prover.VCExprGen);
                    summaryExpr = gen.AndSimp(summaryExpr, gen.Eq(tup.Item3, ts));
                }
                //Console.WriteLine("Trying summary for {0}: {1}", impl.Name, summaryExpr);

                reporter.model = null;
                var vc = gen.AndSimp(env, summaryExpr);
                vc = gen.Implies(vc, impl2VC[impl.Name]);
                
                //Console.WriteLine("Checking: {0}", vc);
                if (CommandLineOptions.Clo.Trace)
                    Console.WriteLine("Verifying {0} ({1}): {2}", impl.Name, usedLower ? "lower" : "ac", query);

                if (usedLower && lowerTime.TotalMilliseconds >= iterTimeLimit && iterTimeLimit >= 0)
                {
                    if (UseBilateralAlgo)
                    {
                        if (CommandLineOptions.Clo.Trace)
                            Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name);
                        ret = prev.IsEqual(upper) ? false : true;
                        impl2Summary[impl.Name] = upper;
                        break;
                    }
                    else
                    {
                        if (CommandLineOptions.Clo.Trace)
                            Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name);
                        var tt = impl2Summary[impl.Name].GetTrueSummary(program, impl);
                        ret = prev.IsEqual(tt) ? false : true; ;
                        impl2Summary[impl.Name] = tt;
                        break;
                    }
                }

                var start = DateTime.Now;

                //prover.Push();
                //prover.Assert(gen.Not(vc), true);
                //prover.FlushAxiomsToTheoremProver();
                //prover.Check();
                //ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter);
                //prover.Pop();

                prover.BeginCheck(impl.Name, vc, reporter);
                ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter);

                var inc = (DateTime.Now - start);
                proverTime += inc;
                numProverQueries++;

                sw.Stop();
                if (usedLower) lowerTime += sw.Elapsed;

                if(CommandLineOptions.Clo.Trace)
                    Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString()); 

                if (UseBilateralAlgo)
                {
                    if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
                    {
                        if(CommandLineOptions.Clo.Trace)
                            Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name);
                        ret = prev.IsEqual(upper) ? false : true;
                        impl2Summary[impl.Name] = upper;
                        break;
                    }
                    
                    if (reporter.model == null && usedLower)
                        break;

                    if (reporter.model == null)
                    {
                        upper.Meet(query);
                    }
                    else
                    {
                        var state = CollectState(impl);
                        impl2Summary[impl.Name].Join(state, reporter.model);
                        ret = true;
                    }
                }
                else
                {
                    if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
                    {
                        if (CommandLineOptions.Clo.Trace)
                            Console.WriteLine("Timeout/Spaceout while verifying " + impl.Name);
                        var tt = impl2Summary[impl.Name].GetTrueSummary(program, impl);
                        ret = prev.IsEqual(tt) ? false : true; ;
                        impl2Summary[impl.Name] = tt;
                        break;
                    }

                    if (reporter.model == null)
                        break;
                    //reporter.model.Write(Console.Out);

                    var state = CollectState(impl);
                    impl2Summary[impl.Name].Join(state, reporter.model);
                    ret = true;
                }
            }
            return ret;
        }

        private Dictionary<string, VCExpr> GetVarMapping(Implementation impl, VCExprNAry summaryPred)
        {
            var ret = new Dictionary<string, VCExpr>();

            var cnt = 0;
            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
            {
                ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]);
                cnt++;
            }
            foreach (var v in impl.InParams.OfType<Variable>().Concat(
                impl.OutParams.OfType<Variable>().Concat(
                impl.Proc.Modifies.OfType<IdentifierExpr>().Select(ie => ie.Decl))))
            {
                ret.Add(v.Name, summaryPred[cnt]);
                cnt++;
            }

            // Fill up values of globals that are not modified
            cnt = 0;
            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
            {
                if (ret.ContainsKey(g.Name)) { cnt++; continue; }

                ret.Add(string.Format("{0}", g.Name), summaryPred[cnt]);
                cnt++;
            }

            // Constants
            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
            {
                var value = prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c));
                ret.Add(string.Format("{0}", c.Name), value);
                ret.Add(string.Format("old({0})", c.Name), value);
            }

            return ret;
        }

        private Dictionary<string, Model.Element> CollectState(Implementation impl)
        {
            var ret = new Dictionary<string, Model.Element>();

            var model = reporter.model;
            var implVars = impl2EndStateVars[impl.Name];

            var cnt = 0;
            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
            {
                ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model));
                cnt++;
            }
            foreach (var v in impl.InParams.OfType<Variable>().Concat(
                impl.OutParams.OfType<Variable>().Concat(
                impl.Proc.Modifies.OfType<IdentifierExpr>().Select(ie => ie.Decl))))
            {
                ret.Add(v.Name, getValue(implVars[cnt], model));
                cnt++;
            }

            // Fill up values of globals that are not modified
            cnt = 0;
            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
            {
                if (ret.ContainsKey(g.Name)) { cnt++; continue; }

                ret.Add(string.Format("{0}", g.Name), getValue(implVars[cnt], model));
                cnt++;
            }

            // Constants
            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
            {
                try
                {
                    var value = getValue(prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c)), model);
                    ret.Add(string.Format("{0}", c.Name), value);
                    ret.Add(string.Format("old({0})", c.Name), value);
                }
                catch (Exception)
                {
                    // constant not assigned a value: add a default value
                    Model.Element value = null;
                    if (c.TypedIdent.Type.IsInt)
                        value = model.MkIntElement(0);
                    else if (c.TypedIdent.Type.IsBool)
                        value = model.MkElement("false");

                    ret.Add(string.Format("{0}", c.Name), value);
                    ret.Add(string.Format("old({0})", c.Name), value);
                }
            }

            return ret;
        }

        private Model.Element getValue(VCExpr arg, Model model)
        {
            if (arg is VCExprLiteral)
            {
                //return model.GetElement(arg.ToString());
                return model.MkElement(arg.ToString());
            }
            else if (arg is VCExprVar)
            {
                var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
                if (el != null)
                {
                    Debug.Assert(el.Arity == 0 && el.AppCount == 1);
                    return el.Apps.First().Result;
                }
                else
                {
                    // Variable not defined; assign arbitrary value
                    if (arg.Type.IsBool)
                        return model.MkElement("false");
                    else if (arg.Type.IsInt)
                        return model.MkIntElement(0);
                    else
                        return null;
                }
            }
            else
            {
                Debug.Assert(false);
                return null;
            }
        }

        private void attachEnsures(Implementation impl)
        {
            List<Variable> functionInterfaceVars = new List<Variable>();
            foreach (Variable v in vcgen.program.GlobalVariables())
            {
                functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
            }
            foreach (Variable v in impl.InParams)
            {
                functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
            }
            foreach (Variable v in impl.OutParams)
            {
                functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
            }
            foreach (IdentifierExpr e in impl.Proc.Modifies)
            {
                if (e.Decl == null) continue;
                functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
            }
            Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
            var function = new Function(Token.NoToken, impl.Name + summaryPredSuffix, functionInterfaceVars, returnVar);
            prover.Context.DeclareFunction(function, "");

            List<Expr> exprs = new List<Expr>();
            foreach (Variable v in vcgen.program.GlobalVariables())
            {
                Contract.Assert(v != null);
                exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
            }
            foreach (Variable v in impl.Proc.InParams)
            {
                Contract.Assert(v != null);
                exprs.Add(new IdentifierExpr(Token.NoToken, v));
            }
            foreach (Variable v in impl.Proc.OutParams)
            {
                Contract.Assert(v != null);
                exprs.Add(new IdentifierExpr(Token.NoToken, v));
            }
            foreach (IdentifierExpr ie in impl.Proc.Modifies)
            {
                Contract.Assert(ie != null);
                if (ie.Decl == null)
                    continue;
                exprs.Add(ie);
            }
            Expr postExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
            impl.Proc.Ensures.Add(
                new Ensures(Token.NoToken, false, postExpr, "", 
                    new QKeyValue(Token.NoToken, "ah", new List<object>(), null)));
        }

        private void GenVC(Implementation impl)
        {
            ModelViewInfo mvInfo;
            Dictionary<int, Absy> label2absy;

            if (CommandLineOptions.Clo.Trace)
            {
                Console.WriteLine("Generating VC of {0}", impl.Name);
            }

            vcgen.ConvertCFG2DAG(impl);
            vcgen.PassifyImpl(impl, out mvInfo);

            var gen = prover.VCExprGen;
            var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context);


            // Find the assert
            impl2EndStateVars.Add(impl.Name, new List<VCExpr>());
            var found = false;
            var assertId = -1;
            foreach (var blk in impl.Blocks)
            {
                foreach (var cmd in blk.Cmds.OfType<AssertCmd>())
                {
                    if (SimpleUtil.isAssertTrue(cmd)) continue;
                    var nary = cmd.Expr as NAryExpr;
                    if (nary == null) continue;
                    var pred = nary.Fun as FunctionCall;
                    if (pred == null || pred.FunctionName != (impl.Name + (AbstractHoudini.summaryPredSuffix)))
                        continue;

                    Debug.Assert(!found);
                    found = true;
                    assertId = cmd.UniqueId;
                    //Console.WriteLine("assert cmd id: {0}", cmd.UniqueId);
                    nary.Args.OfType<Expr>()
                        .Iter(expr => impl2EndStateVars[impl.Name].Add(prover.Context.BoogieExprTranslator.Translate(expr)));
                }
            }

            // It is possible that no assert is found in the procedure. It happens when the
            // procedure doesn't return.
            //Debug.Assert(found);

            // Grab summary predicates
            var visitor = new FindSummaryPred(prover.VCExprGen, assertId);
            vcexpr = visitor.Mutate(vcexpr, true);

            // Create a macro so that the VC can sit with the theorem prover
            Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
            prover.DefineMacro(macro, vcexpr);

            // Store VC
            impl2VC.Add(impl.Name, gen.Function(macro));

            //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);

            // check sanity: only one predicate for self-summary
            // (There may be none when the procedure doesn't return)
            Debug.Assert(visitor.summaryPreds.Count(tup => tup.Item2) <= 1);

            impl2CalleeSummaries.Add(impl.Name, new List<Tuple<string, bool, VCExprVar, VCExprNAry>>());
            visitor.summaryPreds.Iter(tup => impl2CalleeSummaries[impl.Name].Add(tup));
        }
    }

    public interface ISummaryElement
    {
        ISummaryElement Copy();
        ISummaryElement GetFlaseSummary(Program program, Implementation impl);
        void Join(Dictionary<string, Model.Element> state, Model model);
        VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen);
        Expr GetSummaryExpr(Func<string, Expr> always, Func<string, Expr> forold);

        // For Bilateral
        ISummaryElement GetTrueSummary(Program program, Implementation impl);
        void Meet(ISummaryElement other);
        bool IsEqual(ISummaryElement other);
        ISummaryElement AbstractConsequence(ISummaryElement upper);
    }

    public class ConstantVal : ISummaryElement
    {
        Program program;
        Implementation impl;
        // var -> const set
        Dictionary<string, HashSet<int>> val;
        // set of vars
        HashSet<Variable> vars;

        public static readonly int MAX = 3;

        public ConstantVal()
        {
            // this is just a place holder
            val = new Dictionary<string, HashSet<int>>();
            vars = new HashSet<Variable>();
        }

        private ConstantVal(Program program, Implementation impl)
        {
            this.program = program;
            this.impl = impl;
            this.val = new Dictionary<string, HashSet<int>>();

            vars = new HashSet<Variable>();
            impl.Proc.Modifies
                .OfType<IdentifierExpr>()
                .Select(ie => ie.Decl)
                .Where(v => v.TypedIdent.Type.IsInt)
                .Iter(v => vars.Add(v));
            impl.OutParams.OfType<Variable>()
                .Where(v => v.TypedIdent.Type.IsInt)
                .Iter(v => vars.Add(v));

            vars.Iter(v => val.Add(v.Name, null));
        }


        public void Join(Dictionary<string, Model.Element> state, Model model)
        {
            foreach (var vv in vars)
            {
                var v = vv.Name;
                var newv = state[v].AsInt();
                var oldv = val[v];

                if (oldv == null)
                {
                    val[v] = new HashSet<int>();
                    val[v].Add(newv);
                }
                else if(oldv.Count > 0)
                {
                    val[v].Add(newv);
                    if (val[v].Count > MAX)
                        val[v] = new HashSet<int>();
                } 

            }
        }

        public VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen)
        {
            VCExpr ret = VCExpressionGenerator.True;
            if (val.Values.Any(v => v == null))
                return VCExpressionGenerator.False;
            
            foreach (var v in vars)
            {
                var consts = val[v.Name];
                Debug.Assert(consts != null);

                if (consts.Count == 0)
                    continue;

                var vexpr = VCExpressionGenerator.False;
                consts.Iter(c => vexpr = gen.OrSimp(vexpr, gen.Eq(incarnations[v.Name], gen.Integer(Microsoft.Basetypes.BigNum.FromInt(c)))));
                ret = gen.AndSimp(ret, vexpr);
            }

            return ret;
        }

        public override string ToString()
        {
            var ret = "true";
            if (val.Values.Any(v => v == null))
                return "false";

            foreach (var v in vars)
            {
                var consts = val[v.Name];
                Debug.Assert(consts != null);

                if (consts.Count == 0)
                    continue;

                var vexpr = "false";
                consts.Iter(c => vexpr = 
                    string.Format("{0} OR ({1} == {2})", vexpr, v.Name, c));

                ret = string.Format("{0} AND ({1})", ret, vexpr);
            }

            return ret;
        }


        public ISummaryElement GetFlaseSummary(Program program, Implementation impl)
        {
            return new ConstantVal(program, impl);
        }

        #region ISummaryElement (Bilateral) Members


        public ISummaryElement GetTrueSummary(Program program, Implementation impl)
        {
            throw new NotImplementedException();
        }

        public void Meet(ISummaryElement other)
        {
            throw new NotImplementedException();
        }

        public bool IsEqual(ISummaryElement other)
        {
            throw new NotImplementedException();
        }

        public ISummaryElement AbstractConsequence(ISummaryElement upper)
        {
            throw new NotImplementedException();
        }

        #endregion

        #region ISummaryElement Members


        public Expr GetSummaryExpr(Func<string, Expr> always, Func<string, Expr> forold)
        {
            throw new NotImplementedException();
        }

        #endregion

        #region ISummaryElement Members

        public ISummaryElement Copy()
        {
            throw new NotImplementedException();
        }

        #endregion
    }

    public class NamedExpr 
    {
        public string name;
        public Expr expr;

        public NamedExpr(string name, Expr expr)
        {
            this.name = name;
            this.expr = expr;
        }

        public NamedExpr(Expr expr)
        {
            this.name = null;
            this.expr = expr;
        }

        public override string ToString()
        {
            if (name != null)
                return name;

            return expr.ToString();
        }
    }

    public class PredicateAbs : ISummaryElement
    {
        public static Dictionary<string, List<NamedExpr>> PrePreds { get; private set; }
        public static Dictionary<string, HashSet<int>> PosPrePreds { get; private set; }
        public static Dictionary<string, List<NamedExpr>> PostPreds { get; private set; }
        public static Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>> UpperCandidates;
        private static HashSet<string> boolConstants;
        // {proc, pred-pair} -> polariry
        public static HashSet<Tuple<string, int, int, bool, bool>> unsatPrePredPairs;
        public static HashSet<Tuple<string, int, int, bool, bool>> unsatPostPredPairs;

        // Temporary: used during eval
        private static Model model = null;

        string procName;
        PredicateAbsDisjunct[] value;
        bool isFalse;

        public PredicateAbs(string procName)
        {
            this.procName = procName;
            isFalse = true;
            value = new PredicateAbsDisjunct[PostPreds[this.procName].Count];
            for (int i = 0; i < PostPreds[this.procName].Count; i++) value[i] = null;
        }

        public static void Initialize(Program program)
        {
            PrePreds = new Dictionary<string, List<NamedExpr>>();
            PostPreds = new Dictionary<string, List<NamedExpr>>();
            PosPrePreds = new Dictionary<string, HashSet<int>>();

            boolConstants = new HashSet<string>();
            UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>();

            program.TopLevelDeclarations.OfType<Constant>()
                .Where(c => c.TypedIdent.Type.IsBool)
                .Iter(c => boolConstants.Add(c.Name));

            // Add template pre-post to all procedures
            var preT = new List<NamedExpr>();
            var postT = new List<NamedExpr>();
            var posPreT = new HashSet<int>();
            var tempP = new HashSet<Procedure>();
            foreach (var proc in
                program.TopLevelDeclarations.OfType<Procedure>()
                .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template")))
            {
                tempP.Add(proc);
                foreach (var ens in proc.Ensures.OfType<Ensures>())
                {
                    var pos = QKeyValue.FindBoolAttribute(ens.Attributes, "positive");

                    if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre"))
                    {
                        preT.Add(new NamedExpr(null, ens.Condition));
                        if (pos) posPreT.Add(preT.Count - 1);
                    }

                    if (QKeyValue.FindBoolAttribute(ens.Attributes, "post"))
                        postT.Add(new NamedExpr(null, ens.Condition));

                    var s = QKeyValue.FindStringAttribute(ens.Attributes, "pre");
                    if (s != null)
                    {
                        preT.Add(new NamedExpr(s, ens.Condition));
                        if (pos) posPreT.Add(preT.Count - 1);
                    }

                    s = QKeyValue.FindStringAttribute(ens.Attributes, "post");
                    if (s != null)
                        postT.Add(new NamedExpr(s, ens.Condition));
                }
            }

            program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl));
            var upperPreds = new Dictionary<string, List<Expr>>();

            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
            {
                PrePreds.Add(impl.Name, new List<NamedExpr>());
                PostPreds.Add(impl.Name, new List<NamedExpr>());
                PosPrePreds.Add(impl.Name, new HashSet<int>());

                // Add "false" as the first post predicate
                //PostPreds[impl.Name].Add(new NamedExpr(Expr.False));

                preT.Iter(e => PrePreds[impl.Name].Add(e));
                postT.Iter(e => PostPreds[impl.Name].Add(e));
                PosPrePreds[impl.Name].UnionWith(posPreT);

                // Pick up per-procedure pre-post
                var nens = new List<Ensures>();
                foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())
                {
                    string s = null;
                    var pos = QKeyValue.FindBoolAttribute(ens.Attributes, "positive");
                    
                    if (QKeyValue.FindBoolAttribute(ens.Attributes, "pre"))
                    {
                        PrePreds[impl.Name].Add(new NamedExpr(ens.Condition));
                        PosPrePreds[impl.Name].Add(PrePreds[impl.Name].Count - 1);
                    }
                    else if (QKeyValue.FindBoolAttribute(ens.Attributes, "post"))
                    {
                        PostPreds[impl.Name].Add(new NamedExpr(ens.Condition));
                    }
                    else if ((s = QKeyValue.FindStringAttribute(ens.Attributes, "pre")) != null)
                    {
                        PrePreds[impl.Name].Add(new NamedExpr(s, ens.Condition));
                        PosPrePreds[impl.Name].Add(PrePreds[impl.Name].Count - 1);
                    }
                    else if ((s = QKeyValue.FindStringAttribute(ens.Attributes, "post")) != null)
                    {
                        PostPreds[impl.Name].Add(new NamedExpr(s, ens.Condition));
                    }
                    else if (QKeyValue.FindBoolAttribute(ens.Attributes, "upper"))
                    {
                        var key = impl.Name;
                        if (!upperPreds.ContainsKey(key))
                            upperPreds.Add(key, new List<Expr>());
                        upperPreds[key].Add(ens.Condition);
                    }
                    else
                    {
                        nens.Add(ens);
                    }
                }
                impl.Proc.Ensures = nens;
            }

            foreach (var tup in upperPreds)
            {
                var procName = tup.Key;
                var candidates = tup.Value;
                if (!candidates.Any()) continue;

                var strToPost = new Dictionary<string, int>();
                for (int i = 0; i < PostPreds[procName].Count; i++)
                {
                    strToPost.Add(PostPreds[procName][i].expr.ToString(), i);
                }

                foreach (var expr in candidates)
                {
                    if (strToPost.ContainsKey(expr.ToString()))
                    {
                        var key = Tuple.Create(procName, strToPost[expr.ToString()]);
                        if (!UpperCandidates.ContainsKey(key))
                            UpperCandidates.Add(key, new List<PredicateAbsDisjunct>());
                        UpperCandidates[key].Add(new PredicateAbsDisjunct(true, procName));
                    }
                    else
                    {
                        // Try parsing the expression as (pre-conjunct ==> post-pred)
                        var parsed = ParseExpr(expr, procName);
                        if (parsed != null && strToPost.ContainsKey(parsed.Item2.ToString()))
                        {
                            var key = Tuple.Create(procName, strToPost[parsed.Item2.ToString()]);
                            if (!UpperCandidates.ContainsKey(key))
                                UpperCandidates.Add(key, new List<PredicateAbsDisjunct>());
                            UpperCandidates[key].Add(parsed.Item1);
                        }
                    }
                }

            }
            //Console.WriteLine("Running Abstract Houdini");
            //PostPreds.Iter(expr => Console.WriteLine("\tPost: {0}", expr));
            //PrePreds.Iter(expr => Console.WriteLine("\tPre: {0}", expr));
        }

        // Try parsing the expression as (pre-conjunct ==> post-pred)
        private static Tuple<PredicateAbsDisjunct, Expr> ParseExpr(Expr expr, string procName)
        {
            Expr postExpr = null;
            Expr preExpr = null;

            // Decompose outer Implies
            var nexpr = expr as NAryExpr;
            if (nexpr != null && (nexpr.Fun is BinaryOperator)
                && (nexpr.Fun as BinaryOperator).Op == BinaryOperator.Opcode.Imp
                && (nexpr.Args.Count == 2))
            {
                postExpr = nexpr.Args[1];
                preExpr = nexpr.Args[0];
            }
            else
            {
                if(CommandLineOptions.Clo.Trace) Console.WriteLine("Failed to parse {0} (ignoring)", expr);
                return null;
            }


            var atoms = DecomposeOuterAnd(preExpr);
            var pos = new HashSet<int>();
            var neg = new HashSet<int>();

            foreach (var atom in atoms)
            {
                var index = PrePreds[procName].FindIndex(ne => ne.expr.ToString() == atom.ToString());
                if (index == -1)
                {
                    index = PrePreds[procName].FindIndex(ne => Expr.Not(ne.expr).ToString() == atom.ToString());
                    if (index == -1)
                    {
                        if(CommandLineOptions.Clo.Trace) Console.WriteLine("Failed to parse {0} (ignoring)", atom);
                        return null;
                    }
                    else
                    {
                        neg.Add(index);
                    }
                }
                else
                {
                    pos.Add(index);
                }
            }

            var conj = new PredicateAbsConjunct(pos, neg, procName);
            var conjls = new List<PredicateAbsConjunct>();
            conjls.Add(conj);

            return Tuple.Create(new PredicateAbsDisjunct(conjls, procName), postExpr);
        }

        // blah && blah ==> {blah, blah}
        static IEnumerable<Expr> DecomposeOuterAnd(Expr expr)
        {
            var ret = new List<Expr>();

            var nexpr = expr as NAryExpr;
            if (nexpr == null
                || !(nexpr.Fun is BinaryOperator)
                || (nexpr.Fun as BinaryOperator).Op != BinaryOperator.Opcode.And)
            {
                    ret.Add(expr);
            }
            else
            {
                foreach (Expr a in nexpr.Args)
                    ret.AddRange(DecomposeOuterAnd(a));
            }

            return ret;
        }


        private Model.Element Eval(Expr expr, Dictionary<string, Model.Element> state)
        {
            if (expr is LiteralExpr)
            {
                return ToElem((expr as LiteralExpr).Val);
            }

            if (expr is IdentifierExpr)
            {
                return LookupVariable((expr as IdentifierExpr).Name, state, false);
            }

            if (expr is OldExpr)
            {
                var ide = (expr as OldExpr).Expr as IdentifierExpr;
                Debug.Assert(ide != null);

                return LookupVariable(ide.Name, state, true);
            }

            if (expr is NAryExpr)
            {
                var nary = expr as NAryExpr;
                if (nary.Fun is UnaryOperator)
                {
                    return ToElem((nary.Fun as UnaryOperator).Evaluate(ToValue(Eval(nary.Args[0], state))));
                }
                if (nary.Fun is BinaryOperator)
                {
                    return ToElem((nary.Fun as BinaryOperator).Evaluate(ToValue(Eval(nary.Args[0], state)), ToValue(Eval(nary.Args[1], state))));
                }
                if (nary.Fun is MapSelect && nary.Args.Count == 2)
                {
                    var index = Eval(nary.Args[1], state);
                    var map = Eval(nary.Args[0], state) as Model.Array;
                    Debug.Assert(map != null, "Variable of map type must have an Array-typed value");
                    var ret = map.Value.TryEval(index as Model.Element);
                    if (ret == null) ret = map.Value.Else;
                    Debug.Assert(ret != null);
                    return ret;
                }
                Debug.Assert(false, "No other op is handled");                
            }
            throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString()));
        }

        private Model.Element LookupVariable(string v, Dictionary<string, Model.Element> state, bool tryOld)
        {
            if (tryOld)
            {
                var oldv = string.Format("old({0})", v);
                if (state.ContainsKey(oldv))
                {
                    return state[oldv];
                }
                throw new AbsHoudiniInternalError("Cannot handle this case");
            }

            if (state.ContainsKey(v))
            {
                return state[v];
            }

            /*
            if (boolConstants.Contains(v))
            {
                // value of this constant is immaterial, return true
                return model.MkElement("true");
            }
            */

            throw new AbsHoudiniInternalError("Cannot handle this case");
        }

        private static VCExpr ToVcVar(string v, Dictionary<string, VCExpr> incarnations, bool tryOld)
        {
            if (tryOld)
            {
                var oldv = string.Format("old({0})", v);
                if (incarnations.ContainsKey(oldv))
                {
                    return incarnations[oldv];
                }
                throw new AbsHoudiniInternalError("Cannot handle this case");
            }

            if (incarnations.ContainsKey(v))
            {
                return incarnations[v];
            }

            throw new AbsHoudiniInternalError("Cannot handle this case");
        }

        public static void FindUnsatPairs(VCExpressionGenerator gen, ProverInterface prover)
        {
            unsatPrePredPairs = new HashSet<Tuple<string, int, int, bool, bool>>();
            unsatPostPredPairs = new HashSet<Tuple<string, int, int, bool, bool>>(); 

            var cachePos = new HashSet<Tuple<string, string>>();
            var cacheNeg = new HashSet<Tuple<string, string>>();
            var record = new Action<object, string, int, int, bool, bool>(
                (map, proc, e1, e2, p1, p2) => {
                    var key = Tuple.Create(proc, e1, e2, p1, p2);
                    if (map == PrePreds)
                        unsatPrePredPairs.Add(key);
                    else
                        unsatPostPredPairs.Add(key);
                }
            );

            var predMaps = new List<Dictionary<string, List<NamedExpr>>>();
            predMaps.Add(PrePreds); predMaps.Add(PostPreds);

            foreach (var map in predMaps)
            {
                foreach (var proc in map.Keys)
                {
                    for (int i = 0; i < 2 * map[proc].Count(); i++)
                    {
                        var p1 = (i % 2); // polarity
                        var e1 = map[proc][i / 2].expr;
                        if (p1 == 0) e1 = Expr.Not(e1);

                        for (int j = 2 * ((i / 2) + 1); j < 2 * map[proc].Count(); j++)
                        {
                            var p2 = (j % 2); // polarity
                            var e2 = map[proc][j / 2].expr;
                            if (p2 == 0) e2 = Expr.Not(e2);

                            var key = Tuple.Create(e1.ToString(), e2.ToString());
                            if (cachePos.Contains(key))
                            {
                                record(map, proc, i / 2, j / 2, p1 == 1, p2 == 1);
                                continue;
                            }
                            else if (cacheNeg.Contains(key))
                            {
                                continue;
                            }

                            if (!CheckIfUnsat(e1, e2, gen, prover))
                            {
                                cacheNeg.Add(key);
                                continue;
                            }
                            cachePos.Add(key);
                            record(map, proc, i / 2, j / 2, p1 == 1, p2 == 1);

                            if (CommandLineOptions.Clo.Trace)
                                Console.WriteLine("Proved UNSAT: {0}    {1}", e1, e2);
                        }
                    }
                }
            }
        }

        // Is a ^ b UNSAT?
        private static bool CheckIfUnsat(Expr a, Expr b, VCExpressionGenerator gen, ProverInterface prover)
        {
            var gatherLitA = new GatherLiterals();
            var gatherLitB = new GatherLiterals();

            gatherLitA.Visit(a);
            gatherLitB.Visit(b);

            var seta = new HashSet<Variable>();
            var setb = new HashSet<Variable>();
            gatherLitA.literals.Iter(tup => seta.Add(tup.Item1));
            gatherLitB.literals.Iter(tup => setb.Add(tup.Item1));
            seta.IntersectWith(setb);
            if (!seta.Any()) return false;
            
            // Create fresh variables
            return CheckIfUnsat(Expr.And(a, b), gen, prover);
        }

        // Is a UNSAT?
        private static bool CheckIfUnsat(Expr a, VCExpressionGenerator gen, ProverInterface prover)
        {
            var gatherLitA = new GatherLiterals();
            gatherLitA.Visit(a);

            // Create fresh variables
            var counter = 0;
            var incarnations = new Dictionary<string, VCExpr>();
            foreach (var literal in gatherLitA.literals)
            {
                if (incarnations.ContainsKey(literal.Item2.ToString()))
                    continue;

                //if(!literal.Item1.TypedIdent.Type.IsInt && !literal.Item1.TypedIdent.Type.IsBool)
                var v = gen.Variable("UNSATCheck" + counter, literal.Item1.TypedIdent.Type);
                incarnations.Add(literal.Item2.ToString(), v);
                counter++;
            }

            var vc1 = ToVcExpr(a, incarnations, gen);
            var vc = gen.LabelPos("Temp", vc1);

            // check
            prover.AssertAxioms();
            prover.Push();
            prover.Assert(vc, true);
            prover.Check();
            var outcome = prover.CheckOutcomeCore(new AbstractHoudiniErrorReporter());
            prover.Pop();

            if (outcome == ProverInterface.Outcome.Valid)
                return true;
            return false;
        }


        class GatherLiterals : ReadOnlyVisitor
        {
            public List<Tuple<Variable, Expr>> literals;
            bool inOld;

            public GatherLiterals()
            {
                literals = new List<Tuple<Variable, Expr>>();
                inOld = false;
            }

            public override Expr VisitOldExpr(OldExpr node)
            {
                var prev = inOld;
                inOld = true;
                var ret = base.VisitOldExpr(node);
                inOld = prev;
                return ret;
            }

            public override Expr VisitIdentifierExpr(IdentifierExpr node)
            {
                if (inOld)
                    literals.Add(Tuple.Create(node.Decl, new OldExpr(Token.NoToken, node) as Expr));
                else
                    literals.Add(Tuple.Create(node.Decl, node as Expr));

                return node;
            }
        }

        private object ToValue(Model.Element elem)
        {
            if (elem is Model.Integer)
            {
                return Microsoft.Basetypes.BigNum.FromInt((elem as Model.Integer).AsInt());
            }
            if (elem is Model.Boolean)
            {
                return (elem as Model.Boolean).Value;
            }
            if (elem is Model.DatatypeValue && (elem as Model.DatatypeValue).Arguments.Length == 1 &&
                (elem as Model.DatatypeValue).ConstructorName == "-" &&
                (elem as Model.DatatypeValue).Arguments[0] is Model.Integer)
            {
                // negative number as "-" @ int
                return Microsoft.Basetypes.BigNum.FromInt(-1 * ((elem as Model.DatatypeValue).Arguments[0] as Model.Integer).AsInt());
            }
            throw new NotImplementedException("Cannot yet handle this Model.Element type");
        }

        private Model.Element ToElem(object val)
        {
            if (val is bool || val is int || val is Basetypes.BigNum)
                return model.MkElement(val.ToString());
            throw new NotImplementedException("Cannot yet handle this value type");
        }

        // replace v by old(v)
        private static Expr MakeOld(Expr expr)
        {
            var substalways = new Substitution(v => new OldExpr(Token.NoToken, Expr.Ident(v)));
            var substold = new Substitution(v => Expr.Ident(v));

            return Substituter.ApplyReplacingOldExprs(substalways, substold, expr);
        }

        private static Expr ToExpr(Expr expr, Func<string, Expr> always, Func<string, Expr> forold)
        {
            var substalways = new Substitution(v =>
            {
                var ret = always(v.Name);
                if (ret != null) return ret;
                else return Expr.Ident(v);
            });
            var substold = new Substitution(v =>
            {
                var ret = forold(v.Name);
                if (ret != null) return ret;
                else return new OldExpr(Token.NoToken, Expr.Ident(v));
            });

            return Substituter.ApplyReplacingOldExprs(substalways, substold, expr);
        }

        private static VCExpr ToVcExpr(Expr expr, Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen)
        {
            if (expr is LiteralExpr)
            {
                var val = (expr as LiteralExpr).Val;
                if (val is bool)
                {
                    if ((bool)val)
                    {
                        return VCExpressionGenerator.True;
                    }
                    else
                    {
                        return VCExpressionGenerator.False;
                    }
                }
                else if (val is Microsoft.Basetypes.BigNum)
                {
                    return gen.Integer((Microsoft.Basetypes.BigNum)val);
                }

                throw new NotImplementedException("Cannot handle literals of this type");
            }

            if (expr is IdentifierExpr)
            {
                return ToVcVar((expr as IdentifierExpr).Name, incarnations, false);
            }

            if (expr is OldExpr)
            {
                var ide = (expr as OldExpr).Expr as IdentifierExpr;
                Debug.Assert(ide != null);

                return ToVcVar(ide.Name, incarnations, true);
            }

            if (expr is NAryExpr)
            {
                var nary = expr as NAryExpr;
                if (nary.Fun is UnaryOperator)
                {
                    if ((nary.Fun as UnaryOperator).Op == UnaryOperator.Opcode.Not)
                        return gen.Not(ToVcExpr(nary.Args[0], incarnations, gen));
                    else if ((nary.Fun as UnaryOperator).Op == UnaryOperator.Opcode.Neg)
                        return gen.Function(VCExpressionGenerator.SubIOp, gen.Integer(Basetypes.BigNum.FromInt(0)), ToVcExpr(nary.Args[0], incarnations, gen));
                    else
                        Debug.Assert(false, "No other unary op is handled");
                }
                if (nary.Fun is BinaryOperator)
                {
                    return gen.Function(Translate(nary.Fun as BinaryOperator), ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen));
                }
                if (nary.Fun is MapSelect && nary.Args.Count == 2)
                {
                    return gen.Select(ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen));
                }
                Debug.Assert(false, "No other op is handled");
            }
            throw new NotImplementedException(string.Format("Expr of type {0} is not handled", expr.GetType().ToString()));
        }

        private static VCExprOp Translate(BinaryOperator op)
        {
            switch (op.Op)
            {
                case BinaryOperator.Opcode.Add:
                    return VCExpressionGenerator.AddIOp;
                case BinaryOperator.Opcode.Sub:
                    return VCExpressionGenerator.SubIOp;
                case BinaryOperator.Opcode.Mul:
                    return VCExpressionGenerator.MulIOp;
                case BinaryOperator.Opcode.Div:
                    return VCExpressionGenerator.DivIOp;
                case BinaryOperator.Opcode.Mod:
                    return VCExpressionGenerator.ModOp;
                case BinaryOperator.Opcode.Eq:
                case BinaryOperator.Opcode.Iff:
                    // we don't distinguish between equality and equivalence at this point
                    return VCExpressionGenerator.EqOp;
                case BinaryOperator.Opcode.Neq:
                    return VCExpressionGenerator.NeqOp;
                case BinaryOperator.Opcode.Lt:
                    return VCExpressionGenerator.LtOp;
                case BinaryOperator.Opcode.Le:
                    return VCExpressionGenerator.LeOp;
                case BinaryOperator.Opcode.Ge:
                    return VCExpressionGenerator.GeOp;
                case BinaryOperator.Opcode.Gt:
                    return VCExpressionGenerator.GtOp;
                case BinaryOperator.Opcode.Imp:
                    return VCExpressionGenerator.ImpliesOp;
                case BinaryOperator.Opcode.And:
                    return VCExpressionGenerator.AndOp;
                case BinaryOperator.Opcode.Or:
                    return VCExpressionGenerator.OrOp;
                case BinaryOperator.Opcode.Subtype:
                    return VCExpressionGenerator.SubtypeOp;
                default:
                    Contract.Assert(false);
                    throw new NotImplementedException();
            }

        }

        // If "false" is a post-predicate, then remove its "pre" constraint from all others, whenever possible
        public void Simplify()
        {
            // find "false"
            var findex = PostPreds[procName].FindIndex(ne => (ne.expr is LiteralExpr) && (ne.expr as LiteralExpr).IsFalse);
            if (findex < 0) return;
            if (value[findex].isTrue)
            {
                // procedure doesn't return
                for (int i = 0; i < value.Length; i++)
                    if (i != findex) value[i] = new PredicateAbsDisjunct(false, procName);
                return;
            }
            if (value[findex].isFalse)
                return;

            for (int i = 0; i < value.Length; i++)
                if (i != findex) value[i].Subtract(value[findex]);
        }

        public HashSet<string> GetPredicates(Program program, VCExpressionGenerator gen, ProverInterface prover)
        {
            var ret = new HashSet<string>();
            if (isFalse) return ret;
            Simplify();

            // Find the free expressions
            var proc = program.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == procName);
            Contract.Assert(proc != null);
            Expr freeSummary = Expr.True;
            foreach (var req in proc.Requires.OfType<Requires>().Where(req => req.Free))
            {
                freeSummary = Expr.And(freeSummary, MakeOld(req.Condition));
            }
            foreach (var ens in proc.Ensures.OfType<Ensures>().Where(ens => ens.Free))
            {
                freeSummary = Expr.And(freeSummary, ens.Condition);
            }
            
            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                if (value[i].isFalse) continue;
                if (PostPreds[procName][i].expr is LiteralExpr && (PostPreds[procName][i].expr as LiteralExpr).IsFalse)
                    continue;

                if (value[i].isTrue)
                    ret.Add(PostPreds[procName][i].expr.ToString());
                else
                {
                    foreach (var c in value[i].GetConjuncts())
                    {
                        var s = Expr.Imp(c.ToExpr(j => PrePreds[procName][j].expr), PostPreds[procName][i].expr);
                        if (CheckIfUnsat(Expr.And(freeSummary, Expr.Not(s)), gen, prover))
                            continue;
                        ret.Add(s.ToString());
                    }
                }
            }
            return ret;
        }

        public override string ToString()
        {
            var ret = "";
            if (isFalse) return "false";
            var first = true;

            for(int i = 0; i < PostPreds[procName].Count; i++) 
            {
                if(value[i].isFalse) continue;
                
                if(value[i].isTrue)
                    ret += string.Format("{0}{1}", first ? "" : " && ", PostPreds[procName][i]);
                else
                    ret += string.Format("{0}({1} ==> {2})", first ? "" : " && ", value[i], PostPreds[procName][i]);

                first = false;
            }
            if (ret == "") ret = "true";
            return ret;
        }


        #region ISummaryElement Members

        public ISummaryElement Copy()
        {
            var ret = new PredicateAbs(procName);
            ret.isFalse = isFalse;
            ret.value = new PredicateAbsDisjunct[value.Length];
            for (int i = 0; i < value.Length; i++)
                ret.value[i] = value[i];
            return ret;
        }

        public ISummaryElement GetFlaseSummary(Program program, Implementation impl)
        {
            return new PredicateAbs(impl.Name);
        }

        public ISummaryElement GetTrueSummary(Program program, Implementation impl)
        {
            var ret = new PredicateAbs(impl.Name);
            ret.isFalse = false;
            for (int i = 0; i < PostPreds[this.procName].Count; i++) ret.value[i] = new PredicateAbsDisjunct(false, impl.Name);

            return ret;
        }

        public void Join(Dictionary<string, Model.Element> state, Model model)
        {
            PredicateAbs.model = model;

            // Evaluate each predicate on the state
            var prePredsVal = new bool[PrePreds[procName].Count];
            var postPredsVal = new bool[PostPreds[procName].Count];

            var indexSeq = new List<int>();
            for (int i = 0; i < PrePreds[procName].Count; i++) indexSeq.Add(i);

            for (int i = 0; i < PrePreds[procName].Count; i++)
            {
                var v = ToValue(Eval(PrePreds[procName][i].expr, state));
                Debug.Assert(v is bool);
                prePredsVal[i] = (bool)v;
            }

            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                var v = ToValue(Eval(PostPreds[procName][i].expr, state));
                Debug.Assert(v is bool);
                postPredsVal[i] = (bool)v;
            }

            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                // No hope for this post pred?
                if (!isFalse && value[i].isFalse) continue;

                var newDisj = new PredicateAbsDisjunct(true, procName);
                if (!postPredsVal[i])
                {
                    newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j] && !PosPrePreds[procName].Contains(j)), procName);
                }

                if (isFalse)
                    value[i] = newDisj;
                else
                    value[i] = PredicateAbsDisjunct.And(value[i], newDisj);
            }

            /*
            // do beta(model)
            var that = new PredicateAbsDisjunct[PostPreds[procName].Count];
            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                if (postPredsVal[i])
                    that[i] = new PredicateAbsDisjunct(true, procName);
                else if (i == 0)
                {
                    Debug.Assert(PostPreds[procName][0].ToString() == "false");
                    var newDisj = new PredicateAbsDisjunct(true, procName);
                    newDisj = new PredicateAbsDisjunct(indexSeq.Where(j => !prePredsVal[j]), indexSeq.Where(j => prePredsVal[j]), procName);
                    that[i] = newDisj;
                }
                else
                {
                    // false
                    that[i] = new PredicateAbsDisjunct(false, procName);
                }
            }

            // Do join
            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                if (isFalse)
                    value[i] = that[i];
                else
                {
                    if (i == 0)
                        value[i] = PredicateAbsDisjunct.And(value[i], that[i]);
                    else
                    {
                        var c1 = PredicateAbsDisjunct.And(value[i], that[i]);
                        var c2 = PredicateAbsDisjunct.And(value[i], that[0]);
                        var c3 = PredicateAbsDisjunct.And(value[0], that[i]);
                        value[i] = PredicateAbsDisjunct.Or(c1, c2);
                        value[i] = PredicateAbsDisjunct.Or(value[i], c3);
                    }
                }
            }
            */
            isFalse = false;

            //Console.WriteLine("Result of Join: {0}", this.ToString());
        }

        // Precondition: the upper guys are just {true/false/upper-candidate} ==> post-pred
        public void Meet(ISummaryElement iother)
        {
            var other = iother as PredicateAbs;
            if (isFalse) return;
            if (other.isFalse)
            {
                isFalse = true;
                for (int i = 0; i < PostPreds[this.procName].Count; i++) value[i] = null;
                return;
            }
            Debug.Assert(this.procName == other.procName);

            for (int i = 0; i < PostPreds[this.procName].Count; i++)
            {
                value[i] = PredicateAbsDisjunct.Or(value[i], other.value[i]);
            }
        }

        public bool IsEqual(ISummaryElement other)
        {
            var that = other as PredicateAbs;
            if (isFalse && that.isFalse) return true;
            if (isFalse || that.isFalse) return false;
            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                if (!PredicateAbsDisjunct.syntacticLessThan(value[i], that.value[i]) ||
                    !PredicateAbsDisjunct.syntacticLessThan(that.value[i], value[i]))
                    return false;
            }
            return true;
        }

        // Precondition: the upper guys are just {true/false/upper-candidate} ==> post-pred
        // Postcondition: the returned value is also of this form (for just one post-pred)
        public ISummaryElement AbstractConsequence(ISummaryElement iupper)
        {
            var upper = iupper as PredicateAbs;

            for (int i = 0; i < PostPreds[this.procName].Count; i++)
            {
                if (upper.value[i].isTrue) continue;
                if (!UpperCandidates.ContainsKey(Tuple.Create(procName, i))) continue;

                foreach (var candidate in UpperCandidates[Tuple.Create(procName, i)])
                {
                    if (PredicateAbsDisjunct.syntacticLessThan(candidate, upper.value[i]))
                        continue;
                    if (!this.isFalse && !PredicateAbsDisjunct.syntacticLessThan(candidate, this.value[i]))
                        continue;

                    var ret = new PredicateAbs(this.procName);
                    ret.isFalse = false;
                    for (int j = 0; j < PostPreds[this.procName].Count; j++)
                        ret.value[j] = new PredicateAbsDisjunct(false, this.procName);

                    ret.value[i] = candidate;

                    return ret;
                }
            }

            // Giveup: the abstract consequence is too difficult to compute
            return null;
        }

        public VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressionGenerator gen)
        {
            if (isFalse)
                return VCExpressionGenerator.False;

            var ret = VCExpressionGenerator.True;

            for(int i = 0; i < PostPreds[procName].Count; i++)
            {
                ret = gen.AndSimp(ret, gen.ImpliesSimp(value[i].ToVcExpr(j => ToVcExpr(PrePreds[procName][j].expr, incarnations, gen), gen), ToVcExpr(PostPreds[procName][i].expr, incarnations, gen)));
            }

            return ret;
        }

        public Expr GetSummaryExpr(Func<string, Expr> always, Func<string, Expr> forold)
        {
            if (isFalse)
                return Expr.False;

            Expr ret = Expr.True;

            for (int i = 0; i < PostPreds[procName].Count; i++)
            {
                ret = Expr.And(ret, Expr.Imp(value[i].ToExpr(j => ToExpr(PrePreds[procName][j].expr, always, forold)), ToExpr(PostPreds[procName][i].expr, always, forold)));
            }

            return ret;
        }

        #endregion
    }

    public class PredicateAbsDisjunct
    {
        List<PredicateAbsConjunct> conjuncts;
        string ProcName;
        public bool isTrue {get; private set;}
        public bool isFalse
        {
            get
            {
                if (isTrue) return false;
                return conjuncts.Count == 0;
            }
        }

        public PredicateAbsDisjunct(bool isTrue, string ProcName)
        {
            this.isTrue = isTrue;
            this.ProcName = ProcName;
            conjuncts = new List<PredicateAbsConjunct>();
        }

        public PredicateAbsDisjunct(List<PredicateAbsConjunct> conjuncts, string ProcName)
        {
            isTrue = false;
            this.conjuncts = conjuncts;
            this.ProcName = ProcName;
        }

        // Disjunct of singleton conjuncts
        public PredicateAbsDisjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName)
        {
            this.ProcName = ProcName;
            conjuncts = new List<PredicateAbsConjunct>();
            isTrue = false;
            pos.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, true, ProcName)));
            neg.Iter(p => conjuncts.Add(PredicateAbsConjunct.Singleton(p, false, ProcName)));
        }

        // Does d1 describe a smaller set of states than d2? This is true when every conjunct of d1
        // is smaller than some conjunct of d2
        public static bool syntacticLessThan(PredicateAbsDisjunct d1, PredicateAbsDisjunct d2)
        {
            if (d2.isTrue) return true;
            if (d1.isTrue) return false;
            if (d1.isFalse) return true;
            if (d2.isFalse) return false;

            foreach (var c1 in d1.conjuncts)
            {
                if (d2.conjuncts.Any(c2 => PredicateAbsConjunct.syntacticLessThan(c1, c2)))
                    continue;
                else
                    return false;
            }
            return true;
        }

        public static PredicateAbsDisjunct And(PredicateAbsDisjunct v1, PredicateAbsDisjunct v2)
        {
            if (v1.isTrue) return v2;
            if (v2.isTrue) return v1;

            var result = new List<PredicateAbsConjunct>();

            foreach (var c1 in v1.conjuncts)
            {
                foreach (var c2 in v2.conjuncts)
                {
                    var c = PredicateAbsConjunct.And(c1, c2);
                    if (c.isFalse) continue;
                    if (result.Any(cprime => c.implies(cprime))) continue;
                    var tmp = new List<PredicateAbsConjunct>();
                    tmp.Add(c);
                    result.Where(cprime => !cprime.implies(c)).Iter(cprime => tmp.Add(cprime));
                    result = tmp;
                }
            }

            return new PredicateAbsDisjunct(result, v1.ProcName);
        }

        public static PredicateAbsDisjunct Or(PredicateAbsDisjunct v1, PredicateAbsDisjunct v2)
        {
            if (v1.isTrue) return v1;
            if (v2.isTrue) return v2;
            if (v1.isFalse) return v2;
            if (v2.isFalse) return v1;

            var result = new List<PredicateAbsConjunct>();
            v1.conjuncts.Iter(c => result.Add(c));

            foreach (var c in v2.conjuncts)
            {
                if (result.Any(cprime => c.implies(cprime))) continue;
                var tmp = new List<PredicateAbsConjunct>();
                tmp.Add(c);
                result.Where(cprime => !cprime.implies(c)).Iter(cprime => tmp.Add(cprime));
                result = tmp;
            }

            return new PredicateAbsDisjunct(result, v1.ProcName);
        }

        public VCExpr ToVcExpr(Func<int, VCExpr> predToExpr, VCExpressionGenerator gen)
        {
            if (isTrue) return VCExpressionGenerator.True;
            var ret = VCExpressionGenerator.False;
            conjuncts.Iter(c => ret = gen.OrSimp(ret, c.ToVcExpr(predToExpr, gen)));
            return ret;
        }

        public Expr ToExpr(Func<int, Expr> predToExpr)
        {
            if (isTrue) return Expr.True;
            Expr ret = Expr.False;
            conjuncts.Iter(c => ret = Expr.Or(ret, c.ToExpr(predToExpr)));
            return ret;
        }

        public override string ToString()
        {
            if(isTrue) 
                return "true";
            var ret = "";
            var first = true;
            foreach (var c in conjuncts)
            {
                if (c.isFalse) continue;
                ret += string.Format("{0}{1}", first ? "" : " || ", c);
                first = false;
            }
            return ret;
        }

        public void Subtract(PredicateAbsDisjunct that)
        {
            var ncon = new List<PredicateAbsConjunct>();
            foreach (var c1 in conjuncts)
            {
                if (that.conjuncts.Any(c2 => c1.implies(c2)))
                    continue;
                ncon.Add(c1);
            }
            conjuncts = ncon;
        }

        public IEnumerable<PredicateAbsConjunct> GetConjuncts()
        {
            return conjuncts;
        }

    }

    public class PredicateAbsConjunct
    {
        static int ConjunctBound = 3;

        public bool isFalse { get; private set; }
        HashSet<int> posPreds;
        HashSet<int> negPreds;
        string ProcName;

        public static void Initialize(int bound)
        {
            ConjunctBound = bound;
        }

        private void Normalize()
        {
            if (posPreds.Intersect(negPreds).Any() || negPreds.Intersect(posPreds).Any() || (posPreds.Count + negPreds.Count > ConjunctBound))
            {
                isFalse = true;
                posPreds = new HashSet<int>();
                negPreds = new HashSet<int>();
            }
        }

        // Do this step only once in a while?
        private void StrongNormalize()
        {
            if (isFalse) return;

            var candidates = new List<Tuple<int, bool>>();
            posPreds.Iter(p => candidates.Add(Tuple.Create(p, true)));
            negPreds.Iter(p => candidates.Add(Tuple.Create(p, false)));
            var drop = new HashSet<int>();
            for (int i = 0; i < candidates.Count; i++)
            {
                for (int j = 0; j < candidates.Count; j++)
                {
                    if (i == j) continue;

                    var key = Tuple.Create(ProcName, candidates[i].Item1, candidates[j].Item1,
                        candidates[i].Item2, candidates[j].Item2);
                    if (PredicateAbs.unsatPrePredPairs.Contains(key))
                    {
                        isFalse = true;
                        posPreds = new HashSet<int>();
                        negPreds = new HashSet<int>();
                        return;
                    }

                    key = Tuple.Create(ProcName, candidates[i].Item1, candidates[j].Item1,
                        candidates[i].Item2, !candidates[j].Item2);

                    if (PredicateAbs.unsatPrePredPairs.Contains(key))
                        drop.Add(candidates[j].Item1);
                }
            }

            posPreds.ExceptWith(drop);
            negPreds.ExceptWith(drop);
        }

        public PredicateAbsConjunct(bool isFalse, string ProcName)
        {
            posPreds = new HashSet<int>();
            negPreds = new HashSet<int>();
            this.isFalse = isFalse;
            this.ProcName = ProcName;
        }

        // do we know that c1 is surely less than or equal to c2? That is, c1 describes a smaller
        // concretization. We check that c2 is a sub-conjunct of c1
        public static bool syntacticLessThan(PredicateAbsConjunct c1, PredicateAbsConjunct c2)
        {
            if (c1.isFalse) return true;
            if (c2.isFalse) return false;
            return (c2.posPreds.IsSubsetOf(c1.posPreds) && c2.negPreds.IsSubsetOf(c1.negPreds));
        }

        public static PredicateAbsConjunct Singleton(int v, bool isPositive, string ProcName)
        {
            if (isPositive)
                return new PredicateAbsConjunct(new int[] { v }, new HashSet<int>(), ProcName);
            else
                return new PredicateAbsConjunct(new HashSet<int>(), new int[] { v }, ProcName);
        }

        public PredicateAbsConjunct(IEnumerable<int> pos, IEnumerable<int> neg, string ProcName)
        {
            isFalse = false;
            posPreds = new HashSet<int>(pos);
            negPreds = new HashSet<int>(neg);
            this.ProcName = ProcName;
            Normalize();
        }

        public static PredicateAbsConjunct And(PredicateAbsConjunct v1, PredicateAbsConjunct v2)
        {
            if (v1.isFalse || v2.isFalse) return new PredicateAbsConjunct(true, v1.ProcName);
            var ret =  new PredicateAbsConjunct(v1.posPreds.Union(v2.posPreds), v1.negPreds.Union(v2.negPreds), v1.ProcName);
            ret.StrongNormalize();
            return ret;
        }

        public bool implies(PredicateAbsConjunct v)
        {
            if (isFalse) return true;
            if (v.isFalse) return false;
            return (posPreds.IsSupersetOf(v.posPreds) && negPreds.IsSupersetOf(v.negPreds));
        }

        public VCExpr ToVcExpr(Func<int, VCExpr> predToExpr, VCExpressionGenerator gen)
        {
            if (isFalse) return VCExpressionGenerator.False;
            var ret = VCExpressionGenerator.True;
            posPreds.Iter(p => ret = gen.AndSimp(ret, predToExpr(p)));
            negPreds.Iter(p => ret = gen.AndSimp(ret, gen.Not(predToExpr(p))));
            return ret;
        }

        public Expr ToExpr(Func<int, Expr> predToExpr)
        {
            if (isFalse) return Expr.False;
            Expr ret = Expr.True;
            var pp = posPreds.ToList(); pp.Sort();
            var np = negPreds.ToList(); np.Sort();
            pp.Iter(p => ret = Expr.And(ret, predToExpr(p)));
            np.Iter(p => ret = Expr.And(ret, Expr.Not(predToExpr(p)))); 
            return ret;
        }

        public override string ToString()
        {
            if (isFalse)
                return "false";

            var ret = "";
            var first = true;
            foreach (var p in posPreds)
            {
                ret += string.Format("{0}{1}", first ? "" : " && ", PredicateAbs.PrePreds[ProcName][p]);
                first = false;
            }
            foreach (var p in negPreds)
            {
                ret += string.Format("{0}!{1}", first ? "" : " && ", PredicateAbs.PrePreds[ProcName][p]);
                first = false;
            }
            return ret;
        }
    }

    class FindSummaryPred : MutatingVCExprVisitor<bool>
    {
        public List<Tuple<string, bool, VCExprVar, VCExprNAry>> summaryPreds;
        int assertId;
        private static int CounterId = 0;

        public FindSummaryPred(VCExpressionGenerator gen, int assertId)
            : base(gen)
        {
            summaryPreds = new List<Tuple<string, bool, VCExprVar, VCExprNAry>>();
            this.assertId = assertId;
        }

        protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
                                              List<VCExpr/*!*/>/*!*/ newSubExprs,
            // has any of the subexpressions changed?
                                              bool changed,
                                              bool arg)
        {
            Contract.Ensures(Contract.Result<VCExpr>() != null);

            VCExpr ret;
            if (changed)
                ret = Gen.Function(originalNode.Op,
                                   newSubExprs, originalNode.TypeArguments);
            else
                ret = originalNode;

            VCExprNAry retnary = ret as VCExprNAry;
            if (retnary == null) return ret;
            var op = retnary.Op as VCExprBoogieFunctionOp;

            if (op == null)
            {
                var lop = retnary.Op as VCExprLabelOp;
                if (lop == null) return ret;
                if (lop.pos) return ret;
                if (!lop.label.Equals("@" + assertId.ToString())) return ret;
                
                //var subexpr = retnary[0] as VCExprNAry;
                //if (subexpr == null) return ret;
                //op = subexpr.Op as VCExprBoogieFunctionOp;
                //if (op == null) return ret;

                var subexpr = retnary[0] as VCExprVar;
                if (subexpr == null) return ret;
                if (!subexpr.Name.StartsWith("AbstractHoudiniControl")) return ret;

                for (int i = 0; i < summaryPreds.Count; i++)
                {
                    if (summaryPreds[i].Item3 == subexpr)
                        summaryPreds[i] = Tuple.Create(summaryPreds[i].Item1, true, summaryPreds[i].Item3, summaryPreds[i].Item4);
                }
                return ret;
            }

            string calleeName = op.Func.Name;

            if (!calleeName.EndsWith(AbstractHoudini.summaryPredSuffix))
                return ret;

            var controlConst = Gen.Variable("AbstractHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool);
            CounterId++;

            summaryPreds.Add(Tuple.Create(calleeName.Substring(0, calleeName.Length - AbstractHoudini.summaryPredSuffix.Length), false, controlConst, retnary));

            return controlConst;
            //return ret;
        }

    }

    class FindExistentialFunctions : MutatingVCExprVisitor<bool>
    {
        public List<Tuple<string, VCExprVar, VCExprNAry>> funcCalls;
        private HashSet<string> existentialFunctions;
        private static int CounterId = 0;

        public FindExistentialFunctions(VCExpressionGenerator gen, HashSet<string> existentialFunctions)
            : base(gen)
        {
            funcCalls = new List<Tuple<string, VCExprVar, VCExprNAry>>();
            this.existentialFunctions = existentialFunctions;
        }

        protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
                                              List<VCExpr/*!*/>/*!*/ newSubExprs,
            // has any of the subexpressions changed?
                                              bool changed,
                                              bool arg)
        {
            Contract.Ensures(Contract.Result<VCExpr>() != null);

            VCExpr ret;
            if (changed)
                ret = Gen.Function(originalNode.Op,
                                   newSubExprs, originalNode.TypeArguments);
            else
                ret = originalNode;

            VCExprNAry retnary = ret as VCExprNAry;
            if (retnary == null) return ret;
            var op = retnary.Op as VCExprBoogieFunctionOp;
            if (op == null) return ret;

            string calleeName = op.Func.Name;

            if (!existentialFunctions.Contains(calleeName))
                return ret;

            var controlConst = Gen.Variable("AbsHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool);
            CounterId++;

            funcCalls.Add(Tuple.Create(calleeName, controlConst, retnary));

            return controlConst;
        }

    }

    class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
    {
        public Model model;

        public AbstractHoudiniErrorReporter()
        {
            model = null;
        }

        public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)
        {
            Debug.Assert(model != null);
            if(CommandLineOptions.Clo.PrintErrorModel >= 1) model.Write(Console.Out);
            this.model = model;
        }
    }

    public class AbsHoudiniInternalError : System.ApplicationException
    {
        public AbsHoudiniInternalError(string msg) : base(msg) { }

    };

    public class SimpleUtil
    {
        // Constructs a mapping from procedure names to the implementation
        public static Dictionary<string, Implementation> nameImplMapping(Program p)
        {
            var m = new Dictionary<string, Implementation>();
            foreach (Declaration d in p.TopLevelDeclarations)
            {
                if (d is Implementation)
                {
                    Implementation impl = d as Implementation;
                    m.Add(impl.Name, impl);
                }
            }

            return m;
        }

        // is "assert true"?
        public static bool isAssertTrue(Cmd cmd)
        {
            var acmd = cmd as AssertCmd;
            if (acmd == null) return false;
            var le = acmd.Expr as LiteralExpr;
            if (le == null) return false;
            if (le.IsTrue) return true;
            return false;
        }
    }

}