Package io.github.cvc5

Class InputParser

java.lang.Object
io.github.cvc5.InputParser
All Implemented Interfaces:
AutoCloseable
public class InputParser extends Object implements AutoCloseable
This class is the main interface for retrieving commands and expressions from an input using a parser. After construction, it is expected that an input is first set via setFileInput(InputLanguage, String), setStringInput(InputLanguage, String, String), or setIncrementalStringInput(InputLanguage, String) and appendIncrementalStringInput(String). Then, the methods nextCommand() and nextTerm() can be invoked to parse the input. The input parser interacts with a symbol manager, which determines which symbols are defined in the current context, based on the background logic and user-defined symbols. If no symbol manager is provided, then the input parser will construct (an initially empty) one. If provided, the symbol manager must have a logic that is compatible with the provided solver. That is, if both the solver and symbol manager have their logics set (SymbolManager.isLogicSet() and Solver.isLogicSet(), then their logics must be the same. Upon setting an input source, if either the solver (resp. symbol manager) has its logic set, then the symbol manager (resp. solver) is set to use that logic, if its logic is not already set.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • InputParser

      public InputParser(Solver solver, SymbolManager sm)
      Construct an input parser
      Parameters:
      solver - The solver (e.g. for constructing terms and sorts)
      sm - The symbol manager, which contains a symbol table that maps symbols to terms and sorts. Must have a logic that is compatible with the solver.

    • InputParser

      public InputParser(Solver solver)
      Construct an input parser with an initially empty symbol manager.
      Parameters:
      solver - The solver (e.g. for constructing terms and sorts).

  • Method Details

    • close

      public void close()
      Free the native input parser, see deletePointer().
      Specified by:
      close in interface AutoCloseable

    • toString

      protected String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native pointer
      Returns:
      a string representation of the pointer

    • getSolver

      public Solver getSolver()
      Get the underlying solver of this input parser.
      Returns:
      The underlying solver of this input parser

    • getSymbolManager

      public SymbolManager getSymbolManager()
      Get the underlying symbol manager of this input parser.
      Returns:
      The underlying symbol manager of this input parser.

    • setFileInput

      public void setFileInput(InputLanguage lang, String fileName)
      Set the input for the given file.
      Parameters:
      lang - the input language (e.g. InputLanguage.SMT_LIB_2_6).
      fileName - the input file name.

    • setStringInput

      public void setStringInput(InputLanguage lang, String input, String name)
      Set the input to the given concrete input string.
      Parameters:
      lang - The input language.
      input - The input string.
      name - The name of the stream, for use in error messages.

    • setIncrementalStringInput

      public void setIncrementalStringInput(InputLanguage lang, String name)
      Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
      Parameters:
      lang - The input language.
      name - The name of the stream, for use in error messages.

    • appendIncrementalStringInput

      public void appendIncrementalStringInput(String input)
      Append string to the input being parsed by this parser. Should be called after calling setIncrementalStringInput.
      Parameters:
      input - The input string.

    • nextCommand

      public Command nextCommand()
      Parse and return the next command. Will initialize the logic to "ALL" or the forced logic if no logic is set prior to this point and a command is read that requires initializing the logic.
      Returns:
      The parsed command. This is the null command if no command was read.

    • nextTerm

      public Term nextTerm()
      Parse and return the next term. Requires setting the logic prior to this point.
      Returns:
      The parsed term.

    • done

      public boolean done()
      Determine if this parser done reading input.
      Returns:
      True if this parser done reading input.

    • getPointer

      public long getPointer()
      Return the raw native pointer.

      Every native call obtains the pointers of the objects it uses through this method, so that using an object after its native resource has been released raises an exception instead of crashing the JVM.

      Returns:
      the pointer value
      Throws:
      IllegalStateException - if the native resource of this object has been released, e.g., via deletePointer()

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      Native resources are freed automatically once the Java object is no longer reachable. This method frees the native resource immediately instead; afterwards, using the object raises an IllegalStateException. It must be called from the thread that is using the associated term manager. Calling it more than once has no further effect.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer