Constant Field Values

Contents

• org.smtlib.*

org.smtlib.*

org.smtlib.AbstractSolver

Modifier and Type	Constant Field	Value
protected static final long	END_WAIT_MILLIS	2000L
public static final String	SOLVER_EXITED	"The solver process has exited"

org.smtlib.CharSequenceInfinite

Modifier and Type	Constant Field	Value
public static final char	endChar	'\u0019'

org.smtlib.SolverCapabilities

Modifier and Type	Constant Field	Value
public static final String	PROPS_CAPABILITIES_SUFFIX	".capabilities"

org.smtlib.Utils

Modifier and Type	Constant Field	Value
public static final String	AS	"as"
public static final String	AUTHORS_VALUE	"David R. Cok"
public static final String	BITVEC	"BitVec"
public static final String	CONTINUED_EXECUTION	"continued-execution"
public static final String	CORE	"Core"
public static final String	DIAGNOSTIC_OUTPUT_CHANNEL	":diagnostic-output-channel"
public static final String	EXISTS	"exists"
public static final String	EXPAND_DEFINITIONS	":expand-definitions"
public static final String	FLOATINGPOINT	"FloatingPoint"
public static final String	FORALL	"forall"
public static final String	GLOBAL_DECLARATIONS	":global-declarations"
public static final String	IMMEDIATE_EXIT	"immediate-exit"
public static final String	INCOMPLETE	"incomplete"
public static final String	INTERACTIVE_MODE	":interactive-mode"
public static final String	IS	"is"
public static final String	LET	"let"
public static final String	LOGIC	"logic"
public static final String	MEMOUT	"memout"
public static final String	NAME_VALUE	"SMT-LIB adapter"
public static final String	PAR	"par"
public static final String	PLUGIN_ID	"org.smtlib.SMT"
public static final String	PRINT_SUCCESS	":print-success"
public static final String	PRODUCE_ASSERTIONS	":produce-assertions"
public static final String	PRODUCE_ASSIGNMENTS	":produce-assignments"
public static final String	PRODUCE_MODELS	":produce-models"
public static final String	PRODUCE_PROOFS	":produce-proofs"
public static final String	PRODUCE_UNSAT_ASSUMPTIONS	":produce-unsat-assumptions"
public static final String	PRODUCE_UNSAT_CORES	":produce-unsat-cores"
public static final String	PROPS_ADAPTER_SUFFIX	".adapter"
public static final String	PROPS_COMMAND_SUFFIX	".command"
public static final String	PROPS_DEFAULT_SOLVER	"org.smtlib.default-solver"
public static final String	PROPS_EXEC_SUFFIX	".exec"
public static final String	PROPS_FILE	"jsmtlib.properties"
public static final String	PROPS_LOGIC_PATH	"org.smtlib.logic_path"
public static final String	PROPS_SOLVER_PREFIX	"org.smtlib.solver_"
public static final String	RANDOM_SEED	":random-seed"
public static final String	REGULAR_OUTPUT_CHANNEL	":regular-output-channel"
public static final String	REPRODUCIBLE_RESOURCE_LIMIT	":reproducible-resource-limit"
public static final String	STDERR	"stderr"
public static final String	STDOUT	"stdout"
public static final String	SUFFIX	".smt2"
public static final String	TEST_SOLVER	"test"
public static final String	THEORY	"theory"
public static final String	VERBOSITY	":verbosity"
public static final String	WILDCARD	"_"

org.smtlib.command.C_assert

Modifier and Type	Constant Field	Value
public static final String	commandName	"assert"

org.smtlib.command.C_check_sat

Modifier and Type	Constant Field	Value
public static final String	commandName	"check-sat"

org.smtlib.command.C_check_sat_assuming

Modifier and Type	Constant Field	Value
public static final String	commandName	"check-sat-assuming"

org.smtlib.command.C_comment

Modifier and Type	Constant Field	Value
public static final String	commandName	"<comment>"

org.smtlib.command.C_declare_const

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-const"

org.smtlib.command.C_declare_datatype

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-datatype"

org.smtlib.command.C_declare_datatypes

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-datatypes"

org.smtlib.command.C_declare_fun

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-fun"

org.smtlib.command.C_declare_sort

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-sort"

org.smtlib.command.C_declare_sort_parameter

Modifier and Type	Constant Field	Value
public static final String	commandName	"declare-sort-parameter"

org.smtlib.command.C_define_const

Modifier and Type	Constant Field	Value
public static final String	commandName	"define-const"

org.smtlib.command.C_define_fun

Modifier and Type	Constant Field	Value
public static final String	commandName	"define-fun"

org.smtlib.command.C_define_fun_rec

Modifier and Type	Constant Field	Value
public static final String	commandName	"define-fun-rec"

org.smtlib.command.C_define_funs_rec

Modifier and Type	Constant Field	Value
public static final String	commandName	"define-funs-rec"

org.smtlib.command.C_define_sort

Modifier and Type	Constant Field	Value
public static final String	commandName	"define-sort"

org.smtlib.command.C_echo

Modifier and Type	Constant Field	Value
public static final String	commandName	"echo"

org.smtlib.command.C_exit

Modifier and Type	Constant Field	Value
public static final String	commandName	"exit"

org.smtlib.command.C_get_assertions

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-assertions"

org.smtlib.command.C_get_assignment

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-assignment"

org.smtlib.command.C_get_info

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-info"

org.smtlib.command.C_get_model

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-model"

org.smtlib.command.C_get_option

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-option"

org.smtlib.command.C_get_proof

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-proof"

org.smtlib.command.C_get_unsat_assumptions

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-unsat-assumptions"

org.smtlib.command.C_get_unsat_core

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-unsat-core"

org.smtlib.command.C_get_value

Modifier and Type	Constant Field	Value
public static final String	commandName	"get-value"

org.smtlib.command.C_pop

Modifier and Type	Constant Field	Value
public static final String	commandName	"pop"

org.smtlib.command.C_push

Modifier and Type	Constant Field	Value
public static final String	commandName	"push"

org.smtlib.command.C_reset

Modifier and Type	Constant Field	Value
public static final String	commandName	"reset"

org.smtlib.command.C_reset_assertions

Modifier and Type	Constant Field	Value
public static final String	commandName	"reset-assertions"

org.smtlib.command.C_set_info

Modifier and Type	Constant Field	Value
public static final String	commandName	"set-info"

org.smtlib.command.C_set_logic

Modifier and Type	Constant Field	Value
public static final String	commandName	"set-logic"

org.smtlib.command.C_set_option

Modifier and Type	Constant Field	Value
public static final String	commandName	"set-option"

org.smtlib.ext.C_exec

Modifier and Type	Constant Field	Value
public static final String	commandName	"exec"

org.smtlib.ext.C_what

Modifier and Type	Constant Field	Value
public static final String	commandName	"what"

org.smtlib.sexpr.Parser

Modifier and Type	Constant Field	Value
public static final String	UNEXPECTED_RESPONSE	"Unexpected response from the solver: "

org.smtlib.sexpr.Utils

Modifier and Type	Constant Field	Value
public static final String	AS	"as"
public static final String	ATTRIBUTE	"!"
public static final String	BINARY	"BINARY"
public static final String	DECIMAL	"DECIMAL"
public static final String	EXISTS	"exists"
public static final String	FORALL	"forall"
public static final String	HEXADECIMAL	"HEXADECIMAL"
public static final String	LAMBDA	"lambda"
public static final String	LET	"let"
public static final String	LOGIC	"logic"
public static final String	MATCH	"match"
public static final String	NUMERAL	"NUMERAL"
public static final String	PAR	"par"
public static final String	PARAM	"_"
public static final String	PATTERN	":pattern"
public static final String	STRING	"STRING"
public static final String	THEORY	"theory"
public static final String	WILDCARD	"_"