Index
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form
N
- name - Variable in class org.smtlib.SymbolTable.Entry
-
The identifier
- name() - Method in class org.smtlib.solvers.Solver_z3_4_3_2
- name() - Method in class org.smtlib.solvers.Solver_z3_4_3
-
The solver's display name for diagnostic logging.
- name(IExpr.ISymbol) - Method in class org.smtlib.solvers.Solver_simplify.Translator
-
The Simplify name of a symbol, as a function name or a bound variable
- NAME - Static variable in class org.smtlib.Utils
-
The string designating an info item
- NAME_VALUE - Static variable in class org.smtlib.Utils
-
The response to the :name info item
- names() - Method in class org.smtlib.impl.Response.UnsatCoreResponse
- names() - Method in interface org.smtlib.IResponse.IUnsatCoreResponse
- needsPrintSuccessPriming - Variable in class org.smtlib.solvers.Solver_z3_recent
-
True only on the platform where the print-success priming command below is needed (see the class javadoc)
- newPrinter(Writer) - Method in interface org.smtlib.IPrinter
-
Creates a new printer of the same type as the receiver, writing to the given Writer.
- newPrinter(Writer) - Method in class org.smtlib.sexpr.Printer
- newPrinter(Writer) - Method in class org.smtlib.sexpr.Printer.WithLines
- newPrinter(Writer) - Method in class org.smtlib.solvers.Printer
- next() - Method in class org.smtlib.SymbolTable.Iterator
- nextLine() - Method in class org.smtlib.SolverProcess
-
The number of the solver input line that the next text sent starts on (lines counted from 1)
- nextLineTermination(int) - Method in class org.smtlib.impl.Pos.Source
-
The (last character of) the next line termination sequence after the given character position
- nextSolverLine() - Method in class org.smtlib.AbstractSolver
-
The solver line, as the solver numbers lines in its messages, on which the next text sent starts; overridden for a solver that does not number the lines of its whole input
- nextSolverLine() - Method in class org.smtlib.solvers.Solver_cvc5
- NO - Enum constant in enum class org.smtlib.SolverCapabilities.Support
- noargs - Static variable in class org.smtlib.impl.Sort.FcnSort
- noExponentiation(IExpr) - Method in class org.smtlib.logic.Logic
- noFunctions(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.Logic
- nonCoefficients(IExpr.IFcnExpr, Predicate<IExpr>) - Static method in class org.smtlib.logic.Logic
-
The arguments of an application (of * or /) that are not coefficients.
- noQuantifiers(IExpr) - Method in class org.smtlib.logic.Logic
- NoResponseException(String) - Constructor for exception class org.smtlib.SolverProcess.NoResponseException
- normalizeForTesting(String, IExpr.IKeyword) - Static method in class org.smtlib.AbstractSolver
-
Replaces known sources of non-deterministic content in a raw solver response with a fixed placeholder, so that --testing runs produce byte-for-byte reproducible output across machines and repeated runs.
- noshow - Variable in class org.smtlib.SMT.Configuration
-
If true, then information about the position of an error is not shown
- noSorts(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.Logic
- nosuccess - Variable in class org.smtlib.SMT.Configuration
-
This field is set from the command-line and sets the initial state of the :print-success option within a solver.
- NOT - Static variable in class org.smtlib.Utils
- noVariables(List<?>, String, IPos) - Method in class org.smtlib.TypeChecker
-
Reports a binder with no variables; returns true if the list is empty
- number - Variable in class org.smtlib.command.C_pop
-
The int value giving the number of stack frames to pop (set by check()), if the value is in the range of an int type
- number - Variable in class org.smtlib.command.C_push
-
The int value giving the number of stack frames to push (set by check()), if the value is in the range of an int type
- number - Variable in class org.smtlib.impl.SMTExpr.Numeral
-
A value equivalent to the BigInteger, when it is in range.
- number() - Method in class org.smtlib.command.C_pop
-
The number of assertion set stack items to pop
- number() - Method in class org.smtlib.command.C_push
-
Returns the number of assertion set scopes to push.
- number() - Method in interface org.smtlib.ICommand.Ipop
-
Returns the number of scopes to pop.
- number() - Method in interface org.smtlib.ICommand.Ipush
-
Returns the number of scopes to push.
- numeral - Variable in class org.smtlib.command.C_pop
-
The (non-negative) number of stack frames to pop
- numeral - Variable in class org.smtlib.command.C_push
-
The (non-negative) number of stack frames to push
- numeral(long) - Method in interface org.smtlib.IExpr.IFactory
-
Creates an INumeral object; the argument must be non-negative.
- numeral(long) - Method in class org.smtlib.impl.Factory
- numeral(String) - Method in interface org.smtlib.IExpr.IFactory
-
Creates an INumeral object; the argument must be a string of digits.
- numeral(String) - Method in class org.smtlib.impl.Factory
- Numeral(int) - Constructor for class org.smtlib.impl.SMTExpr.Numeral
-
Constructs a Numeral with the given value.
- Numeral(BigInteger) - Constructor for class org.smtlib.impl.SMTExpr.Numeral
-
Constructs a Numeral with the given value.
- NUMERAL - Static variable in class org.smtlib.sexpr.Utils
-
Concrete syntax for the special NUMERAL token
- numericLiteral(int) - Method in class org.smtlib.impl.Response.Factory
- numericLiteral(int) - Method in interface org.smtlib.IResponse.IFactory
- numericOptions - Variable in class org.smtlib.Utils
-
The set of standard options with numeric values
- numErrors - Variable in class org.smtlib.Log
-
Number of errors logged since last clear
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form