All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type |
Method and Description |
static SMTTerm |
and(List<SMTTerm> args) |
SMTTerm |
and(SMTTerm right) |
SMTTerm |
binOp(SMTTermBinOp.Op op,
SMTTerm f) |
SMTTerms |
c(SMTTerm f) |
static SMTTerm |
call(SMTFunction func) |
static SMTTerm |
call(SMTFunction func,
List<? extends SMTTerm>... args) |
static SMTTerm |
call(SMTFunction func,
List<? extends SMTTerm> args,
SMTTerm... moreArgs) |
static SMTTerm |
call(SMTFunction func,
List<SMTTerm> args) |
static SMTTerm |
call(SMTFunction func,
SMTTerm... args) |
static SMTTerm |
call(SMTFunction func,
SMTTerm arg) |
static SMTTerm |
call(SMTFunction func,
SMTTerm[]... args) |
static SMTTerm |
call(SMTFunction func,
SMTTerms t) |
SMTTerm |
concat(SMTTerm f) |
abstract SMTTerm |
copy() |
private SMTTerm |
defaultMultOp(SMTTermMultOp.Op op,
SMTTerm f) |
SMTTerm |
div(SMTTerm right) |
static SMTTerm |
equal(List<SMTTerm> args) |
SMTTerm |
equal(SMTTerm right) |
SMTTerm |
exists(List<SMTTermVariable> bindVars) |
SMTTerm |
exists(List<SMTTermVariable> bindVars,
List<List<SMTTerm>> pats) |
SMTTerm |
exists(List<SMTTermVariable> bindVars1,
List<SMTTermVariable> bindVars2,
List<List<SMTTerm>> pats) |
static SMTTerm |
exists(List<SMTTermVariable> bindVars,
SMTTerm subForm,
List<SMTTerm> pats) |
SMTTerm |
exists(SMTTermVariable var) |
SMTTerm |
exists(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
exists(SMTTermVariable bindVar,
SMTTerm subForm,
List<SMTTerm> pats) |
static SMTTerm |
exists(SMTTermVariable bindVar,
SMTTerm subForm,
SMTTerm pat) |
SMTTerm |
forall(List<SMTTermVariable> bindVars) |
SMTTerm |
forall(List<SMTTermVariable> bindVars,
List<List<SMTTerm>> pats) |
SMTTerm |
forall(List<SMTTermVariable> bindVars1,
List<SMTTermVariable> bindVars2,
List<List<SMTTerm>> pats) |
SMTTerm |
forall(List<SMTTermVariable> bindVars1,
List<SMTTermVariable> bindVars2,
SMTTerm pat) |
static SMTTerm |
forall(List<SMTTermVariable> bindVars,
SMTTerm subForm,
List<SMTTerm> pats) |
SMTTerm |
forall(SMTTerms terms) |
SMTTerm |
forall(SMTTerms terms,
SMTTerm pat) |
SMTTerm |
forall(SMTTermVariable var) |
SMTTerm |
forall(SMTTermVariable var,
List<List<SMTTerm>> pats) |
SMTTerm |
forall(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
forall(SMTTermVariable bindVar,
SMTTerm subForm,
List<SMTTerm> pats) |
String |
getComment() |
List<SMTTermVariable> |
getEQVars() |
List<SMTTermVariable> |
getQuantVars() |
List<SMTTerm> |
getSubs() |
List<SMTTermVariable> |
getUQVars() |
List<SMTTermVariable> |
getVars() |
SMTTerm |
gt(SMTTerm right) |
SMTTerm |
gte(SMTTerm right) |
SMTTerm |
iff(SMTTerm right) |
static SMTTerm |
implies(List<SMTTerm> args) |
SMTTerm |
implies(SMTTerm right) |
abstract SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
isCons() |
static SMTTerm |
ite(SMTTerm condition,
SMTTerm trueCase,
SMTTerm falseCase) |
SMTTerm |
lt(SMTTerm right) |
SMTTerm |
lte(SMTTerm right) |
SMTTerm |
minus(SMTTerm right) |
SMTTerm |
mul(SMTTerm right) |
SMTTerm |
multOp(SMTTermMultOp.Op op,
SMTTerm t) |
SMTTerm |
not() |
static SMTTerm |
not(SMTTerm subForm) |
static SMTTerm |
number(int n) |
static SMTTerm |
number(int n,
int bitSize) |
abstract boolean |
occurs(SMTTermVariable a) |
abstract boolean |
occurs(String id) |
static SMTTerm |
or(List<SMTTerm> args) |
SMTTerm |
or(SMTTerm right) |
SMTTerm |
plus(SMTTerm right) |
SMTTerm |
quant(SMTTermQuant.Quant quant,
List<SMTTermVariable> bindVars) |
SMTTerm |
quant(SMTTermQuant.Quant quant,
List<SMTTermVariable> bindVars,
List<List<SMTTerm>> pats) |
SMTTerm |
rem(SMTTerm right) |
abstract SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setComment(String comment) |
SMTTerm |
sign(boolean pol) |
abstract SMTSort |
sort() |
abstract SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
abstract SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerms |
terms() |
static SMTTerms |
terms(List<SMTTerm> terms) |
List<SMTTerm> |
toList() |
static <T> List<T> |
toList(T e) |
String |
toString() |
String |
toString(int nestPos) |
SMTTerm |
unaryOp(SMTTermUnaryOp.Op op) |