BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
BoolExpr MkOr(params BoolExpr[] t)
Create an expression representing t[0] or t[1] or ....
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
The main interaction with Z3 happens via the Context.
BoolExpr MkNot(BoolExpr a)
Mk an expression representing not(a).