19using System.Diagnostics;
21using System.Collections.Generic;
38 Debug.Assert(ctx !=
null);
Arithmetic expressions (int/real)
static BoolExpr operator>(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
static ArithExpr operator*(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
static BoolExpr operator>=(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
static ArithExpr operator+(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
static BoolExpr operator<(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
static ArithExpr operator-(ArithExpr a)
Operator overloading for arithmetical operator
static ArithExpr operator/(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical division operator (over reals)
static BoolExpr operator<=(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
The main interaction with Z3 happens via the Context.
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
RealSort MkRealSort()
Create a real sort.
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
IntSort MkIntSort()
Create a new integer sort.
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2