src/parser/smt2/smt2.h

   1 /*********************                                                        */
   2 /*! \file smt2.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Morgan Deters
   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 Definitions of SMT2 constants.
  13  **
  14  ** Definitions of SMT2 constants.
  15  **/
  16
  17 #include "cvc4parser_private.h"
  18
  19 #ifndef CVC4__PARSER__SMT2_H
  20 #define CVC4__PARSER__SMT2_H
  21
  22 #include <sstream>
  23 #include <stack>
  24 #include <string>
  25 #include <unordered_map>
  26 #include <utility>
  27
  28 #include "api/cvc4cpp.h"
  29 #include "parser/parse_op.h"
  30 #include "parser/parser.h"
  31 #include "theory/logic_info.h"
  32 #include "util/abstract_value.h"
  33
  34 namespace CVC4 {
  35
  36 class Command;
  37 class SExpr;
  38
  39 namespace api {
  40 class Solver;
  41 }
  42
  43 namespace parser {
  44
  45 class Smt2 : public Parser
  46 {
  47   friend class ParserBuilder;
  48
  49  private:
  50   /** Has the logic been set (either by forcing it or a set-logic command)? */
  51   bool d_logicSet;
  52   /** Have we seen a set-logic command yet? */
  53   bool d_seenSetLogic;
  54
  55   LogicInfo d_logic;
  56   std::unordered_map<std::string, api::Kind> operatorKindMap;
  57   /**
  58    * Maps indexed symbols to the kind of the operator (e.g. "extract" to
  59    * BITVECTOR_EXTRACT).
  60    */
  61   std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
  62   std::pair<api::Term, std::string> d_lastNamedTerm;
  63   /**
  64    * A list of sygus grammar objects. We keep track of them here to ensure that
  65    * they don't get deleted before the commands using them get invoked.
  66    */
  67   std::vector<std::unique_ptr<api::Grammar>> d_allocGrammars;
  68
  69  protected:
  70   Smt2(api::Solver* solver,
  71        SymbolManager* sm,
  72        Input* input,
  73        bool strictMode = false,
  74        bool parseOnly = false);
  75
  76  public:
  77   ~Smt2();
  78
  79   /**
  80    * Add core theory symbols to the parser state.
  81    */
  82   void addCoreSymbols();
  83
  84   void addOperator(api::Kind k, const std::string& name);
  85
  86   /**
  87    * Registers an indexed function symbol.
  88    *
  89    * @param tKind The kind of the term that uses the operator kind (e.g.
  90    *              BITVECTOR_EXTRACT). NOTE: this is an internal kind for now
  91    *              because that is what we use to create expressions. Eventually
  92    *              it will be an api::Kind.
  93    * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT)
  94    * @param name The name of the symbol (e.g. "extract")
  95    */
  96   void addIndexedOperator(api::Kind tKind,
  97                           api::Kind opKind,
  98                           const std::string& name);
  99
 100   api::Kind getOperatorKind(const std::string& name) const;
 101
 102   bool isOperatorEnabled(const std::string& name) const;
 103
 104   bool isTheoryEnabled(theory::TheoryId theory) const;
 105
 106   /**
 107    * Checks if higher-order support is enabled.
 108    *
 109    * @return true if higher-order support is enabled, false otherwise
 110    */
 111   bool isHoEnabled() const;
 112
 113   bool logicIsSet() override;
 114
 115   /**
 116    * Creates an indexed constant, e.g. (_ +oo 8 24) (positive infinity
 117    * as a 32-bit floating-point constant).
 118    *
 119    * @param name The name of the constant (e.g. "+oo")
 120    * @param numerals The parameters for the constant (e.g. [8, 24])
 121    * @return The term corresponding to the constant or a parse error if name is
 122    *         not valid.
 123    */
 124   api::Term mkIndexedConstant(const std::string& name,
 125                               const std::vector<uint64_t>& numerals);
 126
 127   /**
 128    * Creates an indexed operator term, e.g. (_ extract 5 0).
 129    *
 130    * @param name The name of the operator (e.g. "extract")
 131    * @param numerals The parameters for the operator (e.g. [5, 0])
 132    * @return The operator term corresponding to the indexed operator or a parse
 133    *         error if the name is not valid.
 134    */
 135   api::Op mkIndexedOp(const std::string& name,
 136                       const std::vector<uint64_t>& numerals);
 137
 138   /**
 139    * Returns the expression that name should be interpreted as.
 140    */
 141   api::Term getExpressionForNameAndType(const std::string& name,
 142                                         api::Sort t) override;
 143
 144   /**
 145    * If we are in a version < 2.6, this updates name to the tester name of cons,
 146    * e.g. "is-cons".
 147    */
 148   bool getTesterName(api::Term cons, std::string& name) override;
 149
 150   /** Make function defined by a define-fun(s)-rec command.
 151    *
 152    * fname : the name of the function.
 153    * sortedVarNames : the list of variable arguments for the function.
 154    * t : the range type of the function we are defining.
 155    *
 156    * This function will create a bind a new function term to name fname.
 157    * The type of this function is
 158    * Parser::mkFlatFunctionType(sorts,t,flattenVars),
 159    * where sorts are the types in the second components of sortedVarNames.
 160    * As descibed in Parser::mkFlatFunctionType, new bound variables may be
 161    * added to flattenVars in this function if the function is given a function
 162    * range type.
 163    */
 164   api::Term bindDefineFunRec(
 165       const std::string& fname,
 166       const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
 167       api::Sort t,
 168       std::vector<api::Term>& flattenVars);
 169
 170   /** Push scope for define-fun-rec
 171    *
 172    * This calls Parser::pushScope() and sets up
 173    * initial information for reading a body of a function definition
 174    * in the define-fun-rec and define-funs-rec command.
 175    * The input parameters func/flattenVars are the result
 176    * of a call to mkDefineRec above.
 177    *
 178    * func : the function whose body we are defining.
 179    * sortedVarNames : the list of variable arguments for the function.
 180    * flattenVars : the implicit variables introduced when defining func.
 181    *
 182    * This function:
 183    * (1) Calls Parser::pushScope().
 184    * (2) Computes the bound variable list for the quantified formula
 185    *     that defined this definition and stores it in bvs.
 186    */
 187   void pushDefineFunRecScope(
 188       const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
 189       api::Term func,
 190       const std::vector<api::Term>& flattenVars,
 191       std::vector<api::Term>& bvs);
 192
 193   void reset() override;
 194
 195   /**
 196    * Creates a command that adds an invariant constraint.
 197    *
 198    * @param names Name of four symbols corresponding to the
 199    *              function-to-synthesize, precondition, postcondition,
 200    *              transition relation.
 201    * @return The command that adds an invariant constraint
 202    */
 203   std::unique_ptr<Command> invConstraint(const std::vector<std::string>& names);
 204
 205   /**
 206    * Sets the logic for the current benchmark. Declares any logic and
 207    * theory symbols.
 208    *
 209    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
 210    * @param fromCommand should be set to true if the request originates from a
 211    *                    set-logic command and false otherwise
 212    * @return the command corresponding to setting the logic
 213    */
 214   Command* setLogic(std::string name, bool fromCommand = true);
 215
 216   /**
 217    * Get the logic.
 218    */
 219   const LogicInfo& getLogic() const { return d_logic; }
 220
 221   /**
 222    * Create a Sygus grammar.
 223    * @param boundVars the parameters to corresponding synth-fun/synth-inv
 224    * @param ntSymbols the pre-declaration of the non-terminal symbols
 225    * @return a pointer to the grammar
 226    */
 227   api::Grammar* mkGrammar(const std::vector<api::Term>& boundVars,
 228                           const std::vector<api::Term>& ntSymbols);
 229
 230   bool v2_0() const
 231   {
 232     return getLanguage() == language::input::LANG_SMTLIB_V2_0;
 233   }
 234   /**
 235    * Are we using smtlib 2.5 or above? If exact=true, then this method returns
 236    * false if the input language is not exactly SMT-LIB 2.5.
 237    */
 238   bool v2_5(bool exact = false) const
 239   {
 240     return language::isInputLang_smt2_5(getLanguage(), exact);
 241   }
 242   /**
 243    * Are we using smtlib 2.6 or above? If exact=true, then this method returns
 244    * false if the input language is not exactly SMT-LIB 2.6.
 245    */
 246   bool v2_6(bool exact = false) const
 247   {
 248     return language::isInputLang_smt2_6(getLanguage(), exact);
 249   }
 250   /** Are we using a sygus language? */
 251   bool sygus() const;
 252   /** Are we using the sygus version 2.0 format? */
 253   bool sygus_v2() const;
 254
 255   /**
 256    * Returns true if the language that we are parsing (SMT-LIB version >=2.5
 257    * and SyGuS) treats duplicate double quotes ("") as an escape sequence
 258    * denoting a single double quote (").
 259    */
 260   bool escapeDupDblQuote() const { return v2_5() || sygus(); }
 261
 262   void checkThatLogicIsSet();
 263
 264   /**
 265    * Checks whether the current logic allows free sorts. If the logic does not
 266    * support free sorts, the function triggers a parse error.
 267    */
 268   void checkLogicAllowsFreeSorts();
 269
 270   /**
 271    * Checks whether the current logic allows functions of non-zero arity. If
 272    * the logic does not support such functions, the function triggers a parse
 273    * error.
 274    */
 275   void checkLogicAllowsFunctions();
 276
 277   void checkUserSymbol(const std::string& name)
 278   {
 279     if (name.length() > 0 && (name[0] == '.' || name[0] == '@'))
 280     {
 281       std::stringstream ss;
 282       ss << "cannot declare or define symbol `" << name
 283          << "'; symbols starting with . and @ are reserved in SMT-LIB";
 284       parseError(ss.str());
 285     }
 286     else if (isOperatorEnabled(name))
 287     {
 288       std::stringstream ss;
 289       ss << "Symbol `" << name << "' is shadowing a theory function symbol";
 290       parseError(ss.str());
 291     }
 292   }
 293
 294   void includeFile(const std::string& filename);
 295
 296   void setLastNamedTerm(api::Term e, std::string name)
 297   {
 298     d_lastNamedTerm = std::make_pair(e, name);
 299   }
 300
 301   void clearLastNamedTerm()
 302   {
 303     d_lastNamedTerm = std::make_pair(api::Term(), "");
 304   }
 305
 306   std::pair<api::Term, std::string> lastNamedTerm() { return d_lastNamedTerm; }
 307
 308   /** Does name denote an abstract value? (of the form '@n' for numeral n). */
 309   bool isAbstractValue(const std::string& name);
 310
 311   /** Make abstract value
 312    *
 313    * Abstract values are used for processing get-value calls. The argument
 314    * name should be such that isAbstractValue(name) is true.
 315    */
 316   api::Term mkAbstractValue(const std::string& name);
 317
 318   /**
 319    * Smt2 parser provides its own checkDeclaration, which does the
 320    * same as the base, but with some more helpful errors.
 321    */
 322   void checkDeclaration(const std::string& name,
 323                         DeclarationCheck check,
 324                         SymbolType type = SYM_VARIABLE,
 325                         std::string notes = "")
 326   {
 327     // if the symbol is something like "-1", we'll give the user a helpful
 328     // syntax hint.  (-1 is a valid identifier in SMT-LIB, NOT unary minus.)
 329     if (name.length() > 1 && name[0] == '-'
 330         && name.find_first_not_of("0123456789", 1) == std::string::npos)
 331     {
 332       std::stringstream ss;
 333       ss << notes << "You may have intended to apply unary minus: `(- "
 334          << name.substr(1) << ")'\n";
 335       this->Parser::checkDeclaration(name, check, type, ss.str());
 336       return;
 337     }
 338     this->Parser::checkDeclaration(name, check, type, notes);
 339   }
 340   /**
 341    * Notify that expression expr was given name std::string via a :named
 342    * attribute.
 343    */
 344   void notifyNamedExpression(api::Term& expr, std::string name);
 345
 346   // Throw a ParserException with msg appended with the current logic.
 347   inline void parseErrorLogic(const std::string& msg)
 348   {
 349     const std::string withLogic = msg + getLogic().getLogicString();
 350     parseError(withLogic);
 351   }
 352
 353   //------------------------- processing parse operators
 354   /**
 355    * Given a parse operator p, apply a type ascription to it. This method is run
 356    * when we encounter "(as t type)" and information regarding t has been stored
 357    * in p.
 358    *
 359    * This updates p to take into account the ascription. This may include:
 360    * - Converting an (pre-ascribed) array constant specification "const" to
 361    * an ascribed array constant specification (as const type) where type is
 362    * (Array T1 T2) for some T1, T2.
 363    * - Converting a (nullary or non-nullary) parametric datatype constructor to
 364    * the specialized constructor for the given type.
 365    * - Converting an empty set, universe set, or separation nil reference to
 366    * the respective term of the given type.
 367    * - If p's expression field is set, then we leave p unchanged, check if
 368    * that expression has the given type and throw a parse error otherwise.
 369    */
 370   void parseOpApplyTypeAscription(ParseOp& p, api::Sort type);
 371   /**
 372    * This converts a ParseOp to expression, assuming it is a standalone term.
 373    *
 374    * In particular:
 375    * - If p's expression field is set, then that expression is returned.
 376    * - If p's name field is set, then we look up that name in the symbol table
 377    * of this class.
 378    * In other cases, a parse error is thrown.
 379    */
 380   api::Term parseOpToExpr(ParseOp& p);
 381   /**
 382    * Apply parse operator to list of arguments, and return the resulting
 383    * expression.
 384    *
 385    * This method involves two phases.
 386    * (1) Processing the operator represented by p,
 387    * (2) Applying that operator to the set of arguments.
 388    *
 389    * For (1), this involves determining the kind of the overall expression. We
 390    * may be in one the following cases:
 391    * - If p's expression field is set, we may choose to prepend it to args, or
 392    * otherwise determine the appropriate kind of the overall expression based on
 393    * this expression.
 394    * - If p's name field is set, then we get the appropriate symbol for that
 395    * name, which may involve disambiguating that name if it is overloaded based
 396    * on the types of args. We then determine the overall kind of the return
 397    * expression based on that symbol.
 398    * - p's kind field may be already set.
 399    *
 400    * For (2), we construct the overall expression, which may involve the
 401    * following:
 402    * - If p is an array constant specification (as const (Array T1 T2)), then
 403    * we return the appropriate array constant based on args[0].
 404    * - If p represents a tuple selector, then we infer the appropriate tuple
 405    * selector expression based on the type of args[0].
 406    * - If the overall kind of the expression is chainable, we may convert it
 407    * to a left- or right-associative chain.
 408    * - If the overall kind is MINUS and args has size 1, then we return an
 409    * application of UMINUS.
 410    * - If the overall expression is a partial application, then we process this
 411    * as a chain of HO_APPLY terms.
 412    */
 413   api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
 414   //------------------------- end processing parse operators
 415  private:
 416
 417   void addArithmeticOperators();
 418
 419   void addTranscendentalOperators();
 420
 421   void addQuantifiersOperators();
 422
 423   void addBitvectorOperators();
 424
 425   void addDatatypesOperators();
 426
 427   void addStringOperators();
 428
 429   void addFloatingPointOperators();
 430
 431   void addSepOperators();
 432
 433   InputLanguage getLanguage() const;
 434
 435   /**
 436    * Utility function to create a conjunction of expressions.
 437    *
 438    * @param es Expressions in the conjunction
 439    * @return True if `es` is empty, `e` if `es` consists of a single element
 440    *         `e`, the conjunction of expressions otherwise.
 441    */
 442   api::Term mkAnd(const std::vector<api::Term>& es);
 443 }; /* class Smt2 */
 444
 445 }  // namespace parser
 446 }  // namespace CVC4
 447
 448 #endif /* CVC4__PARSER__SMT2_H */