ZenLib 3.1.5
See the version list below for details.
dotnet add package ZenLib version 3.1.5
NuGet\InstallPackage ZenLib Version 3.1.5
<PackageReference Include="ZenLib" Version="3.1.5" />
paket add ZenLib version 3.1.5
#r "nuget: ZenLib, 3.1.5"
// Install ZenLib as a Cake Addin #addin nuget:?package=ZenLib&version=3.1.5 // Install ZenLib as a Cake Tool #tool nuget:?package=ZenLib&version=3.1.5
Introduction
Zen is a constraint solving library for .NET. Zen makes it easy to express highlevel symbolic computations directly in .NET. It translates these symbolic expressions to lowlevel constraint solvers and then back to .NET objects. The Zen library comes equipped with a number of builtin tools for processing symbolic models, including a compiler (to .NET IL), an exhaustive model checker, and a test input generator. It supports multiple backends including one based on the Z3 SMT solver and another based on Binary Decision Diagrams (BDDs).
Table of contents
 Introduction
 Table of contents
 Installation
 Overview of Zen
 Supported data types
 Zen Attributes
 Solver Backends
 Solver Timeouts
 Example: Network ACLs
 Implementation Details
 Contributing
<a name="installation"></a>
Installation
Just add the project to your visual studio solution. Alternatively, a nuget package is available here.
<a name="overviewofzen"></a>
Overview of Zen
To import the Zen library, add the following line to your source file:
using ZenLib;
Most library methods are found in the Zen.*
namespace. To avoid having to write this prefix out every time, you can alternatively add the following using statement:
using static ZenLib.Zen;
The Zen library provides the type Zen<T>
, which represents a symbolic value of type T
. The library can then solve constraints involving symbolic values. The following code shows a basic use of Zen  it creates several symbolic variables of different types (e.g., bool
, int
, string
, FSeq
 finite sequences) and then encodes constraints over those variables.
// create symbolic variables of different types
var b = Zen.Symbolic<bool>();
var i = Zen.Symbolic<int>();
var s = Zen.Symbolic<string>();
var o = Zen.Symbolic<Option<ulong>>();
var l = Zen.Symbolic<FSeq<int>>(depth: 10);
// build constraints on these variables
var c1 = Zen.Or(b, i <= 10);
var c2 = Zen.Or(Zen.Not(b), o == Option.Some(1UL));
var c3 = Zen.Or(s.Contains("hello"), o.IsNone());
var c4 = Zen.And(
l.Where(x => x == i).Length() == (BigInteger)5,
Zen.Not(l.All(x => x == i)));
var c5 = l.All(x => Zen.And(x >= 0, x <= 100));
// solve the constraints to get a solution
var solution = Zen.And(c1, c2, c3, c4, c5).Solve();
System.Console.WriteLine("b: " + solution.Get(b));
System.Console.WriteLine("i: " + solution.Get(i));
System.Console.WriteLine("s: " + solution.Get(s));
System.Console.WriteLine("o: " + solution.Get(o));
System.Console.WriteLine("l: " + string.Join(",", solution.Get(l)));
An example output is the following values:
b: True
i: 38
s: hello
o: Some(1)
l: [10,38,38,38,38,38]
<a name="computingwithzenexpressions"></a>
Zen Expressions
Zen<T>
objects are just normal .NET objects, we can pass them and return them from functions. For instance, the following code computes a new symbolic integer from two integer inputs x
and y
:
Zen<int> MultiplyAndAdd(Zen<int> x, Zen<int> y)
{
return 3 * x + y;
}
Zen overloads common C# operators such as &,,^,<=, <, >, >=, +, , *, true, false
to work with Zen values and supports implicit conversions to lift C# values (of type T
) to Zen values (of type Zen<T>
). Zen can represent a "function" like the one above to perform various symbolic tasks by creating a ZenFunction
to wrap the MultiplyAndAdd
function:
var function = new ZenFunction<int, int, int>(MultiplyAndAdd);
<a name="executingafunction"></a>
Executing a function
Zen can execute the function we have built on inputs by calling the Evaluate
method on the ZenFunction
:
var output = function.Evaluate(3, 2); // output = 11
This will interpret the expression tree created by the Zen function at runtime and return back a C# int
value in this case. Of course interpreting a tree is quite slow compared to multiplying a few numbers, so if you need to execute a function many times, Zen can compile the model using the C# System.Reflection.Emit
API. This generates IL instructions that execute efficiently  as if the function had been written using actual int
values. Doing so is easy, just call the Compile
method on the function first:
function.Compile();
output = function.Evaluate(3, 2); // output = 11
Or alternatively:
Func<int, int, int> f = Zen.Compile(MultiplyAndAdd);
var output = f(3, 2); // output = 11
We can see the difference by comparing the performance between the two:
var watch = System.Diagnostics.Stopwatch.StartNew();
for (int i = 0; i < 1000000; i++)
function.Evaluate(3, 2);
Console.WriteLine($"interpreted function time: {watch.ElapsedMilliseconds}ms");
watch.Restart();
function.Compile();
Console.WriteLine($"compilation time: {watch.ElapsedMilliseconds}ms");
watch.Restart();
for (int i = 0; i < 1000000; i++)
function.Evaluate(3, 2);
Console.WriteLine($"compiled function time: {watch.ElapsedMilliseconds}ms");
interpreted function time: 4601ms
compilation time: 4ms
compiled function time: 2ms
<a name="searchingforinputs"></a>
Searching for inputs
Zen can find function inputs that lead to some (un)desirable outcome. For example, we can find an (x, y)
input pair such that x
is less than zero and the output of the function is 11
:
var input = function.Find((x, y, result) => Zen.And(x <= 0, result == 11));
// input.Value = (1883171776, 1354548043)
The type of the result in this case is Option<(int, int)>
, which will have a pair of integer inputs that make the output 11 if such a pair exists. In this case the library will find x = 1883171776
and y = 1354548043
To find multiple inputs, Zen supports an equivalent FindAll
method, which returns an IEnumerable
of inputs where each input in inputs
will be unique so there are no duplicates.
using System.Linq;
...
var inputs = function.FindAll((x, y, result) => Zen.And(x <= 0, result == 11)).Take(5);
<a name="computingwithsets"></a>
Computing with sets
While the Find
function provides a way to find a single input to a function, Zen also provides an additional API for reasoning about sets of inputs and outputs to functions. It does this through a StateSetTransformer
API. A transformer is created by calling the Transformer()
method on a ZenFunction
(or by calling Zen.Transformer(...)
):
var f = new ZenFunction<uint, uint>(i => i + 1);
StateSetTransformer<uint, uint> t = f.Transformer();
Transformers allow for manipulating (potentially huge) sets of objects efficient. For example, we can get the set of all input uint
values where adding one will result in an output y
that is no more than 10 thousand:
StateSet<uint> inputSet = t.InputSet((x, y) => y <= 10000);
This set will include all the values 0  9999
as well as uint.MaxValue
due to wrapping. Transformers can also manpulate sets by propagating them forward or backwards:
StateSet<uint> outputSet = t.TransformForward(inputSet);
Finally, StateSet
objects can also be intersected, unioned, and negated. We can pull an example element out of a set as follows (if one exists):
Option<uint> example = inputSet.Element(); // example.Value = 0
Internally, transformers leverage binary decision diagrams to represent, possibly very large, sets of objects efficiently.
<a name="generatingtestinputs"></a>
Generating test inputs
Zen can automatically generate test inputs for a given model by finding inputs that will lead to different execution paths. For instance, consider an insertion sort implementation. We can ask Zen to generate test inputs for the function that can then be used, for instance to test other sorting algorithms:
var f = new ZenFunction<Pair<int, int>, int>(pair => Zen.If<int>(pair.Item1() < pair.Item2(), 1, 2));
foreach (var input in f.GenerateInputs())
{
Console.WriteLine($"input: {input}");
}
In this case, we get the following output:
input: (0, 0)
input: (0, 1)
The test generation approach uses symbolic execution to enumerate program paths and solve constraints on inputs that lead down each path. Each Zen.If
expression is treated as a program branch point (note: you can set the setting Settings.PreserveBranches = true
to prevent Zen from simplifying formulas involving If
by default if you want to preserve the expression structure.).
<a name="optimization"></a>
Optimization
Zen supports optimization of objective functions subject to constraints. The API is similar to that for Solve
, but requires a maximization or minimization objective. The solver will find the maximal satisfying assignment to the variables.
var a = Zen.Symbolic<Real>();
var b = Zen.Symbolic<Real>();
var constraints = Zen.And(a <= (Real)10, b <= (Real)10, a + (Real)4 <= b);
var solution = Zen.Maximize(objective: a + b, subjectTo: constraints); // a = 6, b = 10
<a name="supporteddatatypes"></a>
Supported data types
Zen currently supports a subset of .NET types and also introduces some of its own data types summarized below.
.NET Type  Description  Supported by Z3 backend  Supported by BDD backend  Supported by StateSetTransformers 

bool 
{true, false}  ✔️  ✔️  ✔️ 
byte 
8bit value  ✔️  ✔️  ✔️ 
char 
16bit UTF16 character  ✔️  ✔️  ✔️ 
short 
16bit signed value  ✔️  ✔️  ✔️ 
ushort 
16bit unsigned value  ✔️  ✔️  ✔️ 
int 
32bit signed value  ✔️  ✔️  ✔️ 
uint 
32bit unsigned value  ✔️  ✔️  ✔️ 
long 
64bit signed value  ✔️  ✔️  ✔️ 
ulong 
64bit unsigned value  ✔️  ✔️  ✔️ 
Int<_N> 
Nbit signed value  ✔️  ✔️  ✔️ 
UInt<_N> 
Nbit unsigned value  ✔️  ✔️  ✔️ 
Option<T> 
an optional/nullable value of type T 
✔️  ✔️  ✔️ 
Pair<T1, ...> 
pairs of different values  ✔️  ✔️  ✔️ 
class , struct 
classes and structs with public fields and/or properties  ✔️  ✔️  ✔️ 
FSeq<T> 
finite length sequence of elements of type T 
✔️  ➖  ➖ 
FSet<T> 
finite size set of elements of type T 
✔️  ➖  ➖ 
FString 
finite length string  ✔️  ➖  ➖ 
BigInteger 
arbitrary length integer  ✔️  ➖  ➖ 
Real 
arbitrary precision rational number  ✔️  ➖  ➖ 
Map<T1, T2> 
arbitrary size maps of keys and values of type T1 and T2 . Note that T1 and T2 can not use finite sequences 
✔️  ➖  ➖ 
Set<T> 
arbitrary size sets of values of type T . Same restrictions as with Map<T1, T2> 
✔️  ➖  ➖ 
CMap<T1, T2> 
maps of constant keys of type T1 to values of type T2 . 
✔️  ➖  ➖ 
CSet<T> 
sets of constants of type T . 
✔️  ➖  ➖ 
Array<T, _N> 
Fixed size arrays of values of type T . 
✔️  ➖  ➖ 
Seq<T> 
arbitrary size sequences of values of type T . Same restrictions as with Set<T> . Note that SMT solvers use heuristics to solve for sequences and are incomplete. 
✔️  ➖  ➖ 
string 
arbitrary size strings. Implemented as Seq<char> 
✔️  ➖  ➖ 
<a name="primitivetypes"></a>
Primitive types
Zen supports the primitive types bool, byte, char, short, ushort, int, uint, long, ulong
. All primitive types support (in)equality and integer types support integer arithmetic operations. As an example:
var x = Symbolic<int>();
var y = Symbolic<int>();
var c1 = (~x & y) == 1;
var c2 = And(x + y > 0, x + y < 100);
var solution = And(c1, c2).Solve(); // x = 20, y = 105
<a name="integertypes"></a>
Integer types
Aside from primitive types, Zen also supports the BigInteger
type found in System.Numerics
for reasoning about ubounded integers as well as other types of integers with fixed, but nonstandard bit width (for instance a 7bit integer). Out of the box, Zen provides the types Int<_N>
and UInt<_N>
for N
=1, 2, 3, ..., 99, 100, 128, 256, 512 ,1024. You can also create a custom integer size by simply declaring a new struct:
public struct _101 { }
<a name="optionsandtuples"></a>
Options, Tuples
Zen offers Pair<T1, T2, ...>
, types as a lightweight alternative to classes. By default all values are assumed to be nonnull by Zen. For nullable values, it provides an Option<T>
type.
var b = Symbolic<Option<byte>>();
var p = Symbolic<Pair<int, int>>>();
var solution = And(b.IsNone(), p.Item1() == 3).Solve(); // b = None, p = (3, 0)
<a name="realvalues"></a>
Real Values
Zen supports arbitrary precision rational numbers through the Real
type.
var c = new Real(3, 2); // the fraction 3/2 or equivalently 1.5
var x = Symbolic<Real>();
var y = Symbolic<Real>();
var solution = (2 * x + 3 * y == c).Solve(); // x = 1/2, y = 1/6
<a name="finitesequencesbagsmaps"></a>
Finite Sequences, Bags, Maps
Zen supports several highlevel data types that are finite (bounded) in size (the default size is 5 but can be changed). These include:
FSeq<T>
for reasoning about variable length sequences of values where the order is important.FSet<T>
represents finite sets.
One can implement complex functionality over FSeq<T>
types by combining the elements of the sequence. For instance, we can sum the elements of a sequence:
public Zen<int> Sum<T>(Zen<FSeq<int>> seq)
{
return seq.Fold(Zen.Constant(0), (x, y) => x + y);
}
<a name="unboundedsetsmaps"></a>
Unbounded Sets and Maps
Zen supports Set<T>
and Map<T1, T2>
data types that do not restrict the size of the set/map. This type only works with the Z3 backend and requires that T
, T1
and T2
not contain any finitized types (FSeq
, FString
, or FSet
). Primitive types (bool, integers, string, BigInteger), classes/structs are allowed.
var s = Symbolic<string>();
var s1 = Symbolic<Set<string>>();
var s2 = Symbolic<Set<string>>();
var s3 = Symbolic<Set<string>>();
var s4 = Symbolic<Set<string>>();
var c1 = s1.Contains("a");
var c2 = s1.Intersect(s2).Contains("b");
var c3 = Implies(s == "c", s3.Add(s) == s2);
var c4 = s4 == s1.Union(s2);
var solution = And(c1, c2, c3, c4).Solve(); // s = "a", s1 = {b, a}, s2 = {b}, s3 = {}, s4 = {b, a}
<a name="constantsetsmaps"></a>
Constant Sets and Maps
Arbitrary sets and maps described above are compiled to the SMT solver theory of Arrays. While this theory is quite general, it has known performance limitations. As a lightweight alternative, Zen provides the CMap<T1, T2>
and CSet<T>
classes that offer similar APIs but with the restriction that any map keys or set elements must be C# constant values and not Zen expressions. Zen will compile these sets and maps by creating fresh variables for all possible constants used by the user for these types.
Constant maps are useful for managing a finite number of unknown variables that should be indexed to some data (e.g., a symbolic boolean variable for every edge in a C# graph), and may have better performance in many cases.
CMap<T1, T2>
represents a total map from keys of type T1
to values of type T2
. When a key is not explicitly added to the map, the resulting value will be the Zen default value for the type T2
(e.g., 0
for integers, false
for booleans). CSet<T>
is simply implemented as a CMap<T, bool>
that says for each key, if the element is in the set. Any example use is shown below:
var x = Symbolic<int>();
var m1 = Symbolic<CMap<string, int>>();
var m2 = Symbolic<CMap<string, int>>();
var c1 = m1.Get("a") == Zen.If(x < 10, x + 1, x + 2);
var c2 = m2 == m1.Set("b", x);
var solution = And(c1, c2).Solve(); // x = 0, m1 = m2 = {"a" => 1, _ => 0}
Constant maps and sets have several limitations:
 Inequality may not always give the expected result, as the constant maps do not have a canonical representation.
 They can not be used as values in the
Map
,Set
, orSeq
types. This restriction may be relaxed in the future.
<a name="arrays"></a>
Fixed Length Arrays
Zen can model fixedlength arrays of symbolic values using the Array<T, TSize>
class. As an example:
var a = Zen.Symbolic<Array<int, _10>>(); // create a symbolic array of size 10
Zen<int>[] elements = a.ToArray(); // get the symbolic elements of the array
var solution = Zen.And(
elements.Aggregate(Zen.Plus) == 100,
a.All(x => Zen.And(x >= 1, x <= 20))).Solve(); // a = [8,6,13,16,14,15,5,13,5,5]
The type parameter TSize
specifies the size of the array. The types _1
through _100
are predefined in the library. To add a custom size, you can create a new struct following this naming convention:
struct _150 { }
<a name="stringsandsequences"></a>
Sequences, Strings, and Regular Expressions
Zen has a Seq<T>
type to represent arbitrarily large sequences of elements of type T
. As there is no complete decision procedure for sequences in constraint solvers, queries for sequences may not always terminate, and you may need to use a timeout. If this is not acceptable, you can always use FSeq
or FString
instead, which will model a finite sequence up to a given size. Sequences also support matching against regular expressions. As an example:
Regex<int> r = Regex.Star(Regex.Char(1)); // zero or more 1s in a Seq<int>
var s1 = Symbolic<Seq<int>>();
var s2 = Symbolic<Seq<int>>();
var c1 = s1.MatchesRegex(r);
var c2 = s1 != Seq.Empty<int>();
var c3 = Not(s2.MatchesRegex(r));
var c4 = s1.Length() == s2.Length();
var solution = And(c1, c2, c3, c4).Solve(); // s1 = [1], s2 = [0]
Zen supports the string
type for reasoning about unbounded strings (the string
type is implemented as a Seq<char>
). Strings also support matching regular expressions. Zen supports a limited subset of regex constructs currently  it supports anchors like $
and ^
but not any other metacharacters like \w,\s,\d,\D,\b
or backreferences \1
. As an example:
Regex<char> r1 = Regex.Parse("[09az]+");
Regex<char> r2 = Regex.Parse("(0.)*");
var s = Symbolic<string>();
var c1 = s.MatchesRegex(Regex.Intersect(r1, r2));
var c2 = s.Contains("a0b0c");
var c3 = s.Length() == new BigInteger(10);
var solution = And(c1, c2, c3).Solve(); // s = "020z0a0b0c"
<a name="customclassesandstructs"></a>
Custom classes and structs
Zen supports custom class
and struct
types with some limitations. It will attempt to model all public fields and properties. For these types to work, either (1) the class/struct must also have a default constructor and all properties must be allowed to be set, or (2) there must be a constructor with matching parameter names and types for all the public fields. For example, the following are examples that are and are not allowed:
// this will work because the fields are public
public class Point
{
public int X;
public int Y;
}
// this will work because the properties are public and can be set.
public class Point
{
public int X { get; set; }
public int Y { get; set; }
}
// this will NOT work because X can not be set.
public class Point
{
public int X { get; }
public int Y { get; set; }
}
// this will work as well since there is a constructor with the same parameter names.
// note that _z will not be modeled by Zen.
public class Point
{
public int X { get; }
public int Y { get; set; }
private int _z;
public Point(int x, int y)
{
this.X = x;
this.Y = y;
}
}
<a name="enums"></a>
Enumerated values
Enums in C# are just structs that wrap some backing type. Zen will model enums like any other struct. For example, Zen will model the following enum as a byte:
public enum Origin : byte
{
Egp,
Igp,
Incomplete,
}
By default, Zen does not constraint an enum value to only be one of the enumerated values  it can be any value allowed by the backing type (any value between 0 and 255 in this example instead of just the 3 listed). If you want to add a constraint to ensure the value is only one of those enumerated by the user, you write a function like the following to test if a value is one of those expected:
public Zen<bool> IsValidOrigin(Zen<Origin> origin)
{
return Zen.Or(Enum.GetValues<Origin>().Select(x => origin == x));
}
<a name="zenattributes"></a>
Zen Attributes
Zen provides two attributes to simplify the creation and manipulation of symbolic objects. The first attribute [ZenObject]
can be applied to classes or structs. It uses C# source generators to generate Get and With methods for all public fields and properties.
[ZenObject]
public class Point
{
public int X { get; set; }
public int Y { get; set; }
public static Zen<Point> Add(Zen<Point> p1, Zen<Point> p2)
{
return p1.WithX(p1.GetX() + p2.GetX()).WithY(p1.GetY() + p2.GetY());
}
}
Note that this requires C# 9.0 and .NET 6 or later to work. In addition, you must add the ZenLib.Generators nuget package to enable code generation. The other attribute supported is the ZenSize
attribute, which controls the size of a generated field in an object. For example, to fix the size of a FSeq
to 10:
public class Person
{
[ZenSize(depth: 10)]
public FSeq<string> Contacts { get; set; }
}
<a name="solverbackends"></a>
Solver Backends
Zen currently supports two solvers, one based on the Z3 SMT solver and another based on binary decision diagrams (BDDs). The Find
and Zen.Solve
APIs provide an option to select one of the two backends and will default to Z3 if left unspecified. The StateSetTransformer
API uses the BDD backend. The BDD backend has the limitation that it can only reason about boundedsize objects. This means that it can not reason about values with type BigInteger
or string
and will throw an exception. Similarly, these types along with FSeq<T>
, FSet<T>
, and Map<T1, T2>
can not be used with transformers.
<a name="solvertimeouts"></a>
Solver Timeouts
Zen supports terminating a call to the solver via the Solve
, Maximize
, Minimize
, and Find
methods for the Z3 backend. If the solver times out, it will raise a ZenSolverTimeoutException
. For example, you can try to find a solution within 100 milliseconds with the following:
var solverConfig = new ZenLib.Solver.SolverConfig
{
SolverType = SolverType.Z3,
SolverTimeout = TimeSpan.FromMilliseconds(100),
};
try
{
var solution = Zen.And(constraints).Solve(config: solverConfig);
...
}
catch (ZenSolverTimeoutException)
{
Console.WriteLine($"a timeout occurred.");
}
<a name="examplenetworkacls"></a>
Example: Network ACLs
As a more complete example, the following shows how to use Zen to encode and then verify a simplified network access control list that allows or blocks packets. ACLs generally consist of an ordered collection of matchaction rules that apply in sequence with the first applicable rule determining the fate of the packet. We can model an ACL with Zen:
// define a class to model Packets using public properties
[ZenObject]
public class Packet
{
// packet destination ip
public uint DstIp { get; set; }
// packet source ip
public uint SrcIp { get; set; }
}
// class representing an ACL with a list of prioritized rules.
public class Acl
{
public string Name { get; set; }
public AclLine[] Lines { get; set; }
public Zen<bool> Allowed(Zen<Packet> packet)
{
return Allowed(packet, 0);
}
// compute whether a packet is allowed by the ACL recursively
private Zen<bool> Allowed(Zen<Packet> packet, int lineNumber)
{
if (lineNumber >= this.Lines.Length)
{
return false; // Zen implicitly converts false to Zen<bool>
}
var line = this.Lines[lineNumber];
// if the current line matches, then return the action, otherwise continue to the next line
return If(line.Matches(packet), line.Action, this.Allowed(packet, lineNumber + 1));
}
}
// An ACL line that matches a packet.
public class AclLine
{
public bool Action { get; set; }
public uint DstIpLow { get; set; }
public uint DstIpHigh { get; set; }
public uint SrcIpLow { get; set; }
public uint SrcIpHigh { get; set; }
// a packet matches a line if it falls within the specified ranges.
public Zen<bool> Matches(Zen<Packet> packet)
{
return And(
packet.GetDstIp() >= this.DstIpLow,
packet.GetDstIp() <= this.DstIpHigh,
packet.GetSrcIp() >= this.SrcIpLow,
packet.GetSrcIp() <= this.SrcIpHigh);
}
}
<a name="implementation"></a>
Implementation Details
Zen builds an abstract syntax tree (AST) for a given user function and then leverages C#'s reflection capabilities to interpret, compile, and symbolically evaluate the AST.
<a name="contributing"></a>
Contributing
This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.opensource.microsoft.com.
When you submit a pull request, a CLA bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., status check, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.
This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact opencode@microsoft.com with any additional questions or comments.
Product  Versions Compatible and additional computed target framework versions. 

.NET  net5.0 was computed. net5.0windows was computed. net6.0 was computed. net6.0android was computed. net6.0ios was computed. net6.0maccatalyst was computed. net6.0macos was computed. net6.0tvos was computed. net6.0windows was computed. net7.0 was computed. net7.0android was computed. net7.0ios was computed. net7.0maccatalyst was computed. net7.0macos was computed. net7.0tvos was computed. net7.0windows was computed. net8.0 was computed. net8.0android was computed. net8.0browser was computed. net8.0ios was computed. net8.0maccatalyst was computed. net8.0macos was computed. net8.0tvos was computed. net8.0windows was computed. 
.NET Core  netcoreapp3.0 was computed. netcoreapp3.1 was computed. 
.NET Standard  netstandard2.1 is compatible. 
MonoAndroid  monoandroid was computed. 
MonoMac  monomac was computed. 
MonoTouch  monotouch was computed. 
Tizen  tizen60 was computed. 
Xamarin.iOS  xamarinios was computed. 
Xamarin.Mac  xamarinmac was computed. 
Xamarin.TVOS  xamarintvos was computed. 
Xamarin.WatchOS  xamarinwatchos was computed. 

.NETStandard 2.1
 DecisionDiagrams (>= 1.3.0)
 Microsoft.CSharp (>= 4.7.0)
 Microsoft.Z3 (>= 4.11.0)
 System.Collections.Immutable (>= 7.0.0)
 System.Dynamic.Runtime (>= 4.3.0)
NuGet packages
This package is not used by any NuGet packages.
GitHub repositories
This package is not used by any popular GitHub repositories.
Version  Downloads  Last updated 

3.1.6  352  10/23/2023 
3.1.5  181  8/30/2023 
3.1.4  196  8/28/2023 
3.1.3  249  7/14/2023 
3.1.2  345  2/28/2023 
3.1.1  534  9/22/2022 
3.1.0  422  9/8/2022 
3.0.0  391  8/25/2022 
2.3.0  443  8/12/2022 
2.2.9  381  8/12/2022 
2.2.8  432  8/11/2022 
2.2.7  425  8/8/2022 
2.2.6  385  8/4/2022 
2.2.5  433  7/27/2022 
2.2.4  519  5/31/2022 
2.2.3  417  5/20/2022 
2.2.2  503  4/14/2022 
2.2.1  454  4/8/2022 
2.2.0  446  4/7/2022 
2.1.9  461  3/24/2022 
2.1.8  438  3/10/2022 
2.1.7  442  3/5/2022 
2.1.6  434  3/3/2022 
2.1.5  431  3/2/2022 
2.1.4  449  2/23/2022 
2.1.3  424  2/18/2022 
2.1.2  429  2/14/2022 
2.1.1  420  2/14/2022 
2.1.0  438  2/11/2022 
2.0.0  434  2/9/2022 
1.3.2  462  1/30/2022 
1.3.1  313  1/5/2022 
1.3.0  371  11/9/2021 
1.2.9  368  10/28/2021 
1.2.8  380  10/19/2021 
1.2.7  318  10/18/2021 
1.2.6  480  10/17/2021 
1.2.5  334  10/16/2021 
1.2.4  339  10/15/2021 
1.2.3  355  10/11/2021 
1.2.2  368  10/8/2021 
1.2.1  324  10/6/2021 
1.2.0  310  10/5/2021 
1.1.9  355  8/31/2021 
1.1.8  336  7/21/2021 
1.1.7  352  7/15/2021 
1.1.6  368  6/3/2021 
1.1.5  615  1/5/2021 
1.1.4  482  12/16/2020 
1.1.3  404  10/13/2020 
1.1.2  430  10/7/2020 
1.1.1  486  10/2/2020 
1.1.0  432  9/29/2020 
1.0.9  428  9/25/2020 
1.0.8  457  9/23/2020 
1.0.7  513  9/17/2020 
1.0.6  531  9/17/2020 
1.0.5  886  7/15/2020 
1.0.4  548  6/14/2020 
1.0.3  565  6/6/2020 
1.0.2  471  5/6/2020 
1.0.1  473  5/6/2020 
1.0.0  494  5/6/2020 