public void TestBitvectorOps()
        {
            string noop = @"

            program noop(w) {
               return iter(c in w) {
              case (c <= 0xFF):
             yield((((c >> 4) & 0xF) << 4)|(c & 0xF));
              case (true):
             yield(c);
              };
            }
            ";

            string triv = @"

            program triv(w) {
               return iter(c in w) {
              case (true):
             yield(c);
              };
            }
            ";
            var solver = new Z3Provider();
            var A = BekConverter.BekToST(solver, noop);
            var B = BekConverter.BekToST(solver, triv);
            bool equiv = A.Eq1(B);
            Assert.IsTrue(equiv);
            //A.ShowGraph();
        }

        public Automaton<Expr> getAutomata(Z3Provider z3p, Expr universe, Expr var, Sort sort)
        {   //Sort for pairs (input theory, BV)
            var bv = z3p.Z3.MkBitVecSort(BVConst.BVSIZE);
            var pairSort = z3p.MkTupleSort(sort, bv);

            var dfapair = this.Normalize().PushQuantifiers().getAutomata(z3p, new List<string>(), universe, var, sort);            

            //Compute the new moves by dropping the last bit of every element in the phiMoves
            var newMoves = Automaton<Expr>.Empty.GetMoves().ToList();
            foreach (var oldMove in dfapair.GetMoves())
            {
                var oldCond = oldMove.Label;                             

                //Compute the new condition as ()
                Expr newCond = oldCond;
                

                //Update the new set of moves
                newMoves.Add(new Move<Expr>(oldMove.SourceState, oldMove.TargetState, newCond));
            }

            //Build the new dfa with the new moves
            var automaton = Automaton<Expr>.Create(dfapair.InitialState, dfapair.GetFinalStates(), newMoves);

            return automaton.Determinize(z3p).Minimize(z3p);
        }

        private static void RunTestForGivenSize(int K)
        {
            Console.WriteLine(K);
            Z3Provider Z = new Z3Provider();
            var A = (Z.TT.MkRankedAlphabet("A", Z.IntSort, new string[] { "zero", "two" }, new int[] { 0, 2 }));

            Func<int, Expr> beta = (i => Z.MkEq(Z.MkInt(1), Z.MkMod(Z.MkDiv(A.AttrVar, Z.MkInt(1 << (i%32))), Z.MkInt(2))));

            Expr e1 = Z.MkEq(Z.MkInt(1), A.AttrVar);
            Expr e2 = Z.MkEq(Z.MkInt(2), A.AttrVar);
            Expr e3 = Z.MkEq(Z.MkInt(3), A.AttrVar);

            var r1 = Z.TT.MkTreeAcceptorRule(A, 0, "zero", e1);
            var r2 = Z.TT.MkTreeAcceptorRule(A, 1, "zero", e2);
            var r3 = Z.TT.MkTreeAcceptorRule(A, 2, "zero", e3);
            var rules = new List<TreeRule>();

            rules.Add(r1);
            rules.Add(r2);
            rules.Add(r3);

            for (int i = 0; i < K; i++)
            {
                rules.Add(Z.TT.MkTreeAcceptorRule(A, 3 * i + 3, "two", beta(i), 3 * i, 3 * i + 2));
                rules.Add(Z.TT.MkTreeAcceptorRule(A, 3 * i + 4, "two", beta(i), 3 * i + 1, 3 * i + 2));
                rules.Add(Z.TT.MkTreeAcceptorRule(A, 3 * i + 5, "two", beta(i), 3 * i + 2, 3 * i + 2));
            }

            var T = Z.TT.MkTreeAutomaton(new int[] { 3 * K , 3 * K +1 }, A, A, rules);
            var comp = T.Complete();

            Util.RunAllAlgorithms(T, comp, K.ToString(), Program.largeAlphabetFile);
        }

 public void HexProjTest2()
 {
     Z3Provider z3p = new Z3Provider();
     Sort bv64 = z3p.MkBitVecSort(64);
     Sort bv16 = z3p.MkBitVecSort(16);
     Expr _0x654321 = z3p.MkNumeral((uint)0xF54321, bv64);
     Expr _6 = z3p.MkHexProj(5, _0x654321, bv16).Simplify();
     Expr _5 = z3p.MkHexProj(4, _0x654321, bv16).Simplify();
     Expr _4 = z3p.MkHexProj(3, _0x654321, bv16).Simplify();
     Expr _3 = z3p.MkHexProj(2, _0x654321, bv16).Simplify();
     Expr _2 = z3p.MkHexProj(1, _0x654321, bv16).Simplify();
     Expr _1 = z3p.MkHexProj(0, _0x654321, bv16).Simplify();
     int _6v = (int)z3p.GetNumeralInt(_6);
     int _5v = (int)z3p.GetNumeralInt(_5);
     int _4v = (int)z3p.GetNumeralInt(_4);
     int _3v = (int)z3p.GetNumeralInt(_3);
     int _2v = (int)z3p.GetNumeralInt(_2);
     int _1v = (int)z3p.GetNumeralInt(_1);
     Assert.AreEqual<int>(0xF, _6v);
     Assert.AreEqual<int>(5, _5v);
     Assert.AreEqual<int>(4, _4v);
     Assert.AreEqual<int>(3, _3v);
     Assert.AreEqual<int>(2, _2v);
     Assert.AreEqual<int>(1, _1v);
 }

        //[TestMethod]
        public void TestCssEncode5()
        {
            var solver = new Z3Provider();
            var stb = BekConverter.BekFileToSTb(solver, sampleDir + "bek/CssEncode5.bek");
            //stb.Explore().ShowGraph();
            var st = stb.ToST();
            //st.ShowGraph(10);
            var sft = st.Explore();
            //sft.ShowGraph(10);

            //just to get longer input strings
            var restr = sft.RestrictDomain("(.){3,}$");

            restr.Simplify();
            //restr.ShowGraph(10);

            restr.AssertTheory();

            Expr inputConst = solver.MkFreshConst("input", sft.InputListSort);
            Expr outputConst = solver.MkFreshConst("output", sft.OutputListSort);

            solver.MainSolver.Assert(restr.MkAccept(inputConst, outputConst));

            int okCnt = 0;
            int error0Cnt = 0;
            int error1Cnt = 0;

            //validate correctness for some values against the actual CssEncode
            //TBD: validate also exceptional behavior
            int K = 10;
            for (int i = 0; i < K; i++)
            {
                var model = solver.MainSolver.GetModel(solver.True, inputConst, outputConst);
                string input = model[inputConst].StringValue;
                string output = model[outputConst].StringValue;

                Assert.IsFalse(string.IsNullOrEmpty(input));
                Assert.IsFalse(string.IsNullOrEmpty(output));
                if ((input != ""))
                {
                    char lastChar = '\0'; //output[output.Length - 1];

                    try
                    {
                        var output_expected = System.Web.Security.AntiXss.AntiXssEncoder.CssEncode(input);
                        Assert.AreEqual<string>(output_expected, output);
                        okCnt += 1;
                    }
                    catch (Exception)
                    {
                        Assert.AreEqual<char>('\0', lastChar);
                        error0Cnt += 1;
                    }
                }
                //exclude this solution, before picking the next one
                solver.MainSolver.Assert(solver.MkNeq(inputConst, model[inputConst].Value));
            }
            Assert.AreEqual(K, okCnt);
        }

 // [TestMethod]
 public void DecodeDecode()
 {
     Z3Provider solver = new Z3Provider();
     var A = BekConverter.BekToSTb(solver, BekConverter.BekFileToBekProgram(sampleDir + "bek/Base64decode.bek")).ExploreBools().ToST();
     var ID = ST<FuncDecl, Expr, Sort>.MkId(solver, solver.CharSort);
     var st = A.Compose(A);
     //st.ShowGraph();
     var sfa1 = st.ToSFA().Automaton;
     var sfa = ConvertToAutomatonOverBvSet(solver, sfa1).Determinize().MinimizeHopcroft();
     //solver.CharSetProvider.ShowGraph(sfa, "test");
 }

 public void EmptyTupleTest()
 {
     Z3Provider Z = new Z3Provider();
     Sort sort = Z.MkTupleSort();
     Expr unit = Z.MkTuple();
     Expr t = Z.MkVar(0, sort);
     Expr t_eq_unit = Z.MkEq(t, unit);
     var v = new List<IValue<Expr>>(Z.MainSolver.FindAllMembers(t_eq_unit));
     Assert.IsTrue(v.Count == 1);
     Assert.AreEqual(unit, v[0].Value);
 }

 public void TestCreationOfTwoAlphabets1()
 {
     Z3Provider Z = new Z3Provider();
     var A = Z.TT.MkRankedAlphabet("A", Z.IntSort, new string[] { "zero", "one", "two" }, new int[] { 0, 1, 2 });
     var B = Z.TT.MkRankedAlphabet("B", Z.IntSort, new string[] { "zero", "one", "two" }, new int[] { 0, 1, 2 });
     Assert.IsTrue(A.ContainsConstructor("two"));
     Assert.IsTrue(B.ContainsConstructor("two"));
     var twoA = A.GetConstructor("two");
     var twoB = B.GetConstructor("two");
     Assert.AreNotEqual<FuncDecl>(twoA, twoB);
     Assert.AreEqual<string>("two", twoA.Name.ToString());
     Assert.AreEqual<string>("two", twoB.Name.ToString());
 }

 public void ZeroOneTwoAlphabetTest2()
 {
     Z3Provider z3p = new Z3Provider();
     try
     {   //number of ranks is wrong
         var A = z3p.TT.MkRankedAlphabet("A", z3p.IntSort, new string[] { "zero", "one", "two" }, new int[] { 0, 1 });
         Assert.IsTrue(false, "expecting exception RankedAlphabet_IsInvalid");
     }
     catch (AutomataException e)
     {
         Assert.IsTrue(AutomataExceptionKind.RankedAlphabet_IsInvalid == e.kind);
     }
 }

 public void TestCreationOfTwoAlphabets2()
 {
     try
     {
         Z3Provider Z = new Z3Provider();
         var A = Z.TT.MkRankedAlphabet("A", Z.IntSort, new string[] { "zero", "one", "two" }, new int[] { 0, 1, 2 });
         var B = Z.TT.MkRankedAlphabet("A", Z.IntSort, new string[] { "zero", "two" }, new int[] { 0, 1 });
         Assert.IsTrue(false, "expecting exception RankedAlphabet_IsAlreadyDefined");
     }
     catch (AutomataException e)
     {
         Assert.IsTrue(e.kind == AutomataExceptionKind.RankedAlphabet_IsAlreadyDefined);
     }
 }

        public void TestBase64Decode()
        {
            Z3Provider solver = new Z3Provider();
            var bek = BekConverter.BekFileToBekProgram(sampleDir + "bek/Base64decode.bek");
            var st = BekConverter.BekToSTb(solver, bek).ExploreBools().ToST();
            st.Simplify();
            //st.ShowGraph();
            var st0 = st.RestrictDomain(@"^([AB]{3})*$");
            //st0.ShowGraph();
            var st1 = st0.Explore();
            //st1.Simplify();
            //st1.ShowGraph();
            //st.ToDot("c:/tmp/b64d.dot");
            var sft = st.Explore();
            var Q = sft.StateCount;
            int M = 0;
            int F = 0;
            int tot = 0;
            var tmp = new Dictionary<Expr, int>();
            foreach (var m in sft.GetMoves())
            {
                if (m.Label.IsFinal)
                {
                    F += 1;
                    tot += 1;
                }
                else
                {
                    M += 1;
                    int k = 0;
                    if (tmp.TryGetValue(m.Label.Guard, out k))
                        tot += k;
                    else
                    {
                        foreach (var v in solver.MainSolver.FindAllMembers(m.Label.Guard))
                            k += 1;
                        tot += k;
                        tmp[m.Label.Guard] = k;
                    }
                }
            }
            Console.WriteLine(tot);

            Assert.AreEqual<int>(87, Q);
        }

 public void FuncDeclTest3()
 {
     try
     {
         Z3Provider Z = new Z3Provider();
         Z.MainSolver.Push();
         FuncDecl f = Z.MkFuncDecl("temp", Z.IntSort, Z.IntSort);
         Z.MainSolver.Push();
         Z.MainSolver.Push();
         Z.MainSolver.Pop();
         Z.MainSolver.Pop();
         FuncDecl g = Z.MkFuncDecl("temp", Z.IntSort, Z.IntSort);
         Z.MainSolver.Push();
         Z.MainSolver.Pop();
     }
     catch (AutomataException e)
     {
         Assert.AreEqual(e.kind, AutomataExceptionKind.FunctionIsAlreadyDeclared);
     }
 }

        public void Test_aaa2b_Keep()
        {
            string bek = @"
program a2b(_){ 
  replace {
     ""aaa"" ==> [#1 + 1];
     else  ==> [#0];
  }
}";
            Z3Provider solver = new Z3Provider();
            var st = BekConverter.BekToSTb(solver, bek).ToST();
            //st.ShowGraph();
            var st1 = st.ExploreBools();
            //st1.ShowGraph();
            var stb = st1.ToSTb();
            //stb.ShowGraph();
            var meth = stb.Compile();
            var res = meth.Apply("ac_aaaaGGhh");
            Assert.AreEqual<string>("ac_baGGhh", res);
        }

 public Const(ConstDef def, FastTransducerInstance fti, Z3Provider z3p)
 {
     this.z3p = z3p;
     this.name = def.id.text;
     switch (def.sort.kind)
     {
         case (FastSortKind.Real):
             {
                 sort = z3p.RealSort;
                 break;
             }
         case (FastSortKind.Bool):
             {
                 sort = z3p.BoolSort;
                 break;
             }
         case (FastSortKind.Int):
             {
                 sort = z3p.IntSort;
                 break;
             }
         case (FastSortKind.String):
             {
                 sort = z3p.MkListSort(z3p.CharSort);
                 break;
             }
         case (FastSortKind.Tree):
             {
                 foreach (var enumSort in fti.enums)
                 {
                     if (enumSort.name == def.sort.name.text)
                     {
                         sort = enumSort.sort;
                         break;
                     }
                 }
                 break;
             }
     }
     this.value = GenerateZ3ExprFromExpr(def.expr, fti).Simplify();
 }

        public void TestCssEncode4eq5()
        {
            var solver = new Z3Provider();
            var stb5 = BekConverter.BekFileToSTb(solver, sampleDir + "bek/CssEncode5.bek");
            var stb4 = BekConverter.BekFileToSTb(solver, sampleDir + "bek/CssEncode4.bek");
            //stb5.ShowGraph(10);
            var fst4 = stb4.ToST().Explore();
            var fst5 = stb5.ToST().Explore();
            var dom4 = fst4.ToSFA();
            var dom5 = fst5.ToSFA();
            bool dom4_subsetof_dom5 = dom4.IsSubsetOf(dom5);
            //var tmp = dom4.Minus(dom5);
            //tmp.ShowGraph();
            //var member = new List<Expr>(tmp.ChoosePathToSomeFinalState()).ToArray();
            //var str = new String(Array.ConvertAll(member, m => solver.GetCharValue(solver.FindOneMember(m).Value)));

            bool dom5_subsetof_dom4 = dom5.IsSubsetOf(dom4);
            bool partial_equiv = fst4.Eq1(fst5);
            Assert.IsTrue(dom4_subsetof_dom5);
            Assert.IsTrue(partial_equiv);
            Assert.IsTrue(dom5_subsetof_dom4);
        }

 public void ZeroOneTwoAlphabetTest1()
 {
     Z3Provider z3p = new Z3Provider();
     var A = z3p.TT.MkRankedAlphabet("A", z3p.IntSort, new string[] { "zero", "one", "two" }, new int[] { 0, 1, 2 });
     var Asort = A.AlphabetSort;
     Assert.IsTrue(A.AlphabetSort.Equals(Asort));
     Assert.IsTrue(A.ContainsConstructor("one"));
     Assert.IsFalse(A.ContainsConstructor("one1"));
     Assert.IsTrue(A.GetRank("one") == 1);
     Assert.IsTrue(z3p.GetDomain(A.GetTester("one")).Length == 1);
     Assert.IsTrue(z3p.GetDomain(A.GetTester("one"))[0].Equals(Asort));
     Assert.IsTrue(z3p.GetDomain(A.GetConstructor("one")).Length == 2);
     Assert.IsTrue(z3p.GetDomain(A.GetConstructor("one"))[0].Equals(z3p.IntSort));
     Assert.IsTrue(z3p.GetDomain(A.GetConstructor("one"))[1].Equals(Asort));
     Assert.IsTrue(z3p.GetRange(A.GetConstructor("one")).Equals(Asort));
     Assert.IsTrue(z3p.GetDomain(A.GetChildAccessor("one", 1)).Length.Equals(1));
     Assert.IsTrue(z3p.GetDomain(A.GetChildAccessor("one", 1))[0].Equals(Asort));
     Assert.IsTrue(z3p.GetRange(A.GetChildAccessor("one", 1)).Equals(Asort));
     Assert.IsTrue(z3p.GetDomain(A.GetAttributeAccessor("one")).Length.Equals(1));
     Assert.IsTrue(z3p.GetDomain(A.GetAttributeAccessor("one"))[0].Equals(Asort));
     Assert.IsTrue(z3p.GetRange(A.GetAttributeAccessor("one")).Equals(z3p.IntSort));
 }

        public static string GetDTAMINFormatString(TreeTransducer aut)
        {
            Z3Provider Z = new Z3Provider();
            StringBuilder sb = new StringBuilder();

            var transition = aut.GetRules();
            foreach (var rule in transition)
            {
                sb.Append(Z.GetNumeralInt(rule.State) + 1);
                sb.Append(" ");
                sb.Append(rule.Symbol.Name.ToString());

                for (int j = 1; j <= rule.Rank; j++)
                {
                    var args_j = rule.Lookahead(j - 1);
                    if (args_j.ToList().Count > 1)
                        throw new Exception("Some i has more than one state");
                    foreach (var rlastate in args_j)
                    {
                        sb.Append(" ");
                        sb.Append(Z.GetNumeralInt(rlastate)+1);
                    }
                }
                sb.AppendLine();
            }

            int c = 0;
            foreach (var st in aut.roots)
            {
                if(c==aut.roots.Count-1)
                    sb.Append("0 " + (Z.GetNumeralInt(st) + 1));
                else
                    sb.AppendLine("0 " + (Z.GetNumeralInt(st) + 1));
                c++;
            }

            return sb.ToString();
        }

        public void TestPositionConflict()
        {
            string bek1 = @"
            program decode(input){
            replace {
              ""&"" ==> ""&"";
              ""&lt;"" ==> ""<"";
              ""&gt;"" ==> "">"";
              else ==> [#0];
            }
            }
            ";
            string bek2 = @"
            program decode(input){
            replace {
              ""&amp;"" ==> ""&"";
              ""&lt;"" ==> ""<"";
              ""&gt;"" ==> "")"";
              else ==> [#0];
            }
            }
            ";
            Z3Provider solver = new Z3Provider(BitWidth.BV16);
            var test1 = BekConverter.BekToSTb(solver, bek1).ExploreBools();
            //test1.ShowGraph();
            var meth1 = test1.Compile();
            var test2 = BekConverter.BekToSTb(solver, bek2).ExploreBools();
            //test1.ShowGraph();
            var meth2 = test2.Compile();

            //just test on couple of samples
            Assert.AreEqual<string>("<", meth1.Apply("&lt;"));
            Assert.AreEqual<string>(">", meth1.Apply("&gt;"));
            Assert.AreEqual<string>("&g>", meth1.Apply("&g&gt;"));
            Assert.AreEqual<string>("&g>", meth1.Apply("&g&gt;"));

            var d1 = test1.ToST().Explore();
            var d2 = test2.ToST().Explore();
            var witness = d1.Neq1(d2);
            Assert.IsFalse(witness == null);
            var inp = new String(Array.ConvertAll(witness.ToArray(), x => (char)solver.GetNumeralInt(x)));
            var out1 = meth1.Apply(inp);
            var out2 = meth2.Apply(inp);
            Assert.AreNotEqual<string>(out1, out2);
        }

        public void TestLengthConflict()
        {
            string bek = @"
            program decode(input){
            replace {
              ""&"" ==> ""&"";
              ""&lt;"" ==> ""<"";
              ""&gt;"" ==> "">"";
              else ==> [#0];
            }
            }
            ";
            Z3Provider solver = new Z3Provider(BitWidth.BV16);
            var test = BekConverter.BekToSTb(solver, bek);
            var test1 = test.ExploreBools();
            //test1.ShowGraph();
            //var meth = test1.Compile();

            //just test on couple of samples
            //Assert.AreEqual<string>("<", meth.Apply("&lt;"));
            //Assert.AreEqual<string>(">", meth.Apply("&gt;"));
            //Assert.AreEqual<string>("&g>", meth.Apply("&g&gt;"));
            //Assert.AreEqual<string>("&g>", meth.Apply("&g&gt;"));

            var dec = test.ToST();
            var d = dec.Explore();

            var dd = d.Compose(d);
            //var ddmeth = dd.ToSTb().Compile();
            var witness = d.Neq1(dd);

            Assert.IsFalse(witness == null);
            var inp = new String(Array.ConvertAll(witness.ToArray(), x => (char)solver.GetNumeralInt(x)));
            //var out1 = meth.Apply(inp);
            //var out2 = ddmeth.Apply(inp);
            var out1b = new String(Array.ConvertAll(new List<Expr>(dec.Apply(witness)).ToArray(), x => ((char)solver.GetNumeralInt(x))));
            var out2b = new String(Array.ConvertAll(new List<Expr>(dd.Apply(witness)).ToArray(), x => ((char)solver.GetNumeralInt(x))));
            //Assert.AreEqual<string>(out1, out1b);
            //Assert.AreEqual<string>(out2, out2b);
            Assert.AreNotEqual<string>(out1b, out2b);
        }

        private static int MintermBlowupTestHelperMoore(int K)
        {
            var z3p = new Z3Provider(BitWidth.BV32);
            var x = z3p.CharVar;
            var zero = z3p.MkNumeral(0, z3p.CharSort);
            Func<int, Expr> gamma = k =>
            {
                int kth = 1 << k;
                Expr mask = z3p.MkNumeral(kth, z3p.CharSort);
                Expr cond = z3p.MkNot(z3p.MkEq(z3p.MkBvAnd(x, mask), zero));
                return cond;
            };
            var moves = new List<Move<Expr>>();
            for (int i = 0; i < K; i++)
                moves.Add(Move<Expr>.Create(i, i + 1, gamma(i)));
            for (int i = 0; i < K; i++)
                moves.Add(Move<Expr>.Create(i == 0 ? 0 : K + i, K + i + 1, i ==0 ? z3p.MkNot(gamma(i)) : gamma(i)));
            var aut = Automaton<Expr>.Create(z3p, 0, new int[] { K, 2 * K }, moves);

            var sfa = new SFA<FuncDecl, Expr, Sort>(z3p, z3p.CharSort, aut);
            sfa.Automaton.CheckDeterminism(true);

            int t = System.Environment.TickCount;
            var autmin = sfa.Automaton.MinimizeMoore();
            t = System.Environment.TickCount - t;

            return t;
        }