Package org.smtlib.impl

Class Response.Factory

java.lang.Object

org.smtlib.impl.Response.Factory

All Implemented Interfaces:

IResponse.IFactory

Enclosing class:

Response

public static class Response.Factory
extends Object
implements IResponse.IFactory

Implements the IResponse.IFactory interface

Field Summary

Fields

Modifier and Type	Field	Description
boolean	printSuccess

Constructor Summary

Constructors

Constructor	Description
Factory(SMT.Configuration smtConfig)

Method Summary

Modifier and Type	Method	Description
IExpr.ISymbol	constant(String sym)	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)
Response.AssertionsResponse	get_assertions_response(List<IExpr> exprs)
Response.AssignmentResponse	get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)
IResponse.IAttributeList	get_info_response(List<IExpr.IAttribute<? extends IAttributeValue>> attributes)
IResponse.IAttributeList	get_info_response(IExpr.IAttribute<? extends IAttributeValue> attr)
IResponse	get_option_response(IAttributeValue v)
Response.ProofResponse	get_proof_response(ISexpr proof)
Response.UnsatAssumptionsResponse	get_unsat_assumptions_response(List<IExpr> assumptions)
Response.UnsatCoreResponse	get_unsat_core_response(List<IExpr.ISymbol> names)
Response.ValueResponse	get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)
IResponse	immediate_exit()
IResponse	incomplete()
IResponse	memout()
IExpr.INumeral	numericLiteral(int value)
<T1, T2> Response.Pair<T1,T2>	pair(T1 first, T2 second)
IResponse	sat()
IExpr.IStringLiteral	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()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

printSuccess

public boolean printSuccess

Constructor Details

Factory

public Factory(SMT.Configuration smtConfig)

Method Details

error

public IResponse.IError error(String msg)

Specified by:

error in interface IResponse.IFactory

error

public IResponse.IError error(String msg,
 IPos pos)

Specified by:

error in interface IResponse.IFactory

empty

public IResponse empty()

Specified by:

empty in interface IResponse.IFactory

success

public IResponse success()

Specified by:

success in interface IResponse.IFactory

unsupported

public IResponse unsupported()

Specified by:

unsupported in interface IResponse.IFactory

unknown

public IResponse unknown()

Specified by:

unknown in interface IResponse.IFactory

sat

public IResponse sat()

Specified by:

sat in interface IResponse.IFactory

unsat

public IResponse unsat()

Specified by:

unsat in interface IResponse.IFactory

immediate_exit

public IResponse immediate_exit()

Specified by:

immediate_exit in interface IResponse.IFactory

continued_execution

public IResponse continued_execution()

Specified by:

continued_execution in interface IResponse.IFactory

memout

public IResponse memout()

Specified by:

memout in interface IResponse.IFactory

timeout

public IResponse timeout()

Description copied from interface: IResponse.IFactory

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.

Specified by:

timeout in interface IResponse.IFactory

incomplete

public IResponse incomplete()

Specified by:

incomplete in interface IResponse.IFactory

constant

public IExpr.ISymbol constant(String sym)

Description copied from interface: IResponse.IFactory

Returns a constant response with the given canonical name

Specified by:

constant in interface IResponse.IFactory

stringLiteral

public IExpr.IStringLiteral stringLiteral(String value)

Description copied from interface: IResponse.IFactory

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

Specified by:

stringLiteral in interface IResponse.IFactory

numericLiteral

public IExpr.INumeral numericLiteral(int value)

Specified by:

numericLiteral in interface IResponse.IFactory

get_info_response

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

Specified by:

get_info_response in interface IResponse.IFactory

get_info_response

public IResponse.IAttributeList get_info_response(List<IExpr.IAttribute<? extends IAttributeValue>> attributes)

Specified by:

get_info_response in interface IResponse.IFactory

pair

public <T1,
T2> Response.Pair<T1,T2> pair(T1 first,
 T2 second)

Specified by:

pair in interface IResponse.IFactory

get_option_response

public IResponse get_option_response(IAttributeValue v)

Specified by:

get_option_response in interface IResponse.IFactory

get_proof_response

public Response.ProofResponse get_proof_response(ISexpr proof)

Specified by:

get_proof_response in interface IResponse.IFactory

get_value_response

public Response.ValueResponse get_value_response(List<IResponse.IPair<IExpr,IExpr>> values)

Specified by:

get_value_response in interface IResponse.IFactory

get_assignment_response

public Response.AssignmentResponse get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)

Specified by:

get_assignment_response in interface IResponse.IFactory

get_unsat_assumptions_response

public Response.UnsatAssumptionsResponse get_unsat_assumptions_response(List<IExpr> assumptions)

Specified by:

get_unsat_assumptions_response in interface IResponse.IFactory

get_unsat_core_response

public Response.UnsatCoreResponse get_unsat_core_response(List<IExpr.ISymbol> names)

Specified by:

get_unsat_core_response in interface IResponse.IFactory

get_assertions_response

public Response.AssertionsResponse get_assertions_response(List<IExpr> exprs)

Specified by:

get_assertions_response in interface IResponse.IFactory