F-Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

F

factory - Variable in class org.smtlib.sexpr.Parser: The (common) factory used to generate objects
Factory - Class in org.smtlib.impl: Implements a factory for SMT-LIB expressions using the standard concrete syntax.
Factory - Class in org.smtlib.sexpr: This is the factory for classes that are part of this particular concrete representation of SMT-LIB syntax: Parser, Printer, Source for parsers.
Factory() - Constructor for class org.smtlib.sexpr.Factory
Factory(SMT.Configuration) - Constructor for class org.smtlib.impl.Factory
Factory(SMT.Configuration) - Constructor for class org.smtlib.impl.Response.Factory
FALSE - Static variable in class org.smtlib.Utils: Symbol constant for boolean false.
family() - Method in class org.smtlib.impl.Sort.Application
family() - Method in interface org.smtlib.ISort.IApplication: The head identifier of the sort expression
family(String) - Static method in class org.smtlib.SolverCapabilities: The family name: the solver name before the first '-' followed by a digit; null if there is none
Family(IExpr.IIdentifier, IExpr.INumeral, List<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.impl.Sort.Family: Creates a sort family with the given identifier, arity, and attributes (null or empty if none).
fcn(IExpr.IQualifiedIdentifier, List<IExpr>) - Method in interface org.smtlib.IExpr.IFactory: Creates a function expression (perhaps with an empty argument list).
fcn(IExpr.IQualifiedIdentifier, List<IExpr>) - Method in class org.smtlib.impl.Factory
fcn(IExpr.IQualifiedIdentifier, IExpr...) - Method in interface org.smtlib.IExpr.IFactory: Creates a function expression (perhaps with an empty argument list).
fcn(IExpr.IQualifiedIdentifier, IExpr...) - Method in class org.smtlib.impl.Factory
FcnExpr(IExpr.IQualifiedIdentifier, List<IExpr>) - Constructor for class org.smtlib.impl.SMTExpr.FcnExpr: Creates a function application from the given identifier and argument list.
fcnName - Variable in class org.smtlib.command.C_declare_fun: The name of the function being declared
fcnName - Variable in class org.smtlib.command.C_define_fun: The name of the function being defined
FcnSort(ISort) - Constructor for class org.smtlib.impl.Sort.FcnSort: Creates a zero-argument (nullary) function sort with the given result sort.
FcnSort(ISort[], ISort) - Constructor for class org.smtlib.impl.Sort.FcnSort: Creates a function sort with the given argument sorts and result sort.
filename - Variable in class org.smtlib.impl.Script: The filename of the script file
filename() - Method in interface org.smtlib.ICommand.IScript
filename() - Method in class org.smtlib.impl.Script: The filename of the script file
files - Variable in class org.smtlib.SMT.Configuration: The files of SMT-LIB commands to process; if null or empty then the standard input is used
find(String) - Static method in enum class org.smtlib.SMT.Configuration.SMTLIB: Returns the SMTLIB constant whose id equals the given string, or null if none matches.
findCommand(String) - Method in interface org.smtlib.ICommand.IFinder: This method finds a class that implements the ICommand interface for the given class name
findLogic(String, IPos) - Method in class org.smtlib.Utils: Reads a logic file, parses it, validates the name, and checks the version.
findTheory(String, String) - Method in class org.smtlib.Utils: Reads a theory file, returning the S-expression that it holds.
finishPipelined() - Method in class org.smtlib.AbstractSolver: At the end of a pipelined run: waits briefly for output still arriving after the last response, and reports any as out of step
first - Variable in class org.smtlib.impl.Response.Pair
first() - Method in class org.smtlib.impl.Response.Pair
first() - Method in interface org.smtlib.IResponse.IPair
FLOAT128 - Static variable in class org.smtlib.Utils
FLOAT16 - Static variable in class org.smtlib.Utils: Short names for common FloatingPoint sorts (FloatingPoint.smt2's :notes documents each as a synonym for a specific (_ FloatingPoint eb sb) instance) -- resolved by SymbolTable.lookupSort() to the exact same ISort.IDefinition as that instance, not registered as their own independent sorts (see Utils.loadTheory(), which excludes them from the generic :sorts loader for the same reason).
FLOAT32 - Static variable in class org.smtlib.Utils
FLOAT64 - Static variable in class org.smtlib.Utils
FLOATING_POINT - Enum constant in enum class org.smtlib.SolverCapabilities.Capability
FLOATINGPOINT - Static variable in class org.smtlib.Utils
FLOATINGPOINT_SYM - Static variable in class org.smtlib.Utils: Canonical ISymbol form of FLOATINGPOINT, for structural comparison against a parsed identifier's head symbol (see TypeChecker.isFloatingPoint() and SymbolTable's FloatingPoint family check) instead of comparing via .toString().
floatingPointTheorySet - Variable in class org.smtlib.SymbolTable: true if the FloatingPoint theory has been set
flush() - Method in class org.smtlib.Log: Logs held output, in order, up to the first pending output that is not yet ready
flush() - Method in class org.smtlib.sexpr.Printer: Flushes the writer, converting any IOException to VisitorException.
forall(List<IExpr.IDeclaration>, IExpr) - Method in interface org.smtlib.IExpr.IFactory: Creates a Forall expression.
forall(List<IExpr.IDeclaration>, IExpr) - Method in class org.smtlib.impl.Factory
forall(List<IExpr.IDeclaration>, IExpr, List<IExpr>) - Method in interface org.smtlib.IExpr.IFactory: Creates a Forall expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
forall(List<IExpr.IDeclaration>, IExpr, List<IExpr>) - Method in class org.smtlib.impl.Factory
Forall(List<IExpr.IDeclaration>, IExpr) - Constructor for class org.smtlib.impl.SMTExpr.Forall: Creates a forall expression with the given bound variable declarations and body.
FORALL - Static variable in class org.smtlib.sexpr.Utils
FORALL - Static variable in class org.smtlib.Utils: The String for the forall reserved word
forceExit() - Method in class org.smtlib.AbstractSolver
forceExit() - Method in interface org.smtlib.ISolver: Terminates the solver forcibly without sending commands (e.g.
forceExit() - Method in class org.smtlib.solvers.Solver_test
forceExit() - Method in class org.smtlib.solvers.Solver_z3_4_3
formula - Variable in class org.smtlib.command.C_assert: The formula to assert
forName(String) - Static method in class org.smtlib.SolverResolver: Class.forName(String), or null if there is no such class: the production class lookup
FP - Static variable in class org.smtlib.Utils
FP_ABS - Static variable in class org.smtlib.Utils
FP_ADD - Static variable in class org.smtlib.Utils
FP_DIV - Static variable in class org.smtlib.Utils
FP_EQ - Static variable in class org.smtlib.Utils
FP_FMA - Static variable in class org.smtlib.Utils
FP_GEQ - Static variable in class org.smtlib.Utils
FP_GT - Static variable in class org.smtlib.Utils
FP_IS_INFINITE - Static variable in class org.smtlib.Utils
FP_IS_NAN - Static variable in class org.smtlib.Utils
FP_IS_NEGATIVE - Static variable in class org.smtlib.Utils
FP_IS_NORMAL - Static variable in class org.smtlib.Utils
FP_IS_POSITIVE - Static variable in class org.smtlib.Utils
FP_IS_SUBNORMAL - Static variable in class org.smtlib.Utils
FP_IS_ZERO - Static variable in class org.smtlib.Utils
FP_LEQ - Static variable in class org.smtlib.Utils
FP_LT - Static variable in class org.smtlib.Utils
FP_MAX - Static variable in class org.smtlib.Utils
FP_MIN - Static variable in class org.smtlib.Utils
FP_MUL - Static variable in class org.smtlib.Utils
FP_NAN - Static variable in class org.smtlib.Utils
FP_NEG - Static variable in class org.smtlib.Utils
FP_NEG_INF - Static variable in class org.smtlib.Utils
FP_NEG_ZERO - Static variable in class org.smtlib.Utils
FP_POS_INF - Static variable in class org.smtlib.Utils: Zero-arity indexed identifiers, e.g.
FP_POS_ZERO - Static variable in class org.smtlib.Utils
FP_REM - Static variable in class org.smtlib.Utils
FP_ROUND_TO_INTEGRAL - Static variable in class org.smtlib.Utils
FP_SQRT - Static variable in class org.smtlib.Utils
FP_SUB - Static variable in class org.smtlib.Utils
FP_TO_REAL - Static variable in class org.smtlib.Utils
FP_TO_SBV - Static variable in class org.smtlib.Utils
FP_TO_UBV - Static variable in class org.smtlib.Utils
functionDeclaration(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort) - Method in interface org.smtlib.IExpr.IFactory: Creates a function declaration (used in define-funs-rec).
functionDeclaration(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort) - Method in class org.smtlib.impl.Factory
FunctionDeclaration(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort) - Constructor for class org.smtlib.impl.SMTExpr.FunctionDeclaration: Creates a function declaration with the given name, parameter declarations, and result sort.
FUNS - Static variable in class org.smtlib.Utils: The attribute tag for defining functions in a theory

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form