- abs() - Method in class de.uni_freiburg.informatik.ultimate.logic.Rational
-
Compute the absolute of this rational.
- add(Rational) - Method in class de.uni_freiburg.informatik.ultimate.logic.MutableRational
-
Add the rational other to this rational.
- add(Rational) - Method in class de.uni_freiburg.informatik.ultimate.logic.Rational
-
Return a new rational representing this + other
.
- addmul(Rational, Rational) - Method in class de.uni_freiburg.informatik.ultimate.logic.MutableRational
-
Computes this += (fac1*fac2)
.
- addmul(Rational, BigInteger) - Method in class de.uni_freiburg.informatik.ultimate.logic.MutableRational
-
Computes this += (fac1*fac2)
.
- addmul(Rational, Rational) - Method in class de.uni_freiburg.informatik.ultimate.logic.Rational
-
Computes this + (fac1*fac2)
.
- addSubstitutions(Map<TermVariable, Term>) - Method in class de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet
-
Add user defined substitutions.
- and(Script, Term...) - Static method in class de.uni_freiburg.informatik.ultimate.logic.Util
-
Return slightly simplified version of (and subforms).
- annotate(Term, Annotation...) - Method in class de.uni_freiburg.informatik.ultimate.logic.LoggingScript
-
- annotate(Term, Annotation...) - Method in class de.uni_freiburg.informatik.ultimate.logic.NoopScript
-
- annotate(Term, Annotation...) - Method in interface de.uni_freiburg.informatik.ultimate.logic.Script
-
Annotate a term.
- AnnotatedTerm - Class in de.uni_freiburg.informatik.ultimate.logic
-
Representation of annotated terms in SMTLIB 2.
- Annotation - Class in de.uni_freiburg.informatik.ultimate.logic
-
Representation of an annotation in a formula.
- Annotation(String, Object) - Constructor for class de.uni_freiburg.informatik.ultimate.logic.Annotation
-
- append(Appendable, Term) - Method in class de.uni_freiburg.informatik.ultimate.logic.PrintTerm
-
Convert a term into an appendable.
- append(Appendable, Sort) - Method in class de.uni_freiburg.informatik.ultimate.logic.PrintTerm
-
Convert a sort into an appendable.
- append(Appendable, Object[]) - Method in class de.uni_freiburg.informatik.ultimate.logic.PrintTerm
-
Append an s-expression.
- ApplicationTerm - Class in de.uni_freiburg.informatik.ultimate.logic
-
Represents a function application term.
- assertTerm(Term) - Method in class de.uni_freiburg.informatik.ultimate.logic.LoggingScript
-
- assertTerm(Term) - Method in class de.uni_freiburg.informatik.ultimate.logic.NoopScript
-
- assertTerm(Term) - Method in interface de.uni_freiburg.informatik.ultimate.logic.Script
-
Assert a Boolean term into the solver.
- assertTerm(Term) - Method in class de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol
-
- Assignments - Class in de.uni_freiburg.informatik.ultimate.logic
-
Class used as a response to get-assignments.
- Assignments(Map<String, Boolean>) - Constructor for class de.uni_freiburg.informatik.ultimate.logic.Assignments
-
Construct a new assignment.
- ASSOCMASK - Static variable in class de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol
-