Z3
BoolExpr.cs
Go to the documentation of this file.
1/*++
2Copyright (<c>) 2012 Microsoft Corporation
3
4Module Name:
5
6 BoolExpr.cs
7
8Abstract:
9
10 Z3 Managed API: Boolean Expressions
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21using System.Collections.Generic;
22using System.Linq;
23using System.Text;
24
25
26namespace 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}
Boolean expressions
Definition: BoolExpr.cs:32
static BoolExpr operator|(BoolExpr a, BoolExpr b)
Disjunction of Boolean expressions
Definition: BoolExpr.cs:40
static BoolExpr operator&(BoolExpr a, BoolExpr b)
Conjunction of Boolean expressions
Definition: BoolExpr.cs:43
static BoolExpr operator!(BoolExpr a)
Negation
Definition: BoolExpr.cs:49
static BoolExpr operator^(BoolExpr a, BoolExpr b)
Xor of Boolean expressions
Definition: BoolExpr.cs:46
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:923
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).
Definition: Context.cs:868
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
Definition: Context.cs:979
Expressions are terms.
Definition: Expr.cs:31