Skip to content

Operations

Jump to bottom
Ryan Beckett edited this page Jan 6, 2021 · 12 revisions

Contents

  1. Creating A Function
  2. Logical Operations
  3. Integer Operations
  4. Equality
  5. Option Operations
  6. List Operations
  7. Class And Struct Operations
  8. Tuple And ValueTuple Operations
  9. String And FiniteString Operations
  10. Implicit Conversions

Creating A Function

Zen offers two types of basic types: ZenFunction and ZenConstraint. The type ZenConstraint<T> is essentially equivalent to ZenFunction<T, bool> but provides a number of additional helper functions. A simple example of a ZenConstraint is shown below:

ZenConstraint<int, int> zc = new ZenConstraint<int, int>((x, y) => x + 3 > y);
var (x, y) = zc.Find().Value;

Assert.IsTrue(x + 3 > y);

To create a ZenConstraint one simply provides a callback function that takes Zen object arguments and returns a value of type Zen<bool>. The same example using a ZenFunction is shown below:

ZenFunction<int, int, bool> zf = new ZenFunction<int, int, bool>((x, y) => x + 3 > y);
var (x, y) = zf.Find((x, y, b) => b).Value;

Assert.IsTrue(x + 3 > y);

The primary difference is that ZenFunction requires a callback function to the Find function since the output type need not be bool.

Logical Operations

Zen supports several basic logical operators:

And: Logical conjunction of two boolean expressions

Zen<bool> And(Zen<bool> x, Zen<bool> y)

Or: Logical disjunction of two boolean expressions

Zen<bool> Or(Zen<bool> x, Zen<bool> y)

Not: Logical negation of a boolean expression

Zen<bool> Not(Zen<bool> x)

Implies: Logical implication of two boolean expressions

Zen<bool> Implies(Zen<bool> x, Zen<bool> y)

If<T>: An if-then-else ternary expression

Zen<T> If<T>(Zen<bool> guard, Zen<T> trueExpr, Zen<T> falseExpr)

Integer Operations

Zen works with the integral types byte, short, ushort, int, uint, long, ulong, and System.Numerics.BigInteger.

Out of the box, Zen also provides the types Int1, UInt1, Int2, UInt2, Int3, UInt3 ..., Int64, UInt64 as well as the types Int128, UInt128, Int256, UInt256.

You can also create a custom fixed-width integer of a given length. For example, to create a 65-bit integer, just add the following code:

    public class Int65 : IntN<Int65, Signed> 
    { 
        public override int Size { get { return 65; } } 
        public Int65(byte[] bytes) : base(bytes) { } 
        public Int65(long value) : base(value) { } 
    }

The library should take care of the rest. Or equivalently, for unsigned integer semantics.

    public class UInt65 : IntN<UInt65, Unsigned> 
    { 
        public override int Size { get { return 65; } } 
        public UInt65(byte[] bytes) : base(bytes) { } 
        public UInt65(long value) : base(value) { } 
    }

Zen overloads the integer operators: +, -, *, \, ~, |, &, <, <=, >, >=, == for each of these types with the single exception that the | and & operators will not work with the BigInteger type.

As a result of overloading these operators, you can write normal-looking arithmetic expressions over Zen values such as the following:

var zf = new ZenFunction<int, int, bool>((x, y) => x + y > 10);

Equality

Zen overloads the == operator for all supported types Zen<T>. It uses structural equality by recursively comparing the equality of all fields for objects, all values for lists, and so on.

// compares two lists for equality
var zf = new ZenFunction<IList<int>, IList<int>, bool>((l1, l2) => l1 == l2);

Option Operations

By default, all values in Zen are assumed to be non-nullable and the solver will not consider null to be a valid value. If you want to represent a potentially nullable value, you can use the Option<T> type. An option is simply a struct with two fields: a flag saying if the option has a value, and the underlying value. The operations defined on options are shown below:

Null<T>: Create a null value for a given option type of value T

Zen<Option<T>> Null<T>()

Some<T>: Create a non-null option value

Zen<Option<T>> Some<T>(Zen<T> expr)

TupleToOption<T>: Create an option from a flag and value. The flag is true if the option should be non-null.

Zen<Option<T>> TupleToOption<T>(Zen<bool> flag, Zen<T> value)

HasValue<T>: Check if an option has a value

Zen<bool> HasValue<T>(this Zen<Option<T>> expr)

Value<T>: Get the value out of an option. The value may be arbitrary if the option is null.

Zen<T> Value<T>(this Zen<Option<T>> expr)

ValueOrDefault<T>: Get the value out of an option or return a default if none.

Zen<T> ValueOrDefault<T>(this Zen<Option<T>> expr, Zen<T> deflt)

Select<T1, T2>: Map a function over the value inside of an option.

Zen<Option<T2>> Select<T1, T2>(this Zen<Option<T1>> expr, Func<Zen<T1>, Zen<T2>> function)

Where<T>: Filter the value in an option, possibly returning null.

Zen<Option<T>> Where<T>(this Zen<Option<T>> expr, Func<Zen<T>, Zen<bool>> function)

List Operations

Zen models lists but bounds their length to ensure that search remains decidable at all times. The default maximum list size is 5 but can be changed in calls to all ZenFunction methods such as Find. To use a list in Zen, you should use the IList<T> interface type rather than a concrete type. As an example consider the following code:

var zf = new ZenConstraint<IList<int>>(l => ...).Find();

When calling Find for this constraint, Zen will simply translate the input list l into an expression like the following:

Zen<ushort> length = Arbitrary<ushort>();
Zen<IList<int>> list0 = EmptyList<int>();
Zen<IList<int>> list1 = List(Arbitrary<int>());
Zen<IList<int>> list2 = List(Arbitrary<int>(), Arbitrary<int>());
Zen<IList<int>> list3 = List(Arbitrary<int>(), Arbitrary<int>(), Arbitrary<int>());
...

Zen<IList<int>> list = If(length == 0, list0, If(length == 1, list1, ...));

This models the possibility for a list to be any size less than or equal to the maximum size. The primary way to write functions over Zen lists is through recursion. This is done using the Case function. For example, consider the following code that is used to implement a list append operation:

public static Zen<IList<T>> Append<T>(this Zen<IList<T>> x, Zen<IList<T>> y)
{
    return x.Case(
        empty: y,
        cons: (hd, tl) => tl.Append(y).AddFront(hd));
}

The function takes two lists x and y and appends y to the end of x. To do this, it calls the Case function on x. This splits the list into two possibilities in the style of functional programming languages. The first case is when x is empty. In this case, we simply return y. The second case is when x has a first element hd, which is proceeded by another list of remaining elements tl. In this case, the function recursively appends y to tl and then adds hd to the front of the result and returns this list.

This recursive style of processing lists can be used to create new list-processing functions. However, the library also already has many such helper functions already implemented (listed below) using the Case mechanism.

EmptyList<T>: Get the empty list

Zen<IList<T>> EmptyList<T>()

AddBack<T>: Add an element to the end of a list.

Zen<IList<T>> AddBack<T>(this Zen<IList<T>> listExpr, Zen<T> valueExpr)

AddFront<T>: Add an element to the front of a list.

Zen<IList<T>> AddFront<T>(this Zen<IList<T>> listExpr, Zen<T> valueExpr)

RemoveFirst<T>: Remove the first occurrence of a value from a list.

Zen<IList<T>> RemoveFirst<T>(this Zen<IList<T>> listExpr, Zen<T> valueExpr)

RemoveAll<T>: Remove all the occurrences of a value from a list.

Zen<IList<T>> RemoveAll<T>(this Zen<IList<T>> listExpr, Zen<T> valueExpr)

Duplicates<T>: Count the number of copies of a value in a list.

Zen<ushort> Duplicates<T>(this Zen<IList<T>> listExpr, Zen<T> valueExpr)

Select<T1, T2>: Map a callback function over a list.

Zen<IList<T2>> Select<T1, T2>(this Zen<IList<T1>> listExpr, Func<Zen<T1>, Zen<T2>> function)

Where<T>: Filter elements from a list with a function.

Zen<IList<T>> Where<T>(this Zen<IList<T>> listExpr, Func<Zen<T>, Zen<bool>> predicate)

Find<T>: Find an element in the list that satisfies a predicate, or return null if there is no such value.

Zen<Option<T>> Find<T>(this Zen<IList<T>> listExpr, Func<Zen<T>, Zen<bool>> predicate)

Length<T>: Get the length of the list.

Zen<ushort> Length<T>(this Zen<IList<T>> listExpr)

Contains<T>: Check if a list contains an element.

Zen<bool> Contains<T>(this Zen<IList<T>> listExpr, Zen<T> element)

Append<T>: Append a second list to the end of a first list.

Zen<IList<T>> Append<T>(this Zen<IList<T>> expr1, Zen<IList<T>> expr2)

IsEmpty<T>: Check if a list is empty.

Zen<bool> IsEmpty<T>(this Zen<IList<T>> expr)

Singleton<T>: Create a list with a single value.

Zen<IList<T>> Singleton<T>(this Zen<T> element)

List<T>: Create a list with any number of elements.

Zen<IList<T>> List<T>(params Zen<T>[] elements)

Reverse: Return a reversed list.

Zen<IList<T>> Reverse<T>(this Zen<IList<T>> expr)

Fold<T1, T2>: Reduce a function over a list, accumulating some value.

Zen<T2> Fold<T1, T2>(this Zen<IList<T1>> expr, Zen<T2> acc, Func<Zen<T1>, Zen<T2>, Zen<T2>> function)

Any<T>: Check if any value in the list satisfies a predicate.

Zen<bool> Any<T>(this Zen<IList<T>> expr, Func<Zen<T>, Zen<bool>> predicate)

All<T>: Check if all values in the list satisfies a predicate.

Zen<bool> All<T>(this Zen<IList<T>> expr, Func<Zen<T>, Zen<bool>> predicate)

Take<T>: Take some number of elements from a list.

Zen<IList<T>> Take<T>(this Zen<IList<T>> expr, Zen<ushort> numElements)

TakeWhile<T>: Take elements from a list while a predicate is true.

Zen<IList<T>> TakeWhile<T>(this Zen<IList<T>> expr, Func<Zen<T>, Zen<bool>> predicate)

Drop<T>: Drop some number of elements from a list.

Zen<IList<T>> Drop<T>(this Zen<IList<T>> expr, Zen<ushort> numElements)

Drop elements from a list while a predicate is true.

Zen<IList<T>> DropWhile<T>(this Zen<IList<T>> expr, Func<Zen<T>, Zen<bool>> predicate)

SplitAt<T>: Split a list at a given index.

Zen<Tuple<IList<T>, IList<T>>> SplitAt<T>(this Zen<IList<T>> expr, Zen<ushort> index)

At<T>: Get the element at a given list index.

Zen<Option<T>> At<T>(this Zen<IList<T>> listExpr, Zen<ushort> index)

IndexOf<T>: Get index of the first occurrence of a value in a list.

Zen<Option<ushort>> IndexOf<T>(this Zen<IList<T>> listExpr, Zen<T> value)

IsSorted<T>: Check if a list is sorted. Only works for integral types.

Zen<bool> IsSorted<T>(this Zen<IList<T>> expr)

Sort<T>: Sort a list. Only works for integral types.

Zen<IList<T>> Sort<T>(this Zen<IList<T>> expr)

Insert<T>: Insert an element into a sorted list in sorted order. Only works for integral types.

Zen<IList<T>> Insert<T>(Zen<T> element, Zen<IList<T>> expr)

Class And Struct Operations

Zen supports user-defined class and struct so long as the type is just plain old data. That is, all fields and properties must be public and properties must have both get and set operations. Finally, the class or struct must have a default constructor. As an example, a valid 2D point class is shown below:

public struct Point2D
{
    public int X { get; set; }
    public int Y { get; set; }
}

Classes can also contain fields of other types so long as that type is also supported by Zen. For example you can have fields with type IList<Point2D>. One restriction is that Zen will not currently work with recursive types, though we may lift this restriction in the future. For instance, the following will not work:

public class TreeNode 
{
    public int Data;
    public TreeNode Left;
    public TreeNode Right;
}

There are three simple ways to interact with classes and structs in Zen:

GetField<T1, T2>: Gets a field of type T2 from an object of type T1.

Zen<T2> GetField<T1, T2>(this Zen<T1> expr, string fieldName)

WithField<T1, T2>: Returns a new object of type T1 that returns a copy of the object with a single field updated.

Zen<T1> WithField<T1, T2>(this Zen<T1> expr, string fieldName, Zen<T2> fieldValue)

Create<T1>: Creates a new object of type T from the supplied fields and values. Each value must be a Zen expression of the correct type.

Zen<T> Create<T>(params (string, object)[] fields)

One thing to note is that the types to these functions must be supplied to GetField and Create since they can not be inferred from the values of strings, which are known only at runtime. As a result, the type checking will occur at runtime for these methods. As a consequence, it is often a good idea to write extension methods to make creating, updating, and getting fields from objects easier. For instance, for the Point2D class, we could write the following:

public static class Point2DExtensions
{
    public static Zen<int> GetX(this Zen<Point2D> p) => p.GetField<Point2D, int>("x");
    public static Zen<int> GetY(this Zen<Point2D> p) => p.GetField<Point2D, int>("y");
    public static Zen<Point2D> SetX(this Zen<Point2D> p, Zen<int> x) => p.WithField("x", x);
    public static Zen<Point2D> SetY(this Zen<Point2D> p, Zen<int> y) => p.WithField("y", y);
}

Tuple And ValueTuple Operations

Zen supports the types Tuple<T1, T2> as well as (T1, T2) but only for tuples of size 2.

Tuple<T1, T2>: Create a new tuple from its two components

Zen<Tuple<T1, T2>> Tuple<T1, T2>(Zen<T1> expr1, Zen<T2> expr2)

ValueTuple<T1, T2>: Create a new value tuple from its two components

Zen<ValueTuple<T1, T2>> ValueTuple<T1, T2>(Zen<T1> expr1, Zen<T2> expr2)

Item1<T1, T2>: Gets the first component from a tuple.

Zen<T1> Item1<T1, T2>(this Zen<Tuple<T1, T2>> expr)

Item2<T1, T2>: Gets the second component from a tuple.

Zen<T2> Item2<T1, T2>(this Zen<Tuple<T1, T2>> expr)

Item1<T1, T2>: Gets the first component from a value tuple.

Zen<T1> Item1<T1, T2>(this Zen<ValueTuple<T1, T2>> expr)

Item2<T1, T2>: Gets the second component from a value tuple.

Zen<T2> Item2<T1, T2>(this Zen<ValueTuple<T1, T2>> expr)

String And FiniteString Operations

Zen supports the built in string type string as well as a library-defined type called FiniteString. The main difference between the two is that string will be treated as an arbitrary-sized string while FiniteString is bounded to a particular length similar to lists. There may be some problems for which solvers can not search exhaustively for string but can for FiniteString. Both data types support a similar set of operations, so the operations for string are shown below:

Concat: Concatenates two strings together. Note that strings also overload the + operator for concatenation.

Zen<string> Concat(Zen<string> expr1, Zen<string> expr2)

EndsWith: Checks if a string ends with a substring.

Zen<bool> EndsWith(this Zen<string> str, Zen<string> substr)

StartsWith: Checks if a string starts with a substring.

Zen<bool> StartsWith(this Zen<string> str, Zen<string> substr)

Contains: Checks if a string contains a substring.

Zen<bool> Contains(this Zen<string> str, Zen<string> substr)

ReplaceFirst: Replaces the first instance of a substring with a replacement string.

Zen<string> ReplaceFirst(this Zen<string> str, Zen<string> substr, Zen<string> replace)

Substring: Gets a substring of a string.

Zen<string> Substring(this Zen<string> str, Zen<BigInteger> offset, Zen<BigInteger> length)

At: Gets a character at a given string index.

Zen<string> At(this Zen<string> str, Zen<BigInteger> index)

Length: Gets the length of a string.

Zen<BigInteger> Length(this Zen<string> str)

IndexOf: Gets the index of a substring, potentially starting from some offset.

Zen<BigInteger> IndexOf(this Zen<string> str, Zen<string> sub)
Zen<BigInteger> IndexOf(this Zen<string> str, Zen<string> sub, Zen<BigInteger> offset)

Implicit Conversions

Any constant C# value can be converted to a Zen expression either explicitly or implicitly:

Zen<int> y = Constant(10);                  // explicit conversion
Zen<bool> b = true;                         // implicit boolean conversion
Zen<byte> x = 10;                           // implicit conversions from int to byte to Zen<byte>
Zen<IList<int>> l = new List<int> { 1, 2 }; // implicit list conversion
Zen<bool> even = IsEven(100);               // argument is implicitly converted to Zen<int>

public Zen<bool> IsEven(Zen<int> i)
{
    return i & 1 == 0;                      // constant 1 implicitly converted to Zen<int>
}

Microsoft Research

Clone this wiki locally