src/parser/smt2/smt2.h

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