public abstract class SMTTerm
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SMTTerm.False |
static class |
SMTTerm.True |
Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
comment |
static SMTTerm |
FALSE |
static SMTTerm |
TRUE |
SMTTerm |
upp |
Constructor and Description |
---|
SMTTerm() |
Modifier and Type | Method and Description |
---|---|
static SMTTerm |
and(java.util.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,
java.util.List<? extends SMTTerm>... args) |
static SMTTerm |
call(SMTFunction func,
java.util.List<? extends SMTTerm> args,
SMTTerm... moreArgs) |
static SMTTerm |
call(SMTFunction func,
java.util.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(java.util.List<SMTTerm> args) |
SMTTerm |
equal(SMTTerm right) |
SMTTerm |
exists(java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
exists(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
exists(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
static SMTTerm |
exists(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
exists(SMTTermVariable var) |
SMTTerm |
exists(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
exists(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
static SMTTerm |
exists(SMTTermVariable bindVar,
SMTTerm subForm,
SMTTerm pat) |
SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
SMTTerm pat) |
static SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
forall(SMTTerms terms) |
SMTTerm |
forall(SMTTerms terms,
SMTTerm pat) |
SMTTerm |
forall(SMTTermVariable var) |
SMTTerm |
forall(SMTTermVariable var,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
forall(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
forall(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
java.lang.String |
getComment() |
java.util.List<SMTTermVariable> |
getEQVars() |
java.util.List<SMTTermVariable> |
getQuantVars() |
java.util.List<SMTTerm> |
getSubs() |
java.util.List<SMTTermVariable> |
getUQVars() |
java.util.List<SMTTermVariable> |
getVars() |
SMTTerm |
gt(SMTTerm right) |
SMTTerm |
gte(SMTTerm right) |
SMTTerm |
iff(SMTTerm right) |
static SMTTerm |
implies(java.util.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(java.lang.String id) |
static SMTTerm |
or(java.util.List<SMTTerm> args) |
SMTTerm |
or(SMTTerm right) |
SMTTerm |
plus(SMTTerm right) |
SMTTerm |
quant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
quant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
rem(SMTTerm right) |
abstract SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setComment(java.lang.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(java.util.List<SMTTerm> terms) |
java.util.List<SMTTerm> |
toList() |
static <T> java.util.List<T> |
toList(T e) |
java.lang.String |
toString() |
java.lang.String |
toString(int nestPos) |
SMTTerm |
unaryOp(SMTTermUnaryOp.Op op) |
protected java.lang.String comment
public SMTTerm upp
public static final SMTTerm FALSE
public static final SMTTerm TRUE
public abstract boolean occurs(SMTTermVariable a)
public abstract boolean occurs(java.lang.String id)
public abstract SMTSort sort()
public abstract SMTTerm substitute(SMTTermVariable a, SMTTerm b)
public abstract SMTTerm replace(SMTTermCall a, SMTTerm b)
public abstract SMTTerm instantiate(SMTTermVariable a, SMTTerm b)
public abstract SMTTerm copy()
public java.lang.String getComment()
public void setComment(java.lang.String comment)
public java.util.List<SMTTermVariable> getQuantVars()
public java.util.List<SMTTermVariable> getUQVars()
public java.util.List<SMTTermVariable> getEQVars()
public java.util.List<SMTTermVariable> getVars()
public java.util.List<SMTTerm> getSubs()
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String toString(int nestPos)
public static SMTTerm call(SMTFunction func, java.util.List<SMTTerm> args)
public static SMTTerm call(SMTFunction func, SMTTerms t)
public static SMTTerm call(SMTFunction func, SMTTerm... args)
public static SMTTerm call(SMTFunction func, java.util.List<? extends SMTTerm> args, SMTTerm... moreArgs)
public static SMTTerm call(SMTFunction func, SMTTerm[]... args)
public static SMTTerm call(SMTFunction func, java.util.List<? extends SMTTerm>... args)
public static SMTTerm call(SMTFunction func, SMTTerm arg)
public static SMTTerm call(SMTFunction func)
public static SMTTerm forall(java.util.List<SMTTermVariable> bindVars, SMTTerm subForm, java.util.List<SMTTerm> pats)
public static SMTTerm forall(SMTTermVariable bindVar, SMTTerm subForm, java.util.List<SMTTerm> pats)
public static SMTTerm exists(java.util.List<SMTTermVariable> bindVars, SMTTerm subForm, java.util.List<SMTTerm> pats)
public static SMTTerm exists(SMTTermVariable bindVar, SMTTerm subForm, SMTTerm pat)
public static SMTTerm exists(SMTTermVariable bindVar, SMTTerm subForm, java.util.List<SMTTerm> pats)
public static SMTTerm number(int n)
public static SMTTerm number(int n, int bitSize)
public SMTTerms terms()
public SMTTerm unaryOp(SMTTermUnaryOp.Op op)
public SMTTerm sign(boolean pol)
public SMTTerm not()
public SMTTerm multOp(SMTTermMultOp.Op op, SMTTerm t)
private SMTTerm defaultMultOp(SMTTermMultOp.Op op, SMTTerm f)
op
- f
- public SMTTerm binOp(SMTTermBinOp.Op op, SMTTerm f)
public SMTTerm quant(SMTTermQuant.Quant quant, java.util.List<SMTTermVariable> bindVars)
public SMTTerm quant(SMTTermQuant.Quant quant, java.util.List<SMTTermVariable> bindVars, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTerm forall(java.util.List<SMTTermVariable> bindVars)
public SMTTerm forall(SMTTermVariable var)
public SMTTerm forall(SMTTermVariable var, SMTTerm pat)
public SMTTerm forall(SMTTermVariable var, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTerm forall(java.util.List<SMTTermVariable> bindVars, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTerm forall(java.util.List<SMTTermVariable> bindVars1, java.util.List<SMTTermVariable> bindVars2, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTerm forall(java.util.List<SMTTermVariable> bindVars1, java.util.List<SMTTermVariable> bindVars2, SMTTerm pat)
public SMTTerm exists(SMTTermVariable var)
public SMTTerm exists(SMTTermVariable var, SMTTerm pat)
public SMTTerm exists(java.util.List<SMTTermVariable> bindVars)
public SMTTerm exists(java.util.List<SMTTermVariable> bindVars, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTerm exists(java.util.List<SMTTermVariable> bindVars1, java.util.List<SMTTermVariable> bindVars2, java.util.List<java.util.List<SMTTerm>> pats)
public java.util.List<SMTTerm> toList()
public static <T> java.util.List<T> toList(T e)
public boolean isCons()