microsoft / zen Goto Github PK

CSC : warning CS8034: Unable to load Analyzer assembly /Users/a/.nuget/packages/zenlib.generators/0.1.3/analyzers/dotnet/cs/ZenLib.Generators.dll : Unable to load ZenLib.Generators [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/Point.cs(9,28): error CS1061: 'Zen<Point>' does not contain a definition for 'GetX' and no accessible extension method 'GetX' accepting a first argument of type 'Zen<Point>' could be found (are you missing a using directive or an assembly reference?) [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/Point.cs(9,40): error CS1061: 'Zen<Point>' does not contain a definition for 'GetX' and no accessible extension method 'GetX' accepting a first argument of type 'Zen<Point>' could be found (are you missing a using directive or an assembly reference?) [/Users/a/test/Test/Test.csproj]
...

/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(6,11): error CS1001: Identifier expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(6,11): error CS1514: { expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(6,12): error CS0116: A namespace cannot directly contain members such as fields, methods or statements [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(6,28): error CS1001: Identifier expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(6,28): error CS1514: { expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(7,1): error CS1022: Type or namespace definition, or end-of-file expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/ZenLib.Generators/ZenLib.Generators.ZenIncrementalGenerator/PointExtensions_0_zen.g.cs(58,2): error CS1513: } expected [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/Point.cs(9,28): error CS1061: 'Zen<Point>' does not contain a definition for 'GetX' and no accessible extension method 'GetX' accepting a first argument of type 'Zen<Point>' could be found (are you missing a using directive or an assembly reference?) [/Users/a/test/Test/Test.csproj]
/Users/a/test/Test/Point.cs(9,40): error CS1061: 'Zen<Point>' does not contain a definition for 'GetX' and no accessible extension method 'GetX' accepting a first argument of type 'Zen<Point>' could be found (are you missing a using directive or an assembly reference?) [/Users/a/test/Test/Test.csproj]
...

    public class /* struct */ Matrix3x3
    {
        public int v11, v12, v13;
        public int v21, v22, v23;
        public int v31, v32, v33;
    }

    class Program
    {
        static Zen<bool> PerformMath(Zen<Matrix3x3> m)
        {
            return true;
        }

        static void Main(string[] args)
        {
            var function = Function<Matrix3x3,bool>(PerformMath);
            var input = function.Find((a, result) => result);
        }
    }

System.InvalidOperationException: 'Sequence contains no elements'
   at System.Linq.ThrowHelper.ThrowNoElementsException()
   at System.Linq.Enumerable.First[TSource](IEnumerable`1 source)
   at Microsoft.Research.Zen.Generation.GeneratorHelper.GetCreateObjectMethod(Int32 numFields) in C:\Users\de\Source\Repos\Zen\Zen\Generation\GeneratorHelper.cs:line 54
   at Microsoft.Research.Zen.Generation.GeneratorHelper.ApplyToObject(Func`2 recurse, Type objectType, Dictionary`2 fields) in C:\Users\de\Source\Repos\Zen\Zen\Generation\GeneratorHelper.cs:line 91
   at Microsoft.Research.Zen.Generation.SymbolicInputGenerator.VisitObject(Func`2 recurse, Type objectType, Dictionary`2 fields) in C:\Users\de\Source\Repos\Zen\Zen\Generation\SymbolicInputGenerator.cs:line 109
   at Microsoft.Research.Zen.ReflectionUtilities.ApplyTypeVisitor[T](ITypeVisitor`1 visitor, Type type) in C:\Users\de\Source\Repos\Zen\Zen\ReflectionUtilities.cs:line 341
   at Microsoft.Research.Zen.Language.Arbitrary[T](Int32 listSize, Boolean checkSmallerLists) in C:\Users\de\Source\Repos\Zen\Zen\Language.cs:line 125
   at Microsoft.Research.Zen.ZenFunction`2.Find(Func`3 invariant, Zen`1 input, Int32 listSize, Boolean checkSmallerLists, Boolean simplify, Backend backend) in C:\Users\de\Source\Repos\Zen\Zen\ZenFunction.cs:line 158
   at BrentEq.Program.Main(String[] args) in C:\Users\de\Source\Repos\Zen\BrentEq\Program.cs:line 24

CancellationTokenSource cts = new CancellationTokenSource(TimeSpan.FromSeconds(10));
var solution = Zen.And(constraints).Solve(cancellationToken: cts.Token);

var solution = Zen.And(constraints).Solve(timeout: TimeSpan.FromSeconds(10));

int len = 5; // 5 will succeed with solution {1, 2, 0, 0, 0}, but 6 will not find solutions?
var l = Zen.Symbolic<FSeq<byte>>();
var idx = Zen.Symbolic<BigInteger>();
var sol = And(
  l.Length() == (BigInteger)len,
  l.At(idx) == Option.Some<byte>(1),
  l.At(idx + new BigInteger(1)) == Option.Some<byte>(2)).Solve(Solver.SolverType.Z3);