Package org.smtlib

Interface ICommand.IFactory

All Known Implementing Classes:

Factory

Enclosing interface:

ICommand

public static interface ICommand.IFactory

This is the interface to be used by a concrete ICommand factory.

Method Summary

Modifier and Type	Method	Description
ICommand.Iassert	assertCommand(IExpr expr)	Creates an assert command object, asserting the given expression.
ICommand.Icheck_sat	check_sat()	Creates a check-sat command object.
ICommand.Icheck_sat_assuming	check_sat_assuming(List<IExpr> terms)	Creates a check-sat-assuming command object.
ICommand.Icomment	comment(String text)	Creates a comment pseudo-command object, carrying the given raw comment text (see ICommand.Icomment).
ICommand.Ideclare_const	declare_const(IExpr.ISymbol symbol, ISort resultSort)	Creates a declare-const command object.
ICommand.Ideclare_datatype	declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)	Creates a declare-datatype command object.
ICommand.Ideclare_datatypes	declare_datatypes(List<IExpr.ISortDeclaration> sds, List<ISort.IDatatype> dts)	Creates a declare-datatypes command object.
ICommand.Ideclare_fun	declare_fun(IExpr.ISymbol id, List<ISort> argSorts, ISort resultSort)	Creates a declare-fun command object.
ICommand.Ideclare_sort	declare_sort(IExpr.ISymbol sym, IExpr.INumeral arity)	Creates a declare-sort command object.
ICommand.Ideclare_sort_parameter	declare_sort_parameter(IExpr.ISymbol sym)	Creates a declare-sort-parameter command object.
ICommand.Idefine_const	define_const(IExpr.ISymbol symbol, ISort resultSort, IExpr expression)	Creates a define-const command object.
ICommand.Idefine_fun	define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun command object.
ICommand.Idefine_fun_rec	define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun-rec command object.
ICommand.Idefine_funs_rec	define_funs_rec(List<IExpr.IFunctionDeclaration> declarations, List<IExpr> bodies)	Creates a define-funs-rec command object.
ICommand.Idefine_sort	define_sort(IExpr.ISymbol id, List<ISort.IParameter> parameters, ISort expression)	Creates a define-sort command object.
ICommand.Iecho	echo(IExpr.IStringLiteral arg)	Creates an echo command object.
ICommand.Iexit	exit()	Creates an exit command object.
ICommand.Iget_assertions	get_assertions()	Creates a get-assertions command object.
ICommand.Iget_assignment	get_assignment()	Creates a get-assignment command object.
ICommand.Iget_info	get_info(IExpr.IKeyword infoflag)	Creates a get-info command object.
ICommand.Iget_model	get_model()	Creates a get-model command object.
ICommand.Iget_option	get_option(IExpr.IKeyword option)	Creates a get-option command object.
ICommand.Iget_proof	get_proof()	Creates a get-proof command object.
ICommand.Iget_unsat_assumptions	get_unsat_assumptions()	Creates a get-unsat-assumptions command object.
ICommand.Iget_unsat_core	get_unsat_core()	Creates a get-unsat-core command object.
ICommand.Iget_value	get_value(List<IExpr> exprs)	Creates a get-value command object.
ICommand.Ipop	pop(IExpr.INumeral number)	Creates a pop command object.
ICommand.Ipush	push(IExpr.INumeral number)	Creates a push command object.
ICommand.Ireset	reset()	Creates a reset command object.
ICommand.Ireset_assertions	reset_assertions()	Creates a reset-assertions command object.
ICommand.IScript	script()	Creates an empty script, with no filename and no commands, ready to have commands added via ICommand.IScript.add(ICommand).
ICommand.IScript	script(IExpr.IStringLiteral filename, List<ICommand> commands)	Creates a script object containing the given filename or the given set of commands.
ICommand.Iset_info	set_info(IExpr.IKeyword infoflag, IAttributeValue value)	Creates a set-info command object.
ICommand.Iset_logic	set_logic(IExpr.ISymbol logic)	Creates a set-logic command object.
ICommand.Iset_option	set_option(IExpr.IKeyword option, IAttributeValue value)	Creates a set-option command object.

Method Details

script

ICommand.IScript script()

Creates an empty script, with no filename and no commands, ready to have commands added via ICommand.IScript.add(ICommand).

script

ICommand.IScript script(IExpr.IStringLiteral filename,
 List<ICommand> commands)

Creates a script object containing the given filename or the given set of commands.

assertCommand

ICommand.Iassert assertCommand(IExpr expr)

Creates an assert command object, asserting the given expression.

check_sat

ICommand.Icheck_sat check_sat()

Creates a check-sat command object.

check_sat_assuming

ICommand.Icheck_sat_assuming check_sat_assuming(List<IExpr> terms)

Creates a check-sat-assuming command object.

comment

ICommand.Icomment comment(String text)

Creates a comment pseudo-command object, carrying the given raw comment text (see ICommand.Icomment).

declare_const

ICommand.Ideclare_const declare_const(IExpr.ISymbol symbol,
 ISort resultSort)

Creates a declare-const command object.

declare_fun

ICommand.Ideclare_fun declare_fun(IExpr.ISymbol id,
 List<ISort> argSorts,
 ISort resultSort)

Creates a declare-fun command object.

declare_sort

ICommand.Ideclare_sort declare_sort(IExpr.ISymbol sym,
 IExpr.INumeral arity)

Creates a declare-sort command object.

declare_sort_parameter

ICommand.Ideclare_sort_parameter declare_sort_parameter(IExpr.ISymbol sym)

Creates a declare-sort-parameter command object.

declare_datatype

ICommand.Ideclare_datatype declare_datatype(IExpr.ISortDeclaration sd,
 ISort.IDatatype d)

Creates a declare-datatype command object.

declare_datatypes

ICommand.Ideclare_datatypes declare_datatypes(List<IExpr.ISortDeclaration> sds,
 List<ISort.IDatatype> dts)

Creates a declare-datatypes command object.

define_const

ICommand.Idefine_const define_const(IExpr.ISymbol symbol,
 ISort resultSort,
 IExpr expression)

Creates a define-const command object.

define_fun

ICommand.Idefine_fun define_fun(IExpr.ISymbol id,
 List<IExpr.IDeclaration> declarations,
 ISort resultSort,
 IExpr expression)

Creates a define-fun command object.

define_fun_rec

ICommand.Idefine_fun_rec define_fun_rec(IExpr.ISymbol id,
 List<IExpr.IDeclaration> declarations,
 ISort resultSort,
 IExpr expression)

Creates a define-fun-rec command object.

define_funs_rec

ICommand.Idefine_funs_rec define_funs_rec(List<IExpr.IFunctionDeclaration> declarations,
 List<IExpr> bodies)

Creates a define-funs-rec command object.

define_sort

ICommand.Idefine_sort define_sort(IExpr.ISymbol id,
 List<ISort.IParameter> parameters,
 ISort expression)

Creates a define-sort command object.

echo

ICommand.Iecho echo(IExpr.IStringLiteral arg)

Creates an echo command object.

exit

ICommand.Iexit exit()

Creates an exit command object.

get_assertions

ICommand.Iget_assertions get_assertions()

Creates a get-assertions command object.

get_assignment

ICommand.Iget_assignment get_assignment()

Creates a get-assignment command object.

get_info

ICommand.Iget_info get_info(IExpr.IKeyword infoflag)

Creates a get-info command object.

get_option

ICommand.Iget_option get_option(IExpr.IKeyword option)

Creates a get-option command object.

get_model

ICommand.Iget_model get_model()

Creates a get-model command object.

get_proof

ICommand.Iget_proof get_proof()

Creates a get-proof command object.

get_unsat_assumptions

ICommand.Iget_unsat_assumptions get_unsat_assumptions()

Creates a get-unsat-assumptions command object.

get_unsat_core

ICommand.Iget_unsat_core get_unsat_core()

Creates a get-unsat-core command object.

get_value

ICommand.Iget_value get_value(List<IExpr> exprs)

Creates a get-value command object.

push

ICommand.Ipush push(IExpr.INumeral number)

Creates a push command object.

pop

ICommand.Ipop pop(IExpr.INumeral number)

Creates a pop command object.

reset

ICommand.Ireset reset()

Creates a reset command object.

reset_assertions

ICommand.Ireset_assertions reset_assertions()

Creates a reset-assertions command object.

set_logic

ICommand.Iset_logic set_logic(IExpr.ISymbol logic)

Creates a set-logic command object.

set_info

ICommand.Iset_info set_info(IExpr.IKeyword infoflag,
 IAttributeValue value)

Creates a set-info command object.

set_option

ICommand.Iset_option set_option(IExpr.IKeyword option,
 IAttributeValue value)

Creates a set-option command object.