add example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Mar 3, 2022 · 811cd9d · 811cd9d
1 parent ee18c50
commit 811cd9d
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs
@@ -200,6 +200,11 @@ public void Add(IEnumerable<Z3_ast> constraints)
 
         /// <summary>
         /// Add constraints to ensure the function f can only be injective.
+        /// Example:
+        /// for function f : D1 x D2 -> R
+        /// assert axioms
+        ///   forall (x1 : D1, x2 : D2) x1 = inv1(f(x1,x2))
+        ///   forall (x1 : D1, x2 : D2) x2 = inv2(f(x1,x2))
         /// </summary>
         /// <param name="f"></param>
         public void AssertInjective(Z3_func_decl f)