Package org.smtlib

Class Utils

java.lang.Object
org.smtlib.Utils
public class Utils extends Object
A class of static utility methods and constants for the SMT-LIB package.

  • Field Details

    • PROPS_FILE

      public static final String PROPS_FILE
      The name of the properties file read by jSMTLIB
      See Also:

    • PROPS_DEFAULT_SOLVER

      public static final String PROPS_DEFAULT_SOLVER
      The property name that specifies the default solver
      See Also:

    • PROPS_SOLVER_PREFIX

      public static final String PROPS_SOLVER_PREFIX
      The default prefix for the property names that identify solver executables, as in org.smtlib.solver_ZZZ
      See Also:

    • PROPS_ADAPTER_SUFFIX

      public static final String PROPS_ADAPTER_SUFFIX
      The suffix for adapter properties, as in org.smtlib.solver_ZZZ.adapter
      See Also:

    • PROPS_EXEC_SUFFIX

      public static final String PROPS_EXEC_SUFFIX
      The suffix for executable properties, as in org.smtlib.solver_ZZZ.exec
      See Also:

    • PROPS_COMMAND_SUFFIX

      public static final String PROPS_COMMAND_SUFFIX
      The suffix for command-line properties, as in org.smtlib.solver_ZZZ.command
      See Also:

    • PROPS_LOGIC_PATH

      public static final String PROPS_LOGIC_PATH
      The property giving the default logic path
      See Also:

    • TEST_SOLVER

      public static final String TEST_SOLVER
      The name of the test solver, implemented by this SMT app.
      See Also:

    • PLUGIN_ID

      public static final String PLUGIN_ID
      The ID of the core functionality plug-in
      See Also:

    • SUFFIX

      public static final String SUFFIX
      The suffix used for SMT-LIB files
      See Also:

    • CORE

      public static final String CORE
      Name of the Core theory
      See Also:

    • BITVEC

      public static final String BITVEC
      Name of the BitVector sort
      See Also:

    • INTERACTIVE_MODE

      public static final String INTERACTIVE_MODE
      The string designating an option item
      See Also:

    • PRODUCE_ASSERTIONS

      public static final String PRODUCE_ASSERTIONS
      The string designating an option item
      See Also:

    • GLOBAL_DECLARATIONS

      public static final String GLOBAL_DECLARATIONS
      The string designating an option item
      See Also:

    • RANDOM_SEED

      public static final String RANDOM_SEED
      The string designating an option item
      See Also:

    • REPRODUCIBLE_RESOURCE_LIMIT

      public static final String REPRODUCIBLE_RESOURCE_LIMIT
      The string designating an option item
      See Also:

    • VERBOSITY

      public static final String VERBOSITY
      The string designating an option item
      See Also:

    • EXPAND_DEFINITIONS

      public static final String EXPAND_DEFINITIONS
      The string designating an option item
      See Also:

    • REGULAR_OUTPUT_CHANNEL

      public static final String REGULAR_OUTPUT_CHANNEL
      The string designating an option item
      See Also:

    • DIAGNOSTIC_OUTPUT_CHANNEL

      public static final String DIAGNOSTIC_OUTPUT_CHANNEL
      The string designating an option item
      See Also:

    • PRODUCE_PROOFS

      public static final String PRODUCE_PROOFS
      The string designating an option item
      See Also:

    • PRODUCE_ASSIGNMENTS

      public static final String PRODUCE_ASSIGNMENTS
      The string designating an option item
      See Also:

    • PRODUCE_UNSAT_CORES

      public static final String PRODUCE_UNSAT_CORES
      The string designating an option item
      See Also:

    • PRODUCE_UNSAT_ASSUMPTIONS

      public static final String PRODUCE_UNSAT_ASSUMPTIONS
      The string designating an option item
      See Also:

    • PRODUCE_MODELS

      public static final String PRODUCE_MODELS
      The string designating an option item
      See Also:

    • startModeOptions

      public static final Set<String> startModeOptions
      The standard options that may be set only in start mode, i.e. before set-logic (SMT-LIB 2.7, 4.1.7)

    • ERROR_BEHAVIOR

      public static final IExpr.IKeyword ERROR_BEHAVIOR
      The string designating an info item

    • NAME

      public static final IExpr.IKeyword NAME
      The string designating an info item

    • AUTHORS

      public static final IExpr.IKeyword AUTHORS
      The string designating an info item

    • VERSION

      public static final IExpr.IKeyword VERSION
      The string designating an info item

    • STATUS

      public static final IExpr.IKeyword STATUS
      The string designating an info item

    • REASON_UNKNOWN

      public static final IExpr.IKeyword REASON_UNKNOWN
      The string designating an info item

    • ALL_STATISTICS

      public static final IExpr.IKeyword ALL_STATISTICS
      The string designating an info item

    • ASSERTION_STACK_LEVELS

      public static final IExpr.IKeyword ASSERTION_STACK_LEVELS
      The string designating an info item

    • AUTHORS_VALUE

      public static final String AUTHORS_VALUE
      The response to the :authors info item
      See Also:

    • NAME_VALUE

      public static final String NAME_VALUE
      The response to the :name info item
      See Also:

    • SMTLIB_VERSION

      public static final IExpr.IKeyword SMTLIB_VERSION
      The string designating the smtlib attribute within a logic or theory

    • SORTS

      public static final IExpr.IKeyword SORTS
      The attribute tag for defining sorts in a theory

    • FUNS

      public static final IExpr.IKeyword FUNS
      The attribute tag for defining functions in a theory

    • THEORIES

      public static final IExpr.IKeyword THEORIES
      The attribute tag for defining theories in a logic

    • CONTINUED_EXECUTION

      public static final String CONTINUED_EXECUTION
      An ERROR_BEHAVIOR return value
      See Also:

    • IMMEDIATE_EXIT

      public static final String IMMEDIATE_EXIT
      An ERROR_BEHAVIOR return value
      See Also:

    • MEMOUT

      public static final String MEMOUT
      A REASON_UNKNOWN return value
      See Also:

    • INCOMPLETE

      public static final String INCOMPLETE
      A REASON_UNKNOWN return value
      See Also:

    • LOGIC

      public static final String LOGIC
      The String for the logic symbol
      See Also:

    • THEORY

      public static final String THEORY
      The String for the theory symbol
      See Also:

    • IS

      public static final String IS
      The String for the head of a datatype tester, (_ is C)
      See Also:

    • PAR

      public static final String PAR
      The String for the par reserved word
      See Also:

    • AS

      public static final String AS
      The String for the as reserved word
      See Also:

    • LET

      public static final String LET
      The String for the let reserved word
      See Also:

    • FORALL

      public static final String FORALL
      The String for the forall reserved word
      See Also:

    • EXISTS

      public static final String EXISTS
      The String for the exists reserved word
      See Also:

    • WILDCARD

      public static final String WILDCARD
      The String for the _ wildcard in match patterns
      See Also:

    • STDOUT

      public static final String STDOUT
      The String for the stdout predefined string
      See Also:

    • STDERR

      public static final String STDERR
      The String for the stderr predefined string
      See Also:

    • TRUE

      public static final IExpr.ISymbol TRUE
      Symbol constant for boolean true.

    • FALSE

      public static final IExpr.ISymbol FALSE
      Symbol constant for boolean false.

    • NOT

      public static final IExpr.ISymbol NOT

    • AND

      public static final IExpr.ISymbol AND

    • OR

      public static final IExpr.ISymbol OR

    • IMPLIES

      public static final IExpr.ISymbol IMPLIES

    • EQ

      public static final IExpr.ISymbol EQ

    • DISTINCT

      public static final IExpr.ISymbol DISTINCT

    • ITE

      public static final IExpr.ISymbol ITE

    • XOR

      public static final IExpr.ISymbol XOR

    • PLUS

      public static final IExpr.ISymbol PLUS

    • MINUS

      public static final IExpr.ISymbol MINUS

    • MULT

      public static final IExpr.ISymbol MULT

    • SLASH

      public static final IExpr.ISymbol SLASH

    • DIV

      public static final IExpr.ISymbol DIV

    • MOD

      public static final IExpr.ISymbol MOD

    • ABS

      public static final IExpr.ISymbol ABS

    • EXP

      public static final IExpr.ISymbol EXP

    • GE

      public static final IExpr.ISymbol GE

    • GT

      public static final IExpr.ISymbol GT

    • LE

      public static final IExpr.ISymbol LE

    • LT

      public static final IExpr.ISymbol LT

    • STORE

      public static final IExpr.ISymbol STORE

    • SELECT

      public static final IExpr.ISymbol SELECT

    • ARRAY

      public static final IExpr.ISymbol ARRAY

    • ARROW

      public static final IExpr.ISymbol ARROW

    • AT

      public static final IExpr.ISymbol AT

    • BVNOT

      public static final IExpr.ISymbol BVNOT

    • BVNEG

      public static final IExpr.ISymbol BVNEG

    • BVAND

      public static final IExpr.ISymbol BVAND

    • BVOR

      public static final IExpr.ISymbol BVOR

    • BVADD

      public static final IExpr.ISymbol BVADD

    • BVMUL

      public static final IExpr.ISymbol BVMUL

    • BVUDIV

      public static final IExpr.ISymbol BVUDIV

    • BVUREM

      public static final IExpr.ISymbol BVUREM

    • BVSHL

      public static final IExpr.ISymbol BVSHL

    • BVLSHR

      public static final IExpr.ISymbol BVLSHR

    • BVNAND

      public static final IExpr.ISymbol BVNAND

    • BVNOR

      public static final IExpr.ISymbol BVNOR

    • BVXOR

      public static final IExpr.ISymbol BVXOR

    • BVXNOR

      public static final IExpr.ISymbol BVXNOR

    • BVSUB

      public static final IExpr.ISymbol BVSUB

    • BVSDIV

      public static final IExpr.ISymbol BVSDIV

    • BVSREM

      public static final IExpr.ISymbol BVSREM

    • BVSMOD

      public static final IExpr.ISymbol BVSMOD

    • BVASHR

      public static final IExpr.ISymbol BVASHR

    • BVCOMP

      public static final IExpr.ISymbol BVCOMP

    • BVULT

      public static final IExpr.ISymbol BVULT

    • BVULE

      public static final IExpr.ISymbol BVULE

    • BVUGT

      public static final IExpr.ISymbol BVUGT

    • BVUGE

      public static final IExpr.ISymbol BVUGE

    • BVSLT

      public static final IExpr.ISymbol BVSLT

    • BVSLE

      public static final IExpr.ISymbol BVSLE

    • BVSGT

      public static final IExpr.ISymbol BVSGT

    • BVSGE

      public static final IExpr.ISymbol BVSGE

    • CONCAT

      public static final IExpr.ISymbol CONCAT

    • EXTRACT

      public static final IExpr.ISymbol EXTRACT

    • CHAR

      public static final IExpr.ISymbol CHAR
      Head of the Strings theory's (_ char H) constants.

    • REPEAT

      public static final IExpr.ISymbol REPEAT

    • ZERO_EXTEND

      public static final IExpr.ISymbol ZERO_EXTEND

    • SIGN_EXTEND

      public static final IExpr.ISymbol SIGN_EXTEND

    • ROTATE_LEFT

      public static final IExpr.ISymbol ROTATE_LEFT

    • ROTATE_RIGHT

      public static final IExpr.ISymbol ROTATE_RIGHT

    • UBV_TO_INT

      public static final IExpr.ISymbol UBV_TO_INT
      Bitvector/Int conversions and overflow predicates (SMT-LIB 2.7 FixedSizeBitVectors).

    • SBV_TO_INT

      public static final IExpr.ISymbol SBV_TO_INT

    • INT_TO_BV

      public static final IExpr.ISymbol INT_TO_BV

    • BVNEGO

      public static final IExpr.ISymbol BVNEGO

    • BVUADDO

      public static final IExpr.ISymbol BVUADDO

    • BVSADDO

      public static final IExpr.ISymbol BVSADDO

    • BVUMULO

      public static final IExpr.ISymbol BVUMULO

    • BVSMULO

      public static final IExpr.ISymbol BVSMULO

    • BITVEC_SYM

      public static final IExpr.ISymbol BITVEC_SYM
      Canonical ISymbol form of BITVEC, for structural comparison against a parsed identifier's head symbol (see TypeChecker.isBitVec() and SymbolTable's bit-vector family check) instead of comparing via .toString().

    • FLOATINGPOINT

      public static final String FLOATINGPOINT
      See Also:

    • FLOATINGPOINT_SYM

      public static final IExpr.ISymbol FLOATINGPOINT_SYM
      Canonical ISymbol form of FLOATINGPOINT, for structural comparison against a parsed identifier's head symbol (see TypeChecker.isFloatingPoint() and SymbolTable's FloatingPoint family check) instead of comparing via .toString().

    • FLOAT16

      public static final IExpr.ISymbol FLOAT16
      Short names for common FloatingPoint sorts (FloatingPoint.smt2's :notes documents each as a synonym for a specific (_ FloatingPoint eb sb) instance) -- resolved by SymbolTable.lookupSort() to the exact same ISort.IDefinition as that instance, not registered as their own independent sorts (see Utils.loadTheory(), which excludes them from the generic :sorts loader for the same reason).

    • FLOAT32

      public static final IExpr.ISymbol FLOAT32

    • FLOAT64

      public static final IExpr.ISymbol FLOAT64

    • FLOAT128

      public static final IExpr.ISymbol FLOAT128

    • FP

      public static final IExpr.ISymbol FP

    • FP_ABS

      public static final IExpr.ISymbol FP_ABS

    • FP_NEG

      public static final IExpr.ISymbol FP_NEG

    • FP_ADD

      public static final IExpr.ISymbol FP_ADD

    • FP_SUB

      public static final IExpr.ISymbol FP_SUB

    • FP_MUL

      public static final IExpr.ISymbol FP_MUL

    • FP_DIV

      public static final IExpr.ISymbol FP_DIV

    • FP_FMA

      public static final IExpr.ISymbol FP_FMA

    • FP_SQRT

      public static final IExpr.ISymbol FP_SQRT

    • FP_REM

      public static final IExpr.ISymbol FP_REM

    • FP_ROUND_TO_INTEGRAL

      public static final IExpr.ISymbol FP_ROUND_TO_INTEGRAL

    • FP_MIN

      public static final IExpr.ISymbol FP_MIN

    • FP_MAX

      public static final IExpr.ISymbol FP_MAX

    • FP_LEQ

      public static final IExpr.ISymbol FP_LEQ

    • FP_LT

      public static final IExpr.ISymbol FP_LT

    • FP_GEQ

      public static final IExpr.ISymbol FP_GEQ

    • FP_GT

      public static final IExpr.ISymbol FP_GT

    • FP_EQ

      public static final IExpr.ISymbol FP_EQ

    • FP_IS_NORMAL

      public static final IExpr.ISymbol FP_IS_NORMAL

    • FP_IS_SUBNORMAL

      public static final IExpr.ISymbol FP_IS_SUBNORMAL

    • FP_IS_ZERO

      public static final IExpr.ISymbol FP_IS_ZERO

    • FP_IS_INFINITE

      public static final IExpr.ISymbol FP_IS_INFINITE

    • FP_IS_NAN

      public static final IExpr.ISymbol FP_IS_NAN

    • FP_IS_NEGATIVE

      public static final IExpr.ISymbol FP_IS_NEGATIVE

    • FP_IS_POSITIVE

      public static final IExpr.ISymbol FP_IS_POSITIVE

    • FP_TO_REAL

      public static final IExpr.ISymbol FP_TO_REAL

    • FP_TO_UBV

      public static final IExpr.ISymbol FP_TO_UBV

    • FP_TO_SBV

      public static final IExpr.ISymbol FP_TO_SBV

    • FP_POS_INF

      public static final IExpr.ISymbol FP_POS_INF
      Zero-arity indexed identifiers, e.g. (_ +oo eb sb) -- head symbols, not full identifiers.

    • FP_NEG_INF

      public static final IExpr.ISymbol FP_NEG_INF

    • FP_POS_ZERO

      public static final IExpr.ISymbol FP_POS_ZERO

    • FP_NEG_ZERO

      public static final IExpr.ISymbol FP_NEG_ZERO

    • FP_NAN

      public static final IExpr.ISymbol FP_NAN

    • TO_FP

      public static final IExpr.ISymbol TO_FP

    • TO_FP_UNSIGNED

      public static final IExpr.ISymbol TO_FP_UNSIGNED

    • ROUNDINGMODE_SYM

      public static final IExpr.ISymbol ROUNDINGMODE_SYM

    • boolOptions

      public final Set<String> boolOptions
      The set of standard options with boolean values

    • numericOptions

      public final Set<String> numericOptions
      The set of standard options with numeric values

    • stringOptions

      public final Set<String> stringOptions
      The set of standard options with string values

    • defaults

      public final Map<String,IAttributeValue> defaults
      The set of default values for all standard options

    • infoKeywords

      public static final HashSet<IExpr.IKeyword> infoKeywords

    • setInfoKeywords

      public static final HashSet<IExpr.IKeyword> setInfoKeywords
      The attributes the standard defines for set-info (any other is allowed, but not standard)

    • smtConfig

      protected SMT.Configuration smtConfig
      A reference to the configuration being used for this instance of Utils.

  • Constructor Details

    • Utils

      public Utils(SMT.Configuration smtConfig)
      Creates a Utils instance for the given configuration

  • Method Details

    • sourceLine

      public static int sourceLine(ICommand cmd)
      The line of its source on which the command starts (counted from 1), or 0 if it has no source position

    • produceAssertionsKey

      public static String produceAssertionsKey(SMT.Configuration smtConfig)
      Returns the name of the option that gates get-assertions -- renamed from :interactive-mode to :produce-assertions in SMT-LIB 2.5.

    • invalidSetInfoValue

      public static String invalidSetInfoValue(IExpr.IKeyword key, IAttributeValue value)
      The reason value is not a valid value for the standard set-info attribute key, or null if it is valid or key is not a standard set-info attribute

    • quote

      public String quote(String msg)
      Quotes a string, adding enclosing quotes and putting in SMT-LIBv2 escapes as needed
      Parameters:
      msg - String to quote
      Returns:
      the quoted string

    • unescape

      public String unescape(String msg)
      Converts a quoted string (which has enclosing double quotes) to a raw sequence of ASCII characters, undoing any SMT-LIBv2 escape sequences, and without the enclosing quotes

    • findLogic

      public ILogic findLogic(String name, IPos pos) throws Utils.SMTLIBException
      Reads a logic file, parses it, validates the name, and checks the version.
      Parameters:
      name - the logic name (and base filename)
      pos - source position for error messages, or null
      Returns:
      the parsed ILogic
      Throws:
      Utils.SMTLIBException - if the file cannot be found, parsed, or validated

    • findTheory

      public ITheory findTheory(String name, String path) throws Utils.SMTLIBException
      Reads a theory file, returning the S-expression that it holds.
      Parameters:
      name - the name of the theory
      path - the directory path in which theory files are stored
      Returns:
      the parsed ITheory
      Throws:
      Utils.SMTLIBException - if an error occurs

    • loadLogic

      public IResponse loadLogic(String logicName, SymbolTable symTable, IPos pos)
      Finds and loads a logic into the given symbol table
      Parameters:
      logicName - name of the logic to load
      symTable - the symbol table into which to load it
      Returns:
      null if read OK, an error if a problem happened

    • loadTheory

      public IResponse loadTheory(String theoryName, SymbolTable symTable)
      Loads a theory into the given symbol table.
      Parameters:
      theoryName - the theory to load
      symTable - the symbol table into which to put the theory
      Returns:
      null if OK, otherwise an error as a IResponse

    • loadLogic

      public IResponse loadLogic(ILogic logicExpr, SymbolTable symTable)

    • loadTheory

      public IResponse loadTheory(ITheory theory, SymbolTable symTable)

    • asSort

      public ISort asSort(ISexpr sexpr, SymbolTable symtab)

    • jacocoNeverExecuted

      public static void jacocoNeverExecuted()
      Called at branches that should never be executed in a correct program; prints a stack trace so that JaCoCo coverage failures are immediately visible at runtime.