Package org.smtlib

Interface IResponse.IFactory

All Known Implementing Classes:

Response.Factory

Enclosing interface:

IResponse

public static interface IResponse.IFactory

The factory interface for creating the standard IResponse singleton and structured instances.

Method Summary

Modifier and Type	Method	Description
IExpr.ISymbol	constant(String id)	Returns a constant response with the given canonical name
IResponse	continued_execution()
IResponse	empty()
IResponse.IError	error(String msg)
IResponse.IError	error(String msg, IPos pos)
IResponse.IAssertionsResponse	get_assertions_response(List<IExpr> exprs)
IResponse.IAssignmentResponse	get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)
IResponse.IAttributeList	get_info_response(List<IExpr.IAttribute<?>> attrList)
IResponse.IAttributeList	get_info_response(IExpr.IAttribute<?> attr)
IResponse	get_option_response(IAttributeValue v)
IResponse.IProofResponse	get_proof_response(ISexpr proof)
IResponse.IUnsatAssumptionsResponse	get_unsat_assumptions_response(List<IExpr> assumptions)
IResponse.IUnsatCoreResponse	get_unsat_core_response(List<IExpr.ISymbol> names)
IResponse.IValueResponse	get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
IResponse	immediate_exit()
IResponse	incomplete()
IResponse	memout()
IResponse	numericLiteral(int value)
<T1, T2> IResponse.IPair<T1,T2>	pair(T1 first, T2 second)
IResponse	sat()
IResponse	stringLiteral(String value)	The argument has no SMT-LIB escapes and no enclosing quotes
IResponse	success()
IResponse	timeout()	The response when the solver's whole-run time limit (SMT.Configuration#timeoutTotal) ended it, normalized across solvers (z3 answers 'timeout' and exits; cvc5 reports the timeout on stderr and aborts); every later command to that solver gets the same response.
IResponse	unknown()
IResponse	unsat()
IResponse	unsupported()

Method Details

error

IResponse.IError error(String msg)

error

IResponse.IError error(String msg,
 IPos pos)

empty

IResponse empty()

success

IResponse success()

unsupported

IResponse unsupported()

unknown

IResponse unknown()

sat

IResponse sat()

unsat

IResponse unsat()

immediate_exit

IResponse immediate_exit()

continued_execution

IResponse continued_execution()

memout

IResponse memout()

timeout

IResponse timeout()

The response when the solver's whole-run time limit (SMT.Configuration#timeoutTotal) ended it, normalized across solvers (z3 answers 'timeout' and exits; cvc5 reports the timeout on stderr and aborts); every later command to that solver gets the same response. Not standard SMT-LIB.

incomplete

IResponse incomplete()

constant

IExpr.ISymbol constant(String id)

Returns a constant response with the given canonical name

stringLiteral

IResponse stringLiteral(String value)

The argument has no SMT-LIB escapes and no enclosing quotes

numericLiteral

IResponse numericLiteral(int value)

get_option_response

IResponse get_option_response(IAttributeValue v)

get_info_response

IResponse.IAttributeList get_info_response(IExpr.IAttribute<?> attr)

get_info_response

IResponse.IAttributeList get_info_response(List<IExpr.IAttribute<?>> attrList)

get_proof_response

IResponse.IProofResponse get_proof_response(ISexpr proof)

get_value_response

IResponse.IValueResponse get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)

pair

<T1,
T2> IResponse.IPair<T1,T2> pair(T1 first,
 T2 second)

get_assignment_response

IResponse.IAssignmentResponse get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)

get_unsat_assumptions_response

IResponse.IUnsatAssumptionsResponse get_unsat_assumptions_response(List<IExpr> assumptions)

get_unsat_core_response

IResponse.IUnsatCoreResponse get_unsat_core_response(List<IExpr.ISymbol> names)

get_assertions_response

IResponse.IAssertionsResponse get_assertions_response(List<IExpr> exprs)