3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-03 09:14:47 -08:00
parent ee18c5070c
commit 811cd9d48d

View file

@ -200,6 +200,11 @@ namespace Microsoft.Z3
/// <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)