src/parser/parser_builder.h

   1 /*********************                                                        */
   2 /*! \file parser_builder.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Christopher L. Conway, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A builder for parsers.
  13  **
  14  ** A builder for parsers.
  15  **/
  16
  17 #include "cvc4parser_public.h"
  18
  19 #ifndef CVC4__PARSER__PARSER_BUILDER_H
  20 #define CVC4__PARSER__PARSER_BUILDER_H
  21
  22 #include <string>
  23
  24 #include "options/language.h"
  25 #include "parser/input.h"
  26
  27 namespace CVC4 {
  28
  29 class Options;
  30
  31 namespace api {
  32 class Solver;
  33 }
  34
  35 namespace parser {
  36
  37 class Parser;
  38
  39 /**
  40  * A builder for input language parsers. <code>build()</code> can be
  41  * called any number of times on an instance and will generate a fresh
  42  * parser each time.
  43  */
  44 class CVC4_PUBLIC ParserBuilder {
  45   enum InputType {
  46     FILE_INPUT,
  47     LINE_BUFFERED_STREAM_INPUT,
  48     STREAM_INPUT,
  49     STRING_INPUT
  50   };
  51
  52   /** The input type. */
  53   InputType d_inputType;
  54
  55   /** The input language */
  56   InputLanguage d_lang;
  57
  58   /** The file name (may not exist) */
  59   std::string d_filename;
  60
  61   /** The string input, if any. */
  62   std::string d_stringInput;
  63
  64   /** The stream input, if any. */
  65   std::istream* d_streamInput;
  66
  67   /** The API Solver object. */
  68   api::Solver* d_solver;
  69
  70   /** Should semantic checks be enabled during parsing? */
  71   bool d_checksEnabled;
  72
  73   /** Should we parse in strict mode? */
  74   bool d_strictMode;
  75
  76   /** Should we allow include-file commands? */
  77   bool d_canIncludeFile;
  78
  79   /** Should we memory-map a file input? */
  80   bool d_mmap;
  81
  82   /** Are we parsing only? */
  83   bool d_parseOnly;
  84
  85   /** Is the logic forced by the user? */
  86   bool d_logicIsForced;
  87
  88   /** The forced logic name */
  89   std::string d_forcedLogic;
  90
  91   /** Initialize this parser builder */
  92   void init(api::Solver* solver, const std::string& filename);
  93
  94  public:
  95   /** Create a parser builder using the given Solver and filename. */
  96   ParserBuilder(api::Solver* solver, const std::string& filename);
  97
  98   ParserBuilder(api::Solver* solver,
  99                 const std::string& filename,
 100                 const Options& options);
 101
 102   /** Build the parser, using the current settings. */
 103   Parser* build();
 104
 105   /** Should semantic checks be enabled in the parser? (Default: yes) */
 106   ParserBuilder& withChecks(bool flag = true);
 107
 108   /** Set the Solver to use with the parser. */
 109   ParserBuilder& withSolver(api::Solver* solver);
 110
 111   /** Set the parser to read a file for its input. (Default) */
 112   ParserBuilder& withFileInput();
 113
 114   /**
 115    * Set the filename for use by the parser. If file input is used,
 116    * this file will be opened and read by the parser. Otherwise, the
 117    * filename string (possibly a non-existent path) will only be used
 118    * in error messages.
 119    */
 120   ParserBuilder& withFilename(const std::string& filename);
 121
 122   /**
 123    * Set the input language to be used by the parser.
 124    *
 125    * (Default: LANG_AUTO)
 126    */
 127   ParserBuilder& withInputLanguage(InputLanguage lang);
 128
 129   /**
 130    * Should the parser memory-map its input? This is only relevant if
 131    * the parser will have a file input.
 132    *
 133    * (Default: no)
 134    */
 135   ParserBuilder& withMmap(bool flag = true);
 136
 137   /**
 138    * Are we only parsing, or doing something with the resulting
 139    * commands and expressions?  This setting affects whether the
 140    * parser will raise certain errors about unimplemented features,
 141    * even if there isn't a parsing error, because the result of the
 142    * parse would otherwise be an incorrect parse tree and the error
 143    * would go undetected.  This is specifically for circumstances
 144    * where the parser is ahead of the functionality present elsewhere
 145    * in CVC4 (such as quantifiers, subtypes, records, etc. in the CVC
 146    * language parser).
 147    */
 148   ParserBuilder& withParseOnly(bool flag = true);
 149
 150   /** Derive settings from the given options. */
 151   ParserBuilder& withOptions(const Options& options);
 152
 153   /**
 154    * Should the parser use strict mode?
 155    *
 156    * (Default: no)
 157    */
 158   ParserBuilder& withStrictMode(bool flag = true);
 159
 160   /**
 161    * Should the include-file commands be enabled?
 162    *
 163    * (Default: yes)
 164    */
 165   ParserBuilder& withIncludeFile(bool flag = true);
 166
 167   /** Set the parser to use the given stream for its input. */
 168   ParserBuilder& withStreamInput(std::istream& input);
 169
 170   /** Set the parser to use the given stream for its input. */
 171   ParserBuilder& withLineBufferedStreamInput(std::istream& input);
 172
 173   /** Set the parser to use the given string for its input. */
 174   ParserBuilder& withStringInput(const std::string& input);
 175
 176   /** Set the parser to use the given logic string. */
 177   ParserBuilder& withForcedLogic(const std::string& logic);
 178 };/* class ParserBuilder */
 179
 180 }/* CVC4::parser namespace */
 181 }/* CVC4 namespace */
 182
 183 #endif /* CVC4__PARSER__PARSER_BUILDER_H */