20 using System.Collections.Generic;
38 Contract.Requires(ctx != null);
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
expr operator*(expr const &a, expr const &b)
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
expr operator>=(expr const &a, expr const &b)
expr operator<=(expr const &a, expr const &b)
RealSort MkRealSort()
Create a real sort.
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
expr operator+(expr const &a, expr const &b)
expr operator<(expr const &a, expr const &b)
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
expr operator>(expr const &a, expr const &b)
The main interaction with Z3 happens via the Context.
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Arithmetic expressions (int/real)
expr operator-(expr const &a)
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
expr operator/(expr const &a, expr const &b)
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
IntSort MkIntSort()
Create a new integer sort.