Package org.smtlib.sexpr

package org.smtlib.sexpr

This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics. In particular, it implements a Parser (which converts concrete to abstract) and a Printer (which converts abstract to concrete).

The particular concrete syntax implemented by the Parser and the Printer is the S-expression syntax described in the SMT-LIB v.2 documentation. In this syntax, all abstract quantities are rendered as S-expressions: either individual tokens, or a sequence consisting of a left-parenthesis, a series of whitespace-separated S-expressions, and a closing right-parenthesis. The whitespace separating a series of S-expressions may be spaces, tabs, new-line or carriage-return characters.

The allowed tokens are

• numeral - either a '0' or a sequence of digits starting with a non-zero digit
• decimal - a numeral followed by a period followed by a sequence of digits
• binary literal - the characters '#b' followed by a sequence of '0' and '1' digits
• hex literal - the characters '#x' followed by a sequence of upper- or lower-case hex digits
• string literal - a '"'-enclosed sequence of printable characters, with a backslash included as '\\' and an embedded quote as '\"'
• symbol - a sequence, starting with a non-digit, of digits, upper and lower case letters and these punctuation characters: +-*/_=%?!.$~&^<>@ Some character sequences that would be symbols are instead reserved words.
• quoted symbol - a sequence of any printable or whitespace characters beginning and ending with vertical bars (|).
• keywords - a colon followed by a sequence of printable characters allowed in unquoted symbols
• reserved words - some character sequences are reserved and not allowed to be used as symbols. These are
  forall exists let as _ ! par NUMERAL DECIMAL STRING
  and the pre-defined commands:
  assert check-sat declare-fun declare-sort define-fun define-sort exit get-assertions get-assignment get-info get_option get-proof get-unsat-core get-value pop push set-info set-logic set-option

A command has the form ( command-name <reserved-word arguments... )
in which the command-name is a symbol or reserved word naming the command and the arguments are also S-expressions of particular forms, depending on the command.

The logical formulas that are asserted and reasoned about by an SMT solver also are S-expressions. An expression can in general take one of the following forms, though the particular logic in effect may limit some of the syntax and will specify which functions are defined:

• a numeral, decimal, binary, hex, or string literal
• a symbol (including quoted symbols), both of which are simple forms of identifiers
• a parameterized identifier: ( _ symbol series-of-numerals )
• a function evaluation: ( identifier arguments... )
• a named expression: ( ! expression :named symbol )
• universal quantification: ( forall ( series-of-symbol-sort-pairs ) expression )
• existential quantification: ( exists ( series-of-symbol-sort-pairs ) expression )
• let expression: ( let ( series-of-symbol-expression-pairs ) expression )

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

Class	Description
Factory	This is the factory for classes that are part of this particular concrete representation of SMT-LIB syntax: Parser, Printer, Source for parsers.
ILexToken	An interface to indicate AST classes that are also lexical tokens in the concrete syntax.
ISexpr	This interface represents S-expressions as used in SMT-LIB; they are used as values for attributes in the standard concrete syntax.
ISexpr.ISeq	Represents a sequence of S-expressions
ISexpr.IToken<T>	Represents a single S-expression token
Lexer	Converts character sequences (from ISource) into tokens, presuming the standard SMT-LIBv2 concrete syntax.
Lexer.IPLexToken	An interface used for punctuation tokens that can be retrieved from the parser input.
Parser	Parses the standard SMT-LIB concrete syntax to produce ASTs of objects that are instances of the org.smtlib.* interfaces.
Printer	This class writes out SMT-LIB ASTs as concrete S-expression syntax; aside from white space between tokens it should simply reverse what the Parser class does.
Printer.PrintArgs	Functional interface for the argument-printing lambda passed to Printer.printCommand(org.smtlib.ICommand, org.smtlib.sexpr.Printer.PrintArgs).
Printer.WithLines
Sexpr	This is the root class for S-expressions in the concrete syntax
Sexpr.Seq	The class corresponding to sequences of S-expressions
Sexpr.Token<T>	Represents a single S-expression token with intrinsic type T
Utils	Constants and reserved-word sets specific to the S-expression concrete syntax.