search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.4k stars 1.47k forks source link

Define generic datatypes in Z3 C# API #1719

Closed ionuttamas closed 6 years ago

ionuttamas commented 6 years ago

I want to declare a generic data structure using C# API (a simple generic wrapper) similar to:

public class Wrapper<T> 
{
   public T Element {get; set;}
}

(declare-datatypes (T) ((Wrapper nil (Element T))))

  1. How can I do that in C#?

    1. How can I make an instantiation providing a specific type like:

    (declare-const instance (Wrapper Int))

NikolajBjorner commented 6 years ago
  1. You can't do generic sorts in C#, but you can create a factory method that produces such a sort per instance.
  2. Correct, you apply the Wrapper sort constructor to the parametric sorts when using SMT-LIB. For more details see the SMT-LIB2 spec.