Uses of Interface
org.smtlib.IExpr

Packages that use IExpr

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.logic	This package contains implementations of classes that implement the constraints of individual logics.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of IExpr in org.smtlib

Subinterfaces of IExpr in org.smtlib

Modifier and Type	Interface	Description
static interface	IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
static interface	IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
static interface	IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
static interface	IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
static interface	IExpr.IError	This interface represents an error, e.g.
static interface	IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
static interface	IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
static interface	IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
static interface	IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
static interface	IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
static interface	IExpr.IIndex	Marker interface for the index types in a parameterized identifier: INumeral and ISymbol, plus IHexLiteral, which the Strings theory's (_ char H) uses, and IBinaryLiteral, which no theory uses but which is parsed so that a solver reports it; each theory decides which kinds it accepts.
static interface	IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
static interface	IExpr.ILet	This interface represents an SMT-LIB let-expression
static interface	IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
static interface	IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
static interface	IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
static interface	IExpr.IStringLiteral	This interface represents SMT-LIB string literals
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().

Fields in org.smtlib declared as IExpr

Modifier and Type	Field	Description
IExpr	SymbolTable.Entry.definition	The definition of the symbol, if any
IExpr	TypeChecker.Variable.expression
protected IExpr	TypeChecker.quantifierBody	The body of the innermost quantifier being checked (the only place a :pattern may appear), or null.

Methods in org.smtlib that return IExpr

Modifier and Type	Method	Description
IExpr	IExpr.IMatchCase.body()
IExpr	ICommand.Iassert.expr()	Returns the expression to be asserted.
IExpr	IExpr.IAttributedExpr.expr()
IExpr	IExpr.IBinding.expr()
IExpr	IExpr.IExists.expr()
IExpr	IExpr.IForall.expr()
IExpr	IExpr.ILambda.expr()
IExpr	IExpr.ILet.expr()
IExpr	IExpr.IMatch.expr()
IExpr	ICommand.Idefine_fun_rec.expression()	Returns the defining expression (body).
IExpr	ICommand.Idefine_fun.expression()	Returns the defining expression (body).
IExpr	IParser.parseExpr()	Parses a term or formula; return null and log an error response if there is no term or formula

Methods in org.smtlib that return types with arguments of type IExpr

Modifier and Type	Method	Description
List<IExpr>	IExpr.IFcnExpr.args()	The arguments of the function
List<IExpr>	IResponse.IAssertionsResponse.assertions()
List<IExpr>	IResponse.IUnsatAssumptionsResponse.assumptions()
List<IExpr>	ICommand.Idefine_funs_rec.bodies()	Returns the list of defining expressions (bodies), parallel to ICommand.Idefine_funs_rec.declarations().
List<IExpr>	ICommand.Iget_value.exprs()	Returns the list of expressions whose values are requested.
default List<IExpr>	IParser.parseListTerms(Parser p)	Parses a parenthesized list of terms from the given parser.
List<IExpr>	ICommand.Icheck_sat_assuming.terms()	Returns the boolean-sorted terms to assume.
List<IExpr>	IExpr.IPatternTerms.terms()
protected List<IExpr>	AbstractSolver.unsatAssumptionsElements(List<IExpr> reply)	The elements of a get-unsat-assumptions reply that belong in the response (all of them); an adapter whose solver's reply holds others filters them out
protected List<IExpr>	AbstractSolver.unsatCoreElements(List<IExpr> reply)	The elements of a get-unsat-core reply that belong in the unsat core (all of them); an adapter whose solver's reply holds others filters them out
List<IResponse.IPair<IExpr,IExpr>>	IResponse.IValueResponse.values()
List<IResponse.IPair<IExpr,IExpr>>	IResponse.IValueResponse.values()

Methods in org.smtlib with parameters of type IExpr

Modifier and Type	Method	Description
ICommand.Iassert	ICommand.IFactory.assertCommand(IExpr expr)	Creates an assert command object, asserting the given expression.
IResponse	AbstractSolver.assertExpr(IExpr sexpr)
IResponse	ISolver.assertExpr(IExpr expr)	Adds the given expression to the current assertion-stack frame.
IExpr.IAttributedExpr	IExpr.IFactory.attributedExpr(IExpr e, List<IExpr.IAttribute<?>> attributes)	Creates an attributed expression (an expression with a positive number of attributes).
<T extends IAttributeValue> IExpr.IAttributedExpr	IExpr.IFactory.attributedExpr(IExpr e, IExpr.IKeyword key, T value)	Creates an attributed expression with just one attribute.
IExpr.IBinding	IExpr.IFactory.binding(IExpr.ISymbol symbol, IExpr expr)	Creates a binding for a Let expression.
static List<IResponse>	TypeChecker.check(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an IExpr (expected to be a Bool)
IResponse	AbstractSolver.check_sat_assuming(IExpr... exprs)
IResponse	ISolver.check_sat_assuming(IExpr... exprs)	Checks satisfiability under the current assertion set plus the given propositional assumptions.
static List<IResponse>	TypeChecker.checkAssertion(SymbolTable symTable, IExpr expr)	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).
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
void	ILanguage.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)	Checks whether the given function declaration is permitted in the language, throwing an exception if not
static List<IResponse>	TypeChecker.checkFcnRec(SymbolTable symTable, boolean global, IExpr.ISymbol id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)	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.
protected boolean	TypeChecker.checkPatternTerm(IExpr t)	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.
static List<IResponse>	TypeChecker.checkTerm(SymbolTable symTable, IExpr expr)	Type-checks a term of any sort (e.g.
static void	TypeChecker.clearSorts(IExpr expr)	Walks the given expression subtree, nulling out the sort recorded on each node (e.g.
ICommand.Idefine_const	ICommand.IFactory.define_const(IExpr.ISymbol symbol, ISort resultSort, IExpr expression)	Creates a define-const command object.
ICommand.Idefine_fun	ICommand.IFactory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun command object.
ICommand.Idefine_fun_rec	ICommand.IFactory.define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun-rec command object.
IExpr.IExists	IExpr.IFactory.exists(List<IExpr.IDeclaration> params, IExpr e)	Creates an Exists expression.
IExpr.IExists	IExpr.IFactory.exists(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IExpr.IFcnExpr	IExpr.IFactory.fcn(IExpr.IQualifiedIdentifier id, IExpr... args)	Creates a function expression (perhaps with an empty argument list).
IExpr.IForall	IExpr.IFactory.forall(List<IExpr.IDeclaration> params, IExpr e)	Creates a Forall expression.
IExpr.IForall	IExpr.IFactory.forall(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates a Forall expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IResponse	AbstractSolver.get_value(IExpr... terms)
IResponse	ISolver.get_value(IExpr... terms)	Returns the values of the given expressions in the current satisfying model.
IExpr.ILambda	IExpr.IFactory.lambda(List<IExpr.IDeclaration> params, IExpr e)	Creates a Lambda expression (SMT-LIB 2.7ff, HO-Core theory).
IExpr.ILet	IExpr.IFactory.let(List<IExpr.IBinding> bindings, IExpr e)	Creates a Let expression.
IExpr.IMatch	IExpr.IFactory.match(IExpr expr, List<IExpr.IMatchCase> cases)	Creates a match expression.
IExpr.IMatchCase	IExpr.IFactory.matchCase(IExpr.IPattern pattern, IExpr body)	Creates a single match case.
protected String	TypeChecker.pr(IExpr e)	Utility method for printing an expression, using the default printer
ISort	TypeChecker.save(IExpr e, ISort s)
void	ILanguage.validExpression(IExpr expression)	Checks whether the given expression is permitted in the language, throwing an exception if not

Method parameters in org.smtlib with type arguments of type IExpr

Modifier and Type	Method	Description
ICommand.Icheck_sat_assuming	ICommand.IFactory.check_sat_assuming(List<IExpr> terms)	Creates a check-sat-assuming command object.
IExpr.IFcnExpr	IExpr.IFactory.fcn(IExpr.IQualifiedIdentifier id, List<IExpr> args)	Creates a function expression (perhaps with an empty argument list).
IResponse.IAssertionsResponse	IResponse.IFactory.get_assertions_response(List<IExpr> exprs)
IResponse.IUnsatAssumptionsResponse	IResponse.IFactory.get_unsat_assumptions_response(List<IExpr> assumptions)
ICommand.Iget_value	ICommand.IFactory.get_value(List<IExpr> exprs)	Creates a get-value command object.
IResponse.IValueResponse	IResponse.IFactory.get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
IResponse.IValueResponse	IResponse.IFactory.get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
IExpr.IPatternTerms	IExpr.IFactory.patternTerms(List<IExpr> terms)	Creates the value of a :pattern attribute: the given terms as one (multi-)pattern.
protected List<IExpr>	AbstractSolver.unsatAssumptionsElements(List<IExpr> reply)	The elements of a get-unsat-assumptions reply that belong in the response (all of them); an adapter whose solver's reply holds others filters them out
protected List<IExpr>	AbstractSolver.unsatCoreElements(List<IExpr> reply)	The elements of a get-unsat-core reply that belong in the unsat core (all of them); an adapter whose solver's reply holds others filters them out

Constructors in org.smtlib with parameters of type IExpr

Modifier	Constructor	Description
	Variable(IExpr.ISymbol sym, ISort sort, IExpr expr, boolean closed)

Uses of IExpr in org.smtlib.command

Fields in org.smtlib.command declared as IExpr

Modifier and Type	Field	Description
protected IExpr	C_define_fun.expression	The defining expression for the function
protected IExpr	C_assert.formula	The formula to assert

Fields in org.smtlib.command with type parameters of type IExpr

Modifier and Type	Field	Description
protected List<IExpr>	C_define_funs_rec.bodies	The list of defining bodies, one per declaration
protected List<IExpr>	C_check_sat_assuming.terms	The boolean-sorted terms to assume.
protected List<IExpr>	C_get_value.terms	The terms whose values are to be gotten

Methods in org.smtlib.command that return IExpr

Modifier and Type	Method	Description
IExpr	C_assert.expr()	Returns the asserted formula
IExpr	C_define_fun.expression()	The defining expression for the function

Methods in org.smtlib.command that return types with arguments of type IExpr

Modifier and Type	Method	Description
List<IExpr>	C_define_funs_rec.bodies()
List<IExpr>	C_get_value.exprs()	The terms whose values are to be gotten
List<IExpr>	C_check_sat_assuming.terms()	Returns the boolean-sorted terms to assume.

Constructors in org.smtlib.command with parameters of type IExpr

Modifier	Constructor	Description
	C_assert(IExpr expr)	Constructs a command object given the expression to assert
	C_define_const(IExpr.ISymbol symbol, ISort resultSort, IExpr expression)	Constructs a command instance
	C_define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expr)	Constructs a command instance
	C_define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expr)	Constructs a command instance

Constructor parameters in org.smtlib.command with type arguments of type IExpr

Modifier	Constructor	Description
	C_check_sat_assuming(List<IExpr> terms)	Creates a check-sat-assuming command with the given assumption terms.
	C_get_value(List<IExpr> terms)	Constructs a command instance

Uses of IExpr in org.smtlib.impl

Classes in org.smtlib.impl that implement IExpr

Modifier and Type	Class	Description
static class	Pos.AbstractExpr	A Printable that also implements IExpr, additionally holding the sort computed for the expression by the type checker (null if not yet, or never, computed).
class	SMTExpr	This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
static class	SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
static class	SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
static class	SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
static class	SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
static class	SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
static class	SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
static class	SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
static class	SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
static class	SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
static class	SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
static class	SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
static class	SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
static class	SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
static class	SMTExpr.Symbol	This class represents an SMT Symbol

Fields in org.smtlib.impl declared as IExpr

Modifier and Type	Field	Description
protected IExpr	SMTExpr.MatchCase.body
protected IExpr	SMTExpr.AttributedExpr.expression
protected IExpr	SMTExpr.Binding.expression
protected IExpr	SMTExpr.Exists.expression
protected IExpr	SMTExpr.Forall.expression
protected IExpr	SMTExpr.Lambda.expression
protected IExpr	SMTExpr.Let.expression
protected IExpr	SMTExpr.Match.expression

Fields in org.smtlib.impl with type parameters of type IExpr

Modifier and Type	Field	Description
protected List<IExpr>	SMTExpr.FcnExpr.args
protected List<IExpr>	SMTExpr.PatternTerms.terms

Methods in org.smtlib.impl that return IExpr

Modifier and Type	Method	Description
IExpr	SMTExpr.MatchCase.body()
IExpr	SMTExpr.AttributedExpr.expr()
IExpr	SMTExpr.Binding.expr()
IExpr	SMTExpr.Exists.expr()
IExpr	SMTExpr.Forall.expr()
IExpr	SMTExpr.Lambda.expr()
IExpr	SMTExpr.Let.expr()
IExpr	SMTExpr.Match.expr()

Methods in org.smtlib.impl that return types with arguments of type IExpr

Modifier and Type	Method	Description
List<IExpr>	SMTExpr.FcnExpr.args()
List<IExpr>	Response.AssertionsResponse.assertions()
List<IExpr>	Response.UnsatAssumptionsResponse.assumptions()
List<IExpr>	SMTExpr.PatternTerms.terms()
List<IResponse.IPair<IExpr,IExpr>>	Response.ValueResponse.values()
List<IResponse.IPair<IExpr,IExpr>>	Response.ValueResponse.values()

Methods in org.smtlib.impl with parameters of type IExpr

Modifier and Type	Method	Description
ICommand.Iassert	Factory.assertCommand(IExpr expr)
IExpr.IAttributedExpr	Factory.attributedExpr(IExpr e, List<IExpr.IAttribute<?>> attributes)
<T extends IAttributeValue> IExpr.IAttributedExpr	Factory.attributedExpr(IExpr e, IExpr.IKeyword key, T value)
IExpr.IBinding	Factory.binding(IExpr.ISymbol symbol, IExpr expr)
void	SMTExpr.Logic.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
ICommand.Idefine_const	Factory.define_const(IExpr.ISymbol s, ISort r, IExpr e)
ICommand.Idefine_fun	Factory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)
ICommand.Idefine_fun_rec	Factory.define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)
IExpr.IExists	Factory.exists(List<IExpr.IDeclaration> params, IExpr e)
IExpr.IExists	Factory.exists(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)
IExpr.IFcnExpr	Factory.fcn(IExpr.IQualifiedIdentifier id, IExpr... args)
IExpr.IForall	Factory.forall(List<IExpr.IDeclaration> params, IExpr e)
IExpr.IForall	Factory.forall(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)
IExpr.ILambda	Factory.lambda(List<IExpr.IDeclaration> params, IExpr e)
IExpr.ILet	Factory.let(List<IExpr.IBinding> bindings, IExpr e)
IExpr.IMatch	Factory.match(IExpr expr, List<IExpr.IMatchCase> cases)
IExpr.IMatchCase	Factory.matchCase(IExpr.IPattern pattern, IExpr body)
void	SMTExpr.Logic.validExpression(IExpr expr)

Method parameters in org.smtlib.impl with type arguments of type IExpr

Modifier and Type	Method	Description
ICommand.Icheck_sat_assuming	Factory.check_sat_assuming(List<IExpr> terms)
IExpr.IFcnExpr	Factory.fcn(IExpr.IQualifiedIdentifier id, List<IExpr> args)
Response.AssertionsResponse	Response.Factory.get_assertions_response(List<IExpr> exprs)
Response.UnsatAssumptionsResponse	Response.Factory.get_unsat_assumptions_response(List<IExpr> assumptions)
ICommand.Iget_value	Factory.get_value(List<IExpr> exprs)
Response.ValueResponse	Response.Factory.get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
Response.ValueResponse	Response.Factory.get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
IExpr.IPatternTerms	Factory.patternTerms(List<IExpr> terms)

Constructors in org.smtlib.impl with parameters of type IExpr

Modifier	Constructor	Description
	AttributedExpr(IExpr expression, List<IExpr.IAttribute<?>> attributes)	Creates an attributed expression from the given base expression and attribute list.
	Binding(IExpr.ISymbol parameter, IExpr expr)	Creates a binding of the given symbol to the given expression.
	Exists(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates an exists expression with the given bound variable declarations and body.
	Forall(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates a forall expression with the given bound variable declarations and body.
	Lambda(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates a lambda expression with the given bound variable declarations and body.
	Let(List<IExpr.IBinding> bindings, IExpr expr)	Creates a let expression with the given bindings and body.
	Match(IExpr expr, List<IExpr.IMatchCase> cases)	Creates a match expression from the given scrutinee and list of cases.
	MatchCase(IExpr.IPattern pattern, IExpr body)	Creates a match case from the given pattern and body expression.

Constructor parameters in org.smtlib.impl with type arguments of type IExpr

Modifier	Constructor	Description
	AssertionsResponse(List<IExpr> assertions)
	FcnExpr(IExpr.IQualifiedIdentifier id, List<IExpr> args)	Creates a function application from the given identifier and argument list.
	PatternTerms(List<IExpr> terms)	Creates a pattern from the given (possibly empty) list of terms.
	UnsatAssumptionsResponse(List<IExpr> assumptions)
	ValueResponse(List<IResponse.IPair<IExpr,IExpr>> values)
	ValueResponse(List<IResponse.IPair<IExpr,IExpr>> values)

Uses of IExpr in org.smtlib.logic

Methods in org.smtlib.logic that return types with arguments of type IExpr

Modifier and Type	Method	Description
protected static List<IExpr>	Logic.nonCoefficients(IExpr.IFcnExpr e, Predicate<IExpr> isCoefficient)	The arguments of an application (of * or /) that are not coefficients.

Methods in org.smtlib.logic with parameters of type IExpr

Modifier and Type	Method	Description
protected abstract void	DifferenceLogic.checkAtom(IExpr.IFcnExpr atom, IExpr lhs, IExpr rhs)	Checks the arguments of a binary arithmetic atom (op lhs rhs).
protected void	QF_IDL.checkAtom(IExpr.IFcnExpr e, IExpr lhs, IExpr rhs)
protected void	QF_RDL.checkAtom(IExpr.IFcnExpr e, IExpr lhs, IExpr rhs)
protected void	Logic.checkBoundArraySorts(IExpr expression)	Checks the Array sorts of the variables bound by quantifiers in expression
void	ALL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFNIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_ABV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFBV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AX.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_BV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_EIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_FP.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_IDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_RDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UF.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFIDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFNRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFNIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
boolean	LRA.isConst(IExpr expr)
protected static boolean	DifferenceLogic.isDifferenceOfSymbols(IExpr e)	True for (- x y) with x and y symbols
boolean	Logic.isFreeConstant(IExpr expr)
boolean	Logic.isInteger(IExpr expr)
boolean	Logic.isLinearInteger(IExpr expr)
boolean	Logic.isLinearReal(IExpr expr)
boolean	Logic.isRealConst(IExpr expr)
void	Logic.noExponentiation(IExpr expression)
void	Logic.noFunctions(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	Logic.noQuantifiers(IExpr expression)
protected IVisitor.VisitorException	Logic.restrictionError(String message, IExpr e)	Builds a VisitorException for a restriction violation (e.g.
void	ALL.validExpression(IExpr expression)
void	AUFLIA.validExpression(IExpr expression)
void	AUFLIRA.validExpression(IExpr expression)
void	AUFNIRA.validExpression(IExpr expression)
void	DifferenceLogic.validExpression(IExpr expression)
void	LIA.validExpression(IExpr expression)
void	LRA.validExpression(IExpr expression)
void	QF_AUFLIA.validExpression(IExpr expression)
void	QF_AX.validExpression(IExpr expression)
void	QF_BV.validExpression(IExpr expression)
void	QF_EIA.validExpression(IExpr expression)
void	QF_FP.validExpression(IExpr expression)
void	QF_LIA.validExpression(IExpr expression)
void	QF_LRA.validExpression(IExpr expression)
void	QF_NIA.validExpression(IExpr expression)
void	QF_NRA.validExpression(IExpr expression)
void	QF_UF.validExpression(IExpr expression)
void	QF_UFIDL.validExpression(IExpr expression)	QF_UFIDL's :language: no quantifiers; Int symbols as above; and "for every term of the form (op t1 t2) with op in {+, -}, at least one of t1 and t2 is a numeral".
void	QF_UFLIA.validExpression(IExpr expression)
void	QF_UFLRA.validExpression(IExpr expression)
void	UFNIA.validExpression(IExpr expression)

Method parameters in org.smtlib.logic with type arguments of type IExpr

Modifier and Type	Method	Description
protected static List<IExpr>	Logic.nonCoefficients(IExpr.IFcnExpr e, Predicate<IExpr> isCoefficient)	The arguments of an application (of * or /) that are not coefficients.

Uses of IExpr in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return IExpr

Modifier and Type	Method	Description
IExpr	Parser.parseExpr()	Parses an expression, returning null with error messages if there is not a valid expression in the token stream.

Methods in org.smtlib.sexpr that return types with arguments of type IExpr

Modifier and Type	Method	Description
List<IExpr>	Parser.parseAssertionList()	Parses a parenthesized list of terms, as returned by a get-assertions response.
List<IExpr>	Parser.parseTermList()	Parses a parenthesized list of terms, as returned by a get-unsat-assumptions response.
List<IResponse.IPair<IExpr,IExpr>>	Parser.parseValueList()	Parses a parenthesized list of (term value) pairs, as returned by a get-value response.
List<IResponse.IPair<IExpr,IExpr>>	Parser.parseValueList()	Parses a parenthesized list of (term value) pairs, as returned by a get-value response.
IResponse.IPair<IExpr,IExpr>	Parser.parseValuePair()	Parses one (term value) pair, as found in a get-value response.
IResponse.IPair<IExpr,IExpr>	Parser.parseValuePair()	Parses one (term value) pair, as found in a get-value response.

Uses of IExpr in org.smtlib.solvers

Fields in org.smtlib.solvers with type parameters of type IExpr

Modifier and Type	Field	Description
protected List<List<IExpr>>	Solver_simplify.assertionSetStack	The data structure that maintains this class's own local simulation of the solver's assertion set stack -- see Solver_test.assertionSetStack.
protected List<List<IExpr>>	Solver_test.assertionSetStack	The solver's assertion set stack, one frame per push level, top first.

Methods in org.smtlib.solvers with type parameters of type IExpr

Modifier and Type	Method	Description
protected <T extends IExpr> void	Solver_z3_4_3.Translator.leftassoc(String fcnname, int length, Iterator<T> iter)

Methods in org.smtlib.solvers that return types with arguments of type IExpr

Modifier and Type	Method	Description
protected List<IExpr>	Solver_z3_recent.unsatAssumptionsElements(List<IExpr> reply)	Drops the labels z3 adds to the unsat assumptions (see Assumptions)
protected List<IExpr>	Solver_z3_4_3.unsatCoreElements(List<IExpr> reply)	Drops the assumptions z3 4.3 adds to the unsat core after check-sat-assuming
protected List<IExpr>	Solver_z3_recent.unsatCoreElements(List<IExpr> reply)	Drops the assumptions z3 adds to the unsat core (see Assumptions)

Methods in org.smtlib.solvers with parameters of type IExpr

Modifier and Type	Method	Description
IResponse	Solver_bitwuzla.assertExpr(IExpr sexpr)
IResponse	Solver_simplify.assertExpr(IExpr expr)
IResponse	Solver_test.assertExpr(IExpr expr)
IResponse	Solver_z3_4_3.assertExpr(IExpr sexpr)
IResponse	Solver_bitwuzla.check_sat_assuming(IExpr... exprs)
IResponse	Solver_simplify.check_sat_assuming(IExpr... exprs)	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.
IResponse	Solver_test.check_sat_assuming(IExpr... exprs)
IResponse	Solver_z3_4_3.check_sat_assuming(IExpr... exprs)	z3 4.3 answers unsupported for check-sat-assuming, so it is sent as z3's legacy (check-sat a1 ...
IResponse	Solver_z3_recent.check_sat_assuming(IExpr... exprs)
IResponse	Solver_altergo.get_value(IExpr... terms)	Alt-Ergo ignores get-value, writing nothing; answered unsupported without sending it
IResponse	Solver_bitwuzla.get_value(IExpr... terms)	With :produce-models on, Bitwuzla writes nothing for get-value unless its last check returned sat, and a fragment and an error if an assert, push, pop or reset-assertions came since or the option was set after the check.
IResponse	Solver_cvc5.get_value(IExpr... terms)	cvc5 answers get-value in assert mode after a check
IResponse	Solver_simplify.get_value(IExpr... terms)	See Solver_test.get_value(IExpr...).
IResponse	Solver_smtinterpol.get_value(IExpr... terms)	SMTInterpol answers get-value with :produce-models off, and in assert mode after a check
IResponse	Solver_test.get_value(IExpr... terms)
IResponse	Solver_yices2.get_value(IExpr... terms)	yices2 answers get-value with :produce-models off, and in assert mode after a check
IResponse	Solver_z3_4_3.get_value(IExpr... terms)	See get_model: z3 4.3 defaults :produce-models to true
IResponse	Solver_z3_recent.get_value(IExpr... terms)	z3 answers get-value in assert mode after a check
String	Solver_simplify.translate(IExpr expr)

Method parameters in org.smtlib.solvers with type arguments of type IExpr

Modifier and Type	Method	Description
protected List<IExpr>	Solver_z3_recent.unsatAssumptionsElements(List<IExpr> reply)	Drops the labels z3 adds to the unsat assumptions (see Assumptions)
protected List<IExpr>	Solver_z3_4_3.unsatCoreElements(List<IExpr> reply)	Drops the assumptions z3 4.3 adds to the unsat core after check-sat-assuming
protected List<IExpr>	Solver_z3_recent.unsatCoreElements(List<IExpr> reply)	Drops the assumptions z3 adds to the unsat core (see Assumptions)