Z3 |

BoolExpr.cs
Go to the documentation of this file.
1/*++
2 Copyright (<c>) 2012 Microsoft Corporation
3
4 Module Name:
5
6 BoolExpr.cs
7
8 Abstract:
9
10 Z3 Managed API: Boolean Expressions
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16 Notes:
17
18--*/
19 using System.Diagnostics;
20 using System;
21 using System.Collections.Generic;
22 using System.Linq;
23 using System.Text;
24
25
26 namespace Microsoft.Z3
27{
31 public class BoolExpr : Expr
32 {
33 #region Internal
35 internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
36 #endregion
37
38 #region Operators
40 public static BoolExpr operator|(BoolExpr a, BoolExpr b) { return a.Context.MkOr(a, b); }
41
43 public static BoolExpr operator &(BoolExpr a, BoolExpr b) { return a.Context.MkAnd(a, b); }
44
46 public static BoolExpr operator ^(BoolExpr a, BoolExpr b) { return a.Context.MkXor(a, b); }
47
49 public static BoolExpr operator !(BoolExpr a) { return a.Context.MkNot(a); }
50
51 #endregion
52 }
53}
Microsoft.Z3.BoolExpr
Boolean expressions
Definition: BoolExpr.cs:32
Microsoft.Z3.BoolExpr.operator|
static BoolExpr operator|(BoolExpr a, BoolExpr b)
Disjunction of Boolean expressions
Definition: BoolExpr.cs:40
Microsoft.Z3.BoolExpr.operator&
static BoolExpr operator&(BoolExpr a, BoolExpr b)
Conjunction of Boolean expressions
Definition: BoolExpr.cs:43
Microsoft.Z3.BoolExpr.operator!
static BoolExpr operator!(BoolExpr a)
Negation
Definition: BoolExpr.cs:49
Microsoft.Z3.BoolExpr.operator^
static BoolExpr operator^(BoolExpr a, BoolExpr b)
Xor of Boolean expressions
Definition: BoolExpr.cs:46
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:923
Microsoft.Z3.Context.MkNot
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition: Context.cs:868
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:979
Microsoft.Z3.Expr
Expressions are terms.
Definition: Expr.cs:31
Microsoft.Z3
Definition: AlgebraicNum.cs:27