GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/smt2/smt2.h Lines: 22 33 66.7 %
Date: 2021-03-22 Branches: 27 74 36.5 %

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