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

C

C_assert - Class in org.smtlib.command
Implements the assert command
C_assert(IExpr) - Constructor for class org.smtlib.command.C_assert
Constructs a command object given the expression to assert
C_check_sat - Class in org.smtlib.command
Implements the check-sat command
C_check_sat() - Constructor for class org.smtlib.command.C_check_sat
Creates a check_sat command (which has no arguments)
C_check_sat_assuming - Class in org.smtlib.command
Implements the check-sat-assuming command
C_check_sat_assuming(List<IExpr>) - Constructor for class org.smtlib.command.C_check_sat_assuming
Creates a check-sat-assuming command with the given assumption terms.
C_comment - Class in org.smtlib.command
A synthetic pseudo-command representing a comment that appeared immediately before a real command in a script -- not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand.Icomment (see issue #115) rather than a generic ICommand, so execution, typed-visitor traversal, and printing all dispatch to it the same way every other command does, with no reflection-based or generic-fallback special case.
C_comment(String) - Constructor for class org.smtlib.command.C_comment
 
C_declare_const - Class in org.smtlib.command
Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
C_declare_const(IExpr.ISymbol, ISort) - Constructor for class org.smtlib.command.C_declare_const
Constructs a command instance from its components
C_declare_datatype - Class in org.smtlib.command
Implements the declare-datatype command
C_declare_datatype(IExpr.ISortDeclaration, ISort.IDatatype) - Constructor for class org.smtlib.command.C_declare_datatype
Constructs a new command object
C_declare_datatypes - Class in org.smtlib.command
Implements the declare-datatypes command
C_declare_datatypes(List<IExpr.ISortDeclaration>, List<ISort.IDatatype>) - Constructor for class org.smtlib.command.C_declare_datatypes
Constructs a new command object
C_declare_fun - Class in org.smtlib.command
Implements the declare-fun command
C_declare_fun(IExpr.ISymbol, List<ISort>, ISort) - Constructor for class org.smtlib.command.C_declare_fun
Constructs a command instance for an ordinary (non-attributed, non-par) declaration
C_declare_fun(IExpr.ISymbol, List<ISort>, ISort, List<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.command.C_declare_fun
Constructs a command instance for an ordinary declaration, including any trailing attributes (see attributes()).
C_declare_fun(IExpr.ISymbol, List<ISort>, ISort, List<IExpr.IAttribute<?>>, List<ISort.IParameter>) - Constructor for class org.smtlib.command.C_declare_fun
Constructs a command instance from all of its components, including the par-polymorphic parameters (see parameters()) for the "(declare-fun par ...)" form.
C_declare_sort - Class in org.smtlib.command
Implements the declare-sort command
C_declare_sort(IExpr.ISymbol, IExpr.INumeral) - Constructor for class org.smtlib.command.C_declare_sort
Constructs a new command object
C_declare_sort_parameter - Class in org.smtlib.command
Implements the declare-sort-parameter command
C_declare_sort_parameter(IExpr.ISymbol) - Constructor for class org.smtlib.command.C_declare_sort_parameter
Constructs a new command object
C_define_const - Class in org.smtlib.command
Implements the define-const command: syntactic sugar for define-fun with no parameters
C_define_const(IExpr.ISymbol, ISort, IExpr) - Constructor for class org.smtlib.command.C_define_const
Constructs a command instance
C_define_fun - Class in org.smtlib.command
Implements the define-fun command
C_define_fun(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Constructor for class org.smtlib.command.C_define_fun
Constructs a command instance
C_define_fun_rec - Class in org.smtlib.command
Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.
C_define_fun_rec(IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Constructor for class org.smtlib.command.C_define_fun_rec
Constructs a command instance
C_define_funs_rec - Class in org.smtlib.command
Implements the define-funs-rec command
C_define_funs_rec(List<IExpr.IFunctionDeclaration>, List<IExpr>) - Constructor for class org.smtlib.command.C_define_funs_rec
Constructs a command instance
C_define_sort - Class in org.smtlib.command
Implements the define-sort command
C_define_sort(IExpr.ISymbol, List<ISort.IParameter>, ISort) - Constructor for class org.smtlib.command.C_define_sort
Constructs a command instance
C_echo - Class in org.smtlib.command
Implements the echo command
C_echo(IExpr.IStringLiteral) - Constructor for class org.smtlib.command.C_echo
Constructs an instance of the command
C_exec - Class in org.smtlib.ext
Implements the non-standard exec command
C_exec(ICommand.IScript) - Constructor for class org.smtlib.ext.C_exec
Constructs a command object for the given script
C_exit - Class in org.smtlib.command
Implements the exit command
C_exit() - Constructor for class org.smtlib.command.C_exit
Constructs an instance of the command
C_get_assertions - Class in org.smtlib.command
Implements the get-assertions command
C_get_assertions() - Constructor for class org.smtlib.command.C_get_assertions
Constructs a command instance
C_get_assignment - Class in org.smtlib.command
Implements the get-assignment command
C_get_assignment() - Constructor for class org.smtlib.command.C_get_assignment
Constructs a command instance
C_get_info - Class in org.smtlib.command
Implements the get-info command.
C_get_info(IExpr.IKeyword) - Constructor for class org.smtlib.command.C_get_info
Constructs a command instance given the keyword
C_get_model - Class in org.smtlib.command
Implements the get-model command
C_get_model() - Constructor for class org.smtlib.command.C_get_model
Constructs a command instance
C_get_option - Class in org.smtlib.command
Implements the get-option command
C_get_option(IExpr.IKeyword) - Constructor for class org.smtlib.command.C_get_option
Constructs a command instance for the given keyword
C_get_proof - Class in org.smtlib.command
Implements the get-proof command
C_get_proof() - Constructor for class org.smtlib.command.C_get_proof
Constructs a command instance
C_get_unsat_assumptions - Class in org.smtlib.command
Implements the get-unsat-assumptions command
C_get_unsat_assumptions() - Constructor for class org.smtlib.command.C_get_unsat_assumptions
Constructs a command instance
C_get_unsat_core - Class in org.smtlib.command
Implements the get-unsat-core command
C_get_unsat_core() - Constructor for class org.smtlib.command.C_get_unsat_core
Constructs a command instance
C_get_value - Class in org.smtlib.command
Implements the get-value command
C_get_value(List<IExpr>) - Constructor for class org.smtlib.command.C_get_value
Constructs a command instance
C_pop - Class in org.smtlib.command
Implements the pop command
C_pop(IExpr.INumeral) - Constructor for class org.smtlib.command.C_pop
Constructs a command instance
C_push - Class in org.smtlib.command
Implements the push command
C_push(IExpr.INumeral) - Constructor for class org.smtlib.command.C_push
Constructs a command instance
C_reset - Class in org.smtlib.command
Implements the reset command
C_reset() - Constructor for class org.smtlib.command.C_reset
Constructs an instance of the command
C_reset_assertions - Class in org.smtlib.command
Implements the reset-assertions command
C_reset_assertions() - Constructor for class org.smtlib.command.C_reset_assertions
Constructs an instance of the command
C_set_info - Class in org.smtlib.command
Implements the set-info command
C_set_info(IExpr.IKeyword, IAttributeValue) - Constructor for class org.smtlib.command.C_set_info
Construct an instance of the command
C_set_logic - Class in org.smtlib.command
Implements the set-logic command.
C_set_logic(IExpr.ISymbol) - Constructor for class org.smtlib.command.C_set_logic
Constructs a command instance for the given logic name.
C_set_option - Class in org.smtlib.command
Implements the set-option command
C_set_option(IExpr.IKeyword, IAttributeValue) - Constructor for class org.smtlib.command.C_set_option
Construct an instance of the command
C_what - Class in org.smtlib.ext
Implements the non-standard what command.
C_what(List<IExpr.IIdentifier>) - Constructor for class org.smtlib.ext.C_what
Constructs a command instance for the given identifiers.
cases - Variable in class org.smtlib.impl.SMTExpr.Match
 
cases() - Method in interface org.smtlib.IExpr.IMatch
 
cases() - Method in class org.smtlib.impl.SMTExpr.Match
 
CHAR - Static variable in class org.smtlib.Utils
Head of the Strings theory's (_ char H) constants.
charAt(int) - Method in class org.smtlib.CharSequenceInfinite
Returns the char at the given index; this may block while input is read if the char has not been read before.
charAt(int) - Method in class org.smtlib.impl.Pos.Source
 
charAt(int) - Method in interface org.smtlib.ISource
Returns the character at the given character position within the source.
charEnd - Variable in class org.smtlib.impl.Pos
One past the last character of the range, beginning from 0
charEnd() - Method in class org.smtlib.impl.Pos
One past the last character of the range, beginning from 0
charEnd() - Method in interface org.smtlib.IPos
One beyond the last position of the character sequence range (0-based).
chars() - Method in class org.smtlib.impl.Pos.Source
The sequence of characters
chars() - Method in interface org.smtlib.ISource
The internal character stream as a CharSequence.
CharSequenceInfinite - Class in org.smtlib
This class implements a CharSequence that obtains its characters from a source of characters of unknown length; it also provides some functionality to retain the characters and compute line numbers.
CharSequenceInfinite(int, int, double) - Constructor for class org.smtlib.CharSequenceInfinite
Constructor for a new instance
CharSequenceInfinite.IPrompter - Interface in org.smtlib
This interface is used to create prompters.
CharSequenceReader - Class in org.smtlib
This class implements a CharSequence that obtains its characters from a Reader.
CharSequenceReader(Reader) - Constructor for class org.smtlib.CharSequenceReader
Constructor for a new instance
CharSequenceReader(Reader, int, int, double) - Constructor for class org.smtlib.CharSequenceReader
Constructor for a new instance
CharSequenceSocket - Class in org.smtlib
This class implements a CharSequence that obtains its characters from a ServerSocket.
CharSequenceSocket(SMT.Configuration, ServerSocket, int, int, double) - Constructor for class org.smtlib.CharSequenceSocket
Constructor for a new instance
charset - Variable in class org.smtlib.SolverProcess
The charset used to encode text sent to the process and decode text read back from it
charStart - Variable in class org.smtlib.impl.Pos
The starting character, beginning from 0
charStart() - Method in class org.smtlib.impl.Pos
The starting character, beginning from 0
charStart() - Method in interface org.smtlib.IPos
The starting position within the character sequence (0-based)
check(SymbolTable, IExpr) - Static method in class org.smtlib.TypeChecker
The main entry point for type-checking an IExpr (expected to be a Bool)
check_sat() - Method in class org.smtlib.AbstractSolver
 
check_sat() - Method in interface org.smtlib.ICommand.IFactory
Creates a check-sat command object.
check_sat() - Method in class org.smtlib.impl.Factory
 
check_sat() - Method in interface org.smtlib.ISolver
Checks whether the current assertion set is satisfiable under the current logic.
check_sat() - Method in class org.smtlib.solvers.Solver_bitwuzla
 
check_sat() - Method in class org.smtlib.solvers.Solver_simplify
 
check_sat() - Method in class org.smtlib.solvers.Solver_test
 
check_sat() - Method in class org.smtlib.solvers.Solver_z3_4_3
 
check_sat() - Method in class org.smtlib.solvers.Solver_z3_recent
 
CHECK_SAT - Enum constant in enum class org.smtlib.AbstractSolver.Shape
sat, unsat, unknown (or timeout, memout, incomplete): check-sat and check-sat-assuming
check_sat_assuming(List<IExpr>) - Method in interface org.smtlib.ICommand.IFactory
Creates a check-sat-assuming command object.
check_sat_assuming(List<IExpr>) - Method in class org.smtlib.impl.Factory
 
check_sat_assuming(IExpr...) - Method in class org.smtlib.AbstractSolver
 
check_sat_assuming(IExpr...) - Method in interface org.smtlib.ISolver
Checks satisfiability under the current assertion set plus the given propositional assumptions.
check_sat_assuming(IExpr...) - Method in class org.smtlib.solvers.Solver_bitwuzla
 
check_sat_assuming(IExpr...) - Method in class org.smtlib.solvers.Solver_simplify
check-sat-assuming postdates Simplify by well over a decade (added in SMT-LIB 2.6; Simplify's protocol has no concept of it), and this class has no override for it -- without one, it silently inherits Solver_test's stub (this class's superclass, the type-check-only pseudo-solver), which never talks to the real Simplify process at all and just echoes back whatever :status a script happened to declare (or "unknown" if none), regardless of whether the assumed literals are actually satisfiable.
check_sat_assuming(IExpr...) - Method in class org.smtlib.solvers.Solver_test
 
check_sat_assuming(IExpr...) - Method in class org.smtlib.solvers.Solver_z3_4_3
z3 4.3 answers unsupported for check-sat-assuming, so it is sent as z3's legacy (check-sat a1 ...
check_sat_assuming(IExpr...) - Method in class org.smtlib.solvers.Solver_z3_recent
 
checkArraySorts(List<ISort>, ISort, IExpr.IIdentifier) - Method in class org.smtlib.logic.Logic
Checks the Array sorts in a function's argument and result sorts
checkArraySorts(ISort, IPos) - Method in class org.smtlib.logic.Logic
Checks every Array sort within sort, expanding abbreviations, against Logic.allowedArraySort(org.smtlib.ISort.IApplication).
checkAssertion(SymbolTable, IExpr) - Static method in class org.smtlib.TypeChecker
The main entry point for type-checking an assert expression (expected to be a Bool); unlike TypeChecker.check(SymbolTable,IExpr), this checks the expression within a pushed scope that is merged into the enclosing scope on success (or popped on error).
checkAtom(IExpr.IFcnExpr, IExpr, IExpr) - Method in class org.smtlib.logic.DifferenceLogic
Checks the arguments of a binary arithmetic atom (op lhs rhs).
checkAtom(IExpr.IFcnExpr, IExpr, IExpr) - Method in class org.smtlib.logic.QF_IDL
 
checkAtom(IExpr.IFcnExpr, IExpr, IExpr) - Method in class org.smtlib.logic.QF_RDL
 
checkBoundArraySorts(IExpr) - Method in class org.smtlib.logic.Logic
Checks the Array sorts of the variables bound by quantifiers in expression
checkFcn(SymbolTable, IExpr.IIdentifier, List<IExpr.IDeclaration>, ISort, IExpr) - Static method in class org.smtlib.TypeChecker
 
checkFcn(SymbolTable, IExpr.IIdentifier, List<ISort>, ISort, IPos) - Static method in class org.smtlib.TypeChecker
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in interface org.smtlib.ILanguage
Checks whether the given function declaration is permitted in the language, throwing an exception if not
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.impl.SMTExpr.Logic
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.ALL
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.AUFLIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.AUFLIRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.AUFNIRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.LIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.LRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_ABV
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_AUFBV
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_AUFLIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_AX
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_BV
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_EIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_FP
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_IDL
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_NIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_NRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_RDL
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_UF
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_UFIDL
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_UFLIA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_UFLRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.QF_UFNRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.UFLRA
 
checkFcnDeclaration(IExpr.IIdentifier, List<ISort>, ISort, IExpr) - Method in class org.smtlib.logic.UFNIA
 
checkFcnRec(SymbolTable, boolean, IExpr.ISymbol, List<IExpr.IDeclaration>, ISort, IExpr) - Static method in class org.smtlib.TypeChecker
Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression.
checkFcnsRec(SymbolTable, boolean, List<IExpr.IFunctionDeclaration>, List<IExpr>) - Static method in class org.smtlib.TypeChecker
Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression.
checkImmediateExit(IResponse) - Method in class org.smtlib.AbstractSolver
Called with each response parsed from the solver.
checkNoArg() - Method in class org.smtlib.sexpr.Parser
A helper check, called by command-specific parse methods in which the commands have no arguments
checkOptionType(SMT.Configuration, IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.command.C_set_option
This method checks that the value for the given keyword has the correct type, when the keyword is used as the key for an SMT-LIB option.
checkPatternTerm(IExpr) - Method in class org.smtlib.TypeChecker
Checks that a pattern term is binder-free and has no annotations (SMT-LIB 2.7, Section 3.6.5); returns false, recording an error, if it is not.
checkPrintSuccess(SMT.Configuration, IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.AbstractSolver
Answers a set-option of :print-success locally (it is never sent), else returns null
checkSatStatus - Variable in class org.smtlib.AbstractSolver
The response to the most recent check-sat or check-sat-assuming, or null if there is none.
checkSatStatus - Variable in class org.smtlib.SMT
The last check-sat status seen during execution; null if no check-sat has been executed yet.
checkSatStatus - Variable in class org.smtlib.solvers.Solver_test
Internal state variable - set to sat, unsat, unknown when check-sat is run and then to null whenever an additional push, pop, assert, declare- or define- command is executed.
checkSatStatus() - Method in class org.smtlib.AbstractSolver
 
checkSatStatus() - Method in interface org.smtlib.ISolver
Returns the result of the most recent check-sat or check-sat-assuming, or null if none has been issued since the last push/pop/assert/declare/define.
checkSatStatus() - Method in class org.smtlib.solvers.Solver_test
 
checkShape(AbstractSolver.Shape, String, String, IResponse) - Method in class org.smtlib.AbstractSolver
r, if it has the given shape; else the error for a response out of step with the command sent, whose raw response was text
checkSortAbbreviation(SymbolTable, IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Static method in class org.smtlib.TypeChecker
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in interface org.smtlib.ILanguage
Checks whether the given sort declaration is permitted in the language, throwing an exception if not
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.impl.SMTExpr.Logic
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.ALL
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.AUFLIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.AUFLIRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.AUFNIRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.LIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.LRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_ABV
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_AUFBV
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_AUFLIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_AX
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_BV
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_EIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_FP
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_IDL
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_NIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_NRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_RDL
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_UFIDL
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_UFLIA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_UFLRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.QF_UFNRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.UFLRA
 
checkSortDeclaration(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.logic.UFNIA
 
checkStatus() - Method in class org.smtlib.AbstractSolver
The response to the most recent check command, or null if there is none or the solver has accepted a command that changes the assertion stack since (after reading the responses to the pipelined commands): sat or unknown in SMT-LIB's sat mode, unsat in its unsat mode
checkTerm(SymbolTable, IExpr) - Static method in class org.smtlib.TypeChecker
Type-checks a term of any sort (e.g.
checkUserId(IExpr.ISymbol) - Method in interface org.smtlib.IParser
Checks that a user-defined symbol does not begin with the reserved characters @ or .; throws a ParserException if the check fails.
cleanup() - Method in class org.smtlib.SMT
Forcibly stops the active solver, if any.
clear(boolean) - Method in class org.smtlib.SymbolTable
Leaves the background frame and an empty primary frame, the state after set-logic; keepBackground false empties the background frame too.
clearListeners() - Method in class org.smtlib.Log
Clears all listeners
clearSorts(IExpr) - Static method in class org.smtlib.TypeChecker
Walks the given expression subtree, nulling out the sort recorded on each node (e.g.
clone() - Method in class org.smtlib.SMT.Configuration
Makes an independent copy of the configuration: a shallow, reference-copying field-for-field clone (via super.clone()) is not enough on its own, since several fields are mutable containers or hold a back-reference to this Configuration -- left reference-copied, mutating one of those through the clone would silently mutate the original too, contradicting this class's own "Separate instances of SMT objects can be run independently and in parallel" design goal (see the class Javadoc).
close() - Method in class org.smtlib.impl.Pos.Source
 
close() - Method in interface org.smtlib.ISource
Closes any open resources - the source is not usable after this call.
closed - Variable in class org.smtlib.TypeChecker.Variable
Whether a reference to this variable is itself closed (no free/bound variable reachable through it) -- false for a quantifier- or match-pattern-bound variable (which IS the free variable), true for a let-bound variable whose own defining expression was itself closed when the let was checked, false for one that wasn't (e.g.
cmd(String) - Method in class org.smtlib.solvers.Solver_smt
 
cmd(String) - Method in class org.smtlib.solvers.Solver_yices2_2_6
 
cmd(String) - Method in class org.smtlib.solvers.Solver_yices2
 
cmds - Variable in class org.smtlib.solvers.Solver_altergo
The command-line arguments for launching the solver.
cmds - Variable in class org.smtlib.solvers.Solver_bitwuzla
The command-line arguments for launching the solver.
cmds - Variable in class org.smtlib.solvers.Solver_cvc5
The command-line arguments for launching the solver.
cmds - Variable in class org.smtlib.solvers.Solver_smtinterpol
The command-line arguments for launching the solver.
cmds - Variable in class org.smtlib.solvers.Solver_z3_4_3
The command-line arguments for launching the Z3 solver
cmds - Variable in class org.smtlib.solvers.Solver_z3_recent
The command-line arguments for launching the solver.
cmds_mac - Variable in class org.smtlib.solvers.Solver_cvc5
 
cmds_mac - Variable in class org.smtlib.solvers.Solver_z3_4_3
 
cmds_mac - Variable in class org.smtlib.solvers.Solver_z3_recent
 
cmds_unix - Variable in class org.smtlib.solvers.Solver_cvc5
 
cmds_unix - Variable in class org.smtlib.solvers.Solver_z3_4_3
 
cmds_unix - Variable in class org.smtlib.solvers.Solver_z3_recent
 
cmds_win - Variable in class org.smtlib.solvers.Solver_cvc5
 
cmds_win - Variable in class org.smtlib.solvers.Solver_z3_4_3
 
cmds_win - Variable in class org.smtlib.solvers.Solver_z3_recent
 
combined - Static variable in class org.smtlib.sexpr.Lexer
This composite regular expression matches tokens in the SMTLIB input.
command() - Method in record class org.smtlib.SolverResolver.Resolution
Returns the value of the command record component.
Command - Class in org.smtlib.impl
This abstract class is the base class for all commands within this implementation.
Command() - Constructor for class org.smtlib.impl.Command
 
commandExtensionPrefixes - Variable in class org.smtlib.SMT.Configuration
An array of fully-qualified class name prefixes; a command name (with hyphen replaced by underscore) is appended to the prefix to obtain a fully-qualified class name that implements the command.
commandFactory - Variable in class org.smtlib.SMT.Configuration
The factory to use to create ICommand objects
commandFinder - Variable in class org.smtlib.SMT.Configuration
A class that implements ICommandFinder, whose one method returns the class object of the class that implements a command with a given name; the algorithm to identify the command class first looks for an entry in the command map above and otherwise uses this default: replace each - in the command name by _, and append the resulting string to the elements of 'commandExtensionPrefixes', looking for the first such class that exists; if relax is false (strict SMT-LIB) then the commands map and all but the initial entry of commandExtensionPrefixes are ignored.
commandHasError - Variable in class org.smtlib.sexpr.Parser
Whether the command being parsed (or last returned) had a recoverable syntax error
commandHasError() - Method in interface org.smtlib.IParser
Returns true if the command most recently returned by parseCommand() had a syntax error that parsing recovered from; such a command is not sent to a solver
commandHasError() - Method in class org.smtlib.sexpr.Parser
 
commandHasLexicalError - Variable in class org.smtlib.sexpr.Parser
Whether any such error was an invalid character, which the type checker does not see
commandHasLexicalError() - Method in interface org.smtlib.IParser
Returns true if one of the errors commandHasError() reports was an invalid character
commandHasLexicalError() - Method in class org.smtlib.sexpr.Parser
 
commandName - Static variable in class org.smtlib.command.C_assert
The command name
commandName - Static variable in class org.smtlib.command.C_check_sat_assuming
The command name
commandName - Static variable in class org.smtlib.command.C_check_sat
The command name
commandName - Static variable in class org.smtlib.command.C_comment
 
commandName - Static variable in class org.smtlib.command.C_declare_const
The command name
commandName - Static variable in class org.smtlib.command.C_declare_datatype
The command name
commandName - Static variable in class org.smtlib.command.C_declare_datatypes
The command name
commandName - Static variable in class org.smtlib.command.C_declare_fun
The command name
commandName - Static variable in class org.smtlib.command.C_declare_sort_parameter
The command name
commandName - Static variable in class org.smtlib.command.C_declare_sort
The command name
commandName - Static variable in class org.smtlib.command.C_define_const
The command name
commandName - Static variable in class org.smtlib.command.C_define_fun_rec
The command name
commandName - Static variable in class org.smtlib.command.C_define_fun
The command name
commandName - Static variable in class org.smtlib.command.C_define_funs_rec
The command name
commandName - Static variable in class org.smtlib.command.C_define_sort
The command name
commandName - Static variable in class org.smtlib.command.C_echo
 
commandName - Static variable in class org.smtlib.command.C_exit
 
commandName - Static variable in class org.smtlib.command.C_get_assertions
The command name
commandName - Static variable in class org.smtlib.command.C_get_assignment
The command name
commandName - Static variable in class org.smtlib.command.C_get_info
The command name
commandName - Static variable in class org.smtlib.command.C_get_model
The command name
commandName - Static variable in class org.smtlib.command.C_get_option
The command name
commandName - Static variable in class org.smtlib.command.C_get_proof
The command name
commandName - Static variable in class org.smtlib.command.C_get_unsat_assumptions
The command name
commandName - Static variable in class org.smtlib.command.C_get_unsat_core
The command name
commandName - Static variable in class org.smtlib.command.C_get_value
The command name
commandName - Static variable in class org.smtlib.command.C_pop
The command name
commandName - Static variable in class org.smtlib.command.C_push
The command name
commandName - Static variable in class org.smtlib.command.C_reset_assertions
 
commandName - Static variable in class org.smtlib.command.C_reset
 
commandName - Static variable in class org.smtlib.command.C_set_info
The command name
commandName - Static variable in class org.smtlib.command.C_set_logic
The command name
commandName - Static variable in class org.smtlib.command.C_set_option
The command name
commandName - Static variable in class org.smtlib.ext.C_exec
The command name
commandName - Static variable in class org.smtlib.ext.C_what
The command name
commandName - Variable in class org.smtlib.sexpr.Parser
This field is used only to communicate the position of the name of a command to the command creator (instead of using method arguments).
commandName() - Method in class org.smtlib.command.C_assert
The command name
commandName() - Method in class org.smtlib.command.C_check_sat_assuming
The command name
commandName() - Method in class org.smtlib.command.C_check_sat
The command name
commandName() - Method in class org.smtlib.command.C_comment
 
commandName() - Method in class org.smtlib.command.C_declare_const
The command name
commandName() - Method in class org.smtlib.command.C_declare_datatype
The command name
commandName() - Method in class org.smtlib.command.C_declare_datatypes
 
commandName() - Method in class org.smtlib.command.C_declare_fun
The command name
commandName() - Method in class org.smtlib.command.C_declare_sort_parameter
The command name
commandName() - Method in class org.smtlib.command.C_declare_sort
The command name
commandName() - Method in class org.smtlib.command.C_define_const
The command name
commandName() - Method in class org.smtlib.command.C_define_fun_rec
The command name
commandName() - Method in class org.smtlib.command.C_define_fun
The command name
commandName() - Method in class org.smtlib.command.C_define_funs_rec
The command name
commandName() - Method in class org.smtlib.command.C_define_sort
The command name
commandName() - Method in class org.smtlib.command.C_echo
The command name
commandName() - Method in class org.smtlib.command.C_exit
The command name
commandName() - Method in class org.smtlib.command.C_get_assertions
The command name
commandName() - Method in class org.smtlib.command.C_get_assignment
The command name
commandName() - Method in class org.smtlib.command.C_get_info
The command name
commandName() - Method in class org.smtlib.command.C_get_model
The command name
commandName() - Method in class org.smtlib.command.C_get_option
The command name
commandName() - Method in class org.smtlib.command.C_get_proof
The command name
commandName() - Method in class org.smtlib.command.C_get_unsat_assumptions
The command name
commandName() - Method in class org.smtlib.command.C_get_unsat_core
The command name
commandName() - Method in class org.smtlib.command.C_get_value
The command name
commandName() - Method in class org.smtlib.command.C_pop
The command name
commandName() - Method in class org.smtlib.command.C_push
The command name
commandName() - Method in class org.smtlib.command.C_reset_assertions
The command name
commandName() - Method in class org.smtlib.command.C_reset
The command name
commandName() - Method in class org.smtlib.command.C_set_info
The command name
commandName() - Method in class org.smtlib.command.C_set_logic
The command name
commandName() - Method in class org.smtlib.command.C_set_option
The command name
commandName() - Method in class org.smtlib.ext.C_exec
The command name
commandName() - Method in class org.smtlib.ext.C_what
The command name
commandName() - Method in interface org.smtlib.ICommand
Returns the SMT-LIB name of this command (e.g.
commandName() - Method in class org.smtlib.impl.Command
The command name
commands - Variable in class org.smtlib.Driver
The commands as specified on the command-line
commands - Variable in class org.smtlib.impl.Script
The list of commands
commands - Variable in class org.smtlib.SMT.Configuration
Holds a mapping from command name to the class implementing the command
commands() - Method in interface org.smtlib.ICommand.IScript
 
commands() - Method in class org.smtlib.impl.Script
Returns a reference to the internal list
comment(String) - Method in class org.smtlib.AbstractSolver
Forwards a standalone comment (its own C_comment pseudo-command -- see issue #42) to the solver process, uniformly for every solver adapter: a comment is legal SMT-LIB input (any conforming solver must silently ignore it), and the solver's log then shows the script's comments.
comment(String) - Method in interface org.smtlib.ICommand.IFactory
Creates a comment pseudo-command object, carrying the given raw comment text (see ICommand.Icomment).
comment(String) - Method in class org.smtlib.impl.Factory
 
comment(String) - Method in interface org.smtlib.ISolver
Passes comment text to the solver (for logging/tracing); the argument is the comment body without the leading semicolon.
comment(String) - Method in class org.smtlib.solvers.Solver_test
 
CONCAT - Static variable in class org.smtlib.Utils
 
Configuration() - Constructor for class org.smtlib.SMT.Configuration
Creates a default configuration, initialized from org.smtlib.impl
configuredExecutable(Properties, String, String) - Static method in class org.smtlib.SolverResolver
The executable the properties configure for the solver: .exec.<platform>, then .exec; null if neither is given, or it is blank.
constant(String) - Method in class org.smtlib.impl.Response.Factory
 
constant(String) - Method in interface org.smtlib.IResponse.IFactory
Returns a constant response with the given canonical name
constructor - Variable in class org.smtlib.impl.SMTExpr.Pattern
 
constructor() - Method in interface org.smtlib.IExpr.IPattern
 
constructor() - Method in class org.smtlib.impl.SMTExpr.Pattern
 
constructor(IExpr.ISymbol, List<IExpr.ISelector>) - Method in interface org.smtlib.IExpr.IFactory
Creates a constructor declaration.
constructor(IExpr.ISymbol, List<IExpr.ISelector>) - Method in class org.smtlib.impl.Factory
 
Constructor(IExpr.ISymbol, List<IExpr.ISelector>) - Constructor for class org.smtlib.impl.SMTExpr.Constructor
Creates a constructor with the given name and list of selector declarations.
constructors - Variable in class org.smtlib.impl.SMTExpr.Datatype
 
constructors() - Method in class org.smtlib.impl.SMTExpr.Datatype
 
constructors() - Method in interface org.smtlib.ISort.IDatatype
 
containsParameter(ISort) - Static method in class org.smtlib.SymbolTable
Whether the sort contains a sort parameter.
continued_execution() - Method in class org.smtlib.impl.Response.Factory
 
continued_execution() - Method in interface org.smtlib.IResponse.IFactory
 
CONTINUED_EXECUTION - Static variable in class org.smtlib.impl.Response
 
CONTINUED_EXECUTION - Static variable in class org.smtlib.Utils
An ERROR_BEHAVIOR return value
CORE - Static variable in class org.smtlib.Utils
Name of the Core theory
correctResponse(ICommand, String) - Method in class org.smtlib.AbstractSolver
The solver's raw response to cmd (sent by sendCommand and waited for), corrected where the solver departs from SMT-LIB; an adapter overrides this to patch a specific non-conforming response
createErrorDefinition(IExpr.IIdentifier, String, IPos) - Method in class org.smtlib.impl.Factory
 
createErrorDefinition(IExpr.IIdentifier, String, IPos) - Method in interface org.smtlib.ISort.IFactory
Creates an error-placeholder definition (suppresses cascading errors).
createFcnSort(ISort[], ISort) - Method in class org.smtlib.impl.Factory
 
createFcnSort(ISort[], ISort) - Method in interface org.smtlib.ISort.IFactory
Creates a function sort.
createParser(SMT.Configuration, ISource) - Method in interface org.smtlib.IParser.IFactory
Creates a parser that reads and parses concrete syntax from the given source
createParser(SMT.Configuration, ISource) - Method in class org.smtlib.sexpr.Factory
 
createPrinter(SMT.Configuration, Writer) - Method in interface org.smtlib.IParser.IFactory
Creates a printer
createPrinter(SMT.Configuration, Writer) - Method in class org.smtlib.sexpr.Factory
 
createSolver(String, String) - Method in class org.smtlib.SMT.Configuration
Resolves the given solver name and executable to a concrete ISolver adapter instance, applying the same name/executable/adapter resolution jsmtlib.properties supports as SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) -- platform-specific .adapter/.exec overrides checked before their bare counterparts, the Solver_<name> naming convention, the z3-specific Solver_z3_recent fallback for an unrecognized z3 variant, the generic Solver_smt fallback, the "test" pseudo-solver special case, and %exec% command-array placeholder substitution -- but, unlike startSolver, this method does not start the solver and does not do any CLI-flavored error()/usage() reporting: any resolution or construction failure is reported as a thrown ISolver.CreationException instead, leaving it to the caller to start the returned solver (via ISolver.start()) and decide how to report a creation failure.
createSortAbbreviation(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in class org.smtlib.impl.Factory
 
createSortAbbreviation(IExpr.IIdentifier, List<ISort.IParameter>, ISort) - Method in interface org.smtlib.ISort.IFactory
Creates a new sort abbreviation.
createSortExpression(IExpr.IIdentifier, List<ISort>) - Method in class org.smtlib.impl.Factory
 
createSortExpression(IExpr.IIdentifier, List<ISort>) - Method in interface org.smtlib.ISort.IFactory
Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
createSortExpression(IExpr.IIdentifier, ISort...) - Method in class org.smtlib.impl.Factory
 
createSortExpression(IExpr.IIdentifier, ISort...) - Method in interface org.smtlib.ISort.IFactory
Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
createSortFamily(IExpr.IIdentifier, IExpr.INumeral, List<IExpr.IAttribute<?>>) - Method in class org.smtlib.impl.Factory
 
createSortFamily(IExpr.IIdentifier, IExpr.INumeral, List<IExpr.IAttribute<?>>) - Method in interface org.smtlib.ISort.IFactory
Creates a sort family with the given identifier, arity, and attributes (null or empty if none).
createSortParameter(IExpr.ISymbol) - Method in class org.smtlib.impl.Factory
 
createSortParameter(IExpr.ISymbol) - Method in interface org.smtlib.ISort.IFactory
Creates a parameter for a parameterized sort abbreviation.
createSource(CharSequence, String) - Method in interface org.smtlib.IParser.IFactory
Creates a character source from the given CharSequence; the second argument is just to be used as a location designator.
createSource(CharSequence, String) - Method in class org.smtlib.sexpr.Factory
 
createSource(SMT.Configuration, File) - Method in interface org.smtlib.IParser.IFactory
Creates a character source from the given file
createSource(SMT.Configuration, File) - Method in class org.smtlib.sexpr.Factory
 
createSource(SMT.Configuration, InputStream, Object) - Method in interface org.smtlib.IParser.IFactory
Creates a character source from the given stream
createSource(SMT.Configuration, InputStream, Object) - Method in class org.smtlib.sexpr.Factory
 
CreationException(String) - Constructor for exception class org.smtlib.ISolver.CreationException
Creates a creation exception with the given message.
CreationException(String, Throwable) - Constructor for exception class org.smtlib.ISolver.CreationException
Creates a creation exception with the given message and underlying cause.
csr - Variable in class org.smtlib.sexpr.Lexer
The CharSequence corresponding to the source object
currentPos() - Method in class org.smtlib.sexpr.Lexer
Returns the position of the next character to be read
currentScope - Variable in class org.smtlib.TypeChecker
 
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