Package org.smtlib.command

package 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.

Related Packages

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.ext	This package contains commands that are extensions to SMT-LIB.
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.

Classes

Class	Description
C_assert	Implements the assert command
C_check_sat	Implements the check-sat command
C_check_sat_assuming	Implements the check-sat-assuming command
C_comment	A synthetic pseudo-command representing a comment that appeared immediately before a real command in a script -- not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand.Icomment (see issue #115) rather than a generic ICommand, so execution, typed-visitor traversal, and printing all dispatch to it the same way every other command does, with no reflection-based or generic-fallback special case.
C_declare_const	Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
C_declare_datatype	Implements the declare-datatype command
C_declare_datatypes	Implements the declare-datatypes command
C_declare_fun	Implements the declare-fun command
C_declare_sort	Implements the declare-sort command
C_declare_sort_parameter	Implements the declare-sort-parameter command
C_define_const	Implements the define-const command: syntactic sugar for define-fun with no parameters
C_define_fun	Implements the define-fun command
C_define_fun_rec	Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.
C_define_funs_rec	Implements the define-funs-rec command
C_define_sort	Implements the define-sort command
C_echo	Implements the echo command
C_exit	Implements the exit command
C_get_assertions	Implements the get-assertions command
C_get_assignment	Implements the get-assignment command
C_get_info	Implements the get-info command.
C_get_model	Implements the get-model command
C_get_option	Implements the get-option command
C_get_proof	Implements the get-proof command
C_get_unsat_assumptions	Implements the get-unsat-assumptions command
C_get_unsat_core	Implements the get-unsat-core command
C_get_value	Implements the get-value command
C_pop	Implements the pop command
C_push	Implements the push command
C_reset	Implements the reset command
C_reset_assertions	Implements the reset-assertions command
C_set_info	Implements the set-info command
C_set_logic	Implements the set-logic command.
C_set_option	Implements the set-option command