Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Definitions of SMT2 constants.
11 : : */
12 : :
13 : : #include "cvc5parser_private.h"
14 : :
15 : : #ifndef CVC5__PARSER__SMT2__SMT2_STATE_H
16 : : #define CVC5__PARSER__SMT2__SMT2_STATE_H
17 : :
18 : : #include <cvc5/cvc5.h>
19 : :
20 : : #include <optional>
21 : : #include <sstream>
22 : : #include <stack>
23 : : #include <string>
24 : : #include <unordered_map>
25 : : #include <utility>
26 : :
27 : : #include "parser/parse_op.h"
28 : : #include "parser/parser.h"
29 : : #include "theory/logic_info.h"
30 : :
31 : : namespace cvc5 {
32 : : namespace parser {
33 : :
34 : : /*
35 : : * The state information when parsing smt2 inputs.
36 : : */
37 : : class Smt2State : public ParserState
38 : : {
39 : : public:
40 : : Smt2State(ParserStateCallback* psc,
41 : : Solver* solver,
42 : : SymManager* sm,
43 : : ParsingMode parsingMode = ParsingMode::DEFAULT,
44 : : bool isSygus = false);
45 : :
46 : : ~Smt2State();
47 : :
48 : : /**
49 : : * Add core theory symbols to the parser state.
50 : : */
51 : : void addCoreSymbols();
52 : : /**
53 : : * Add skolem symbols to the parser state.
54 : : */
55 : : void addSkolemSymbols();
56 : :
57 : : void addOperator(Kind k, const std::string& name);
58 : :
59 : : /**
60 : : * Registers an indexed function symbol.
61 : : *
62 : : * @param tKind The kind of the term that uses the operator kind (e.g.
63 : : * BITVECTOR_EXTRACT). If an indexed function symbol is
64 : : * overloaded (e.g., `to_fp`), this argument should
65 : : * be`UNDEFINED_KIND`.
66 : : * @param name The name of the symbol (e.g. "extract")
67 : : */
68 : : void addIndexedOperator(Kind tKind, const std::string& name);
69 : : /**
70 : : * Registers a closure kind
71 : : *
72 : : * @param tKind The kind of the term that uses the operator kind (e.g.
73 : : * LAMBDA).
74 : : * @param name The name of the symbol (e.g. "lambda")
75 : : */
76 : : void addClosureKind(Kind tKind, const std::string& name);
77 : : /**
78 : : * Registers a skolem
79 : : *
80 : : * @param skolemID The is of the skolem
81 : : * @param name The name of the skolem, e.g. @array_deq_diff
82 : : */
83 : : void addSkolemId(SkolemId skolemID, const std::string& name);
84 : : /**
85 : : * Checks whether an indexed operator is enabled. All indexed operators in
86 : : * the current logic are considered to be enabled. This includes operators
87 : : * such as `to_fp`, which do not correspond to a single kind.
88 : : *
89 : : * @param name The name of the indexed operator.
90 : : * @return true if the indexed operator is enabled.
91 : : */
92 : : bool isIndexedOperatorEnabled(const std::string& name) const;
93 : :
94 : : Kind getOperatorKind(const std::string& name) const;
95 : :
96 : : bool isOperatorEnabled(const std::string& name) const;
97 : :
98 : : /** Parse block models mode */
99 : : modes::BlockModelsMode getBlockModelsMode(const std::string& mode);
100 : : /** Parse learned literal type */
101 : : modes::LearnedLitType getLearnedLitType(const std::string& mode);
102 : : /** Parse proof component */
103 : : modes::ProofComponent getProofComponent(const std::string& pc);
104 : : /** Parse find synth target */
105 : : modes::FindSynthTarget getFindSynthTarget(const std::string& fst);
106 : :
107 : : bool isTheoryEnabled(internal::theory::TheoryId theory) const;
108 : :
109 : : /**
110 : : * Checks if higher-order support is enabled.
111 : : *
112 : : * @return true if higher-order support is enabled, false otherwise
113 : : */
114 : : bool isHoEnabled() const;
115 : : /**
116 : : * @return true if cardinality constraints are enabled, false otherwise
117 : : */
118 : : bool hasCardinalityConstraints() const;
119 : :
120 : : bool logicIsSet() override;
121 : :
122 : : /**
123 : : * Creates an indexed constant, e.g. (_ +oo 8 24) (positive infinity
124 : : * as a 32-bit floating-point constant).
125 : : *
126 : : * @param name The name of the constant (e.g. "+oo")
127 : : * @param numerals The parameters for the constant (e.g. [8, 24])
128 : : * @return The term corresponding to the constant or a parse error if name is
129 : : * not valid.
130 : : */
131 : : Term mkIndexedConstant(const std::string& name,
132 : : const std::vector<uint32_t>& numerals);
133 : : /** Same as above, for constants indexed by symbols. */
134 : : Term mkIndexedConstant(const std::string& name,
135 : : const std::vector<std::string>& symbols);
136 : : /**
137 : : * Make the operator for kind k that is indexed by the given symbols.
138 : : * The arguments are passed for the purposes of resolving overloading.
139 : : * For example, this method is used to construct the proper tester. This
140 : : * requires knowing the type of the (first) argument in args.
141 : : */
142 : : Term mkIndexedOp(Kind k,
143 : : const std::vector<std::string>& symbols,
144 : : const std::vector<Term>& args);
145 : :
146 : : /**
147 : : * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".
148 : : *
149 : : * @param name The name of the operator (e.g. "extract")
150 : : * @return The kind corresponding to the indexed operator or a parse
151 : : * error if the name is not valid.
152 : : */
153 : : Kind getIndexedOpKind(const std::string& name);
154 : : /**
155 : : * Creates the closure kind, e.g. FORALL for "forall".
156 : : *
157 : : * @param name The name of the operator (e.g. "forall")
158 : : * @return The kind corresponding to the closure or a parse
159 : : * error if the name is not valid.
160 : : */
161 : : Kind getClosureKind(const std::string& name);
162 : :
163 : : /**
164 : : * If we are in a version < 2.6, this updates name to the tester name of cons,
165 : : * e.g. "is-cons".
166 : : */
167 : : bool getTesterName(Term cons, std::string& name) override;
168 : :
169 : : /**
170 : : * Make function defined by a define-fun(s)-rec command and bind it.
171 : : *
172 : : * fname : the name of the function.
173 : : * sortedVarNames : the list of variable arguments for the function.
174 : : * t : the range type of the function we are defining.
175 : : *
176 : : * This function will create a bind a new function term to name fname.
177 : : * The type of this function is
178 : : * ParserState::mkFlatFunctionType(sorts,t,flattenVars),
179 : : * where sorts are the types in the second components of sortedVarNames.
180 : : * As descibed in ParserState::mkFlatFunctionType, new bound variables may be
181 : : * added to flattenVars in this function if the function is given a function
182 : : * range type.
183 : : */
184 : : Term setupDefineFunRecScope(
185 : : const std::string& fname,
186 : : const std::vector<std::pair<std::string, Sort>>& sortedVarNames,
187 : : Sort t,
188 : : std::vector<Term>& flattenVars);
189 : :
190 : : /** Push scope for define-fun-rec
191 : : *
192 : : * This calls ParserState::pushScope() and sets up
193 : : * initial information for reading a body of a function definition
194 : : * in the define-fun-rec and define-funs-rec command.
195 : : * The input parameter flattenVars is the result
196 : : * of a call to mkDefineRec above.
197 : : *
198 : : * sortedVarNames : the list of variable arguments for the function.
199 : : * flattenVars : the implicit variables introduced when defining func.
200 : : *
201 : : * This function:
202 : : * (1) Calls ParserState::pushScope().
203 : : * (2) Computes the bound variable list for the quantified formula
204 : : * that defined this definition and stores it in bvs and binds it.
205 : : */
206 : : void pushDefineFunRecScope(
207 : : const std::vector<std::pair<std::string, Sort>>& sortedVarNames,
208 : : const std::vector<Term>& flattenVars,
209 : : std::vector<Term>& bvs);
210 : :
211 : : void reset() override;
212 : :
213 : : /**
214 : : * Creates a command that adds an invariant constraint.
215 : : *
216 : : * @param names Name of four symbols corresponding to the
217 : : * function-to-synthesize, precondition, postcondition,
218 : : * transition relation.
219 : : * @return The command that adds an invariant constraint
220 : : */
221 : : std::unique_ptr<Cmd> invConstraint(const std::vector<std::string>& names);
222 : :
223 : : /**
224 : : * Sets the logic for the current benchmark. Declares any logic and
225 : : * theory symbols.
226 : : *
227 : : * @param name the name of the logic (e.g., QF_UF, AUFLIA)
228 : : */
229 : : void setLogic(std::string name);
230 : :
231 : : /**
232 : : * Get the logic.
233 : : */
234 : 0 : const internal::LogicInfo& getLogic() const { return d_logic; }
235 : :
236 : : /**
237 : : * Create a Sygus grammar.
238 : : * @param boundVars the parameters to corresponding synth-fun/synth-inv
239 : : * @param ntSymbols the pre-declaration of the non-terminal symbols
240 : : * @return a pointer to the grammar
241 : : */
242 : : Grammar* mkGrammar(const std::vector<Term>& boundVars,
243 : : const std::vector<Term>& ntSymbols);
244 : :
245 : : /** Are we using a sygus language? */
246 : : bool sygus() const;
247 : :
248 : : /**
249 : : * Are we using SyGuS grammars? This is true if the input is the SyGuS
250 : : * language or if produce-abducts or produce-interpolants is true. Enables
251 : : * grammar-specific token `Constant`.
252 : : */
253 : : bool hasGrammars() const;
254 : : /**
255 : : * Are we using fresh binders? If this returns true, then every binder
256 : : * is assumed to refer to fresh variables. If this returns false, then
257 : : * variables are assumed to be globally unique up to their name and type.
258 : : */
259 : : bool usingFreshBinders() const;
260 : :
261 : : void checkThatLogicIsSet();
262 : :
263 : : /**
264 : : * Checks whether the current logic allows free sorts. If the logic does not
265 : : * support free sorts, the function triggers a parse error.
266 : : */
267 : : void checkLogicAllowsFreeSorts();
268 : :
269 : : /**
270 : : * Checks whether the current logic allows functions of non-zero arity. If
271 : : * the logic does not support such functions, the function triggers a parse
272 : : * error.
273 : : */
274 : : void checkLogicAllowsFunctions();
275 : :
276 : 365401 : void checkUserSymbol(const std::string& name)
277 : : {
278 [ + + ]: 730786 : if (!lenientModeEnabled() && name.length() > 0
279 [ + + ][ + - ]: 730786 : && (name[0] == '.' || name[0] == '@'))
[ - + ][ - + ]
280 : : {
281 : 0 : std::stringstream ss;
282 : : ss << "cannot declare or define symbol `" << name
283 : 0 : << "'; symbols starting with . and @ are reserved in SMT-LIB";
284 : 0 : parseError(ss.str());
285 : 0 : }
286 [ + + ]: 365401 : else if (isOperatorEnabled(name))
287 : : {
288 : 2 : std::stringstream ss;
289 : 2 : ss << "Symbol `" << name << "' is shadowing a theory function symbol";
290 : 4 : parseError(ss.str());
291 : 2 : }
292 : 365399 : }
293 : 11260 : void setLastNamedTerm(Term e, std::string name)
294 : : {
295 : 11260 : d_lastNamedTerm = std::make_pair(e, name);
296 : 11260 : }
297 : :
298 : 210014 : void clearLastNamedTerm() { d_lastNamedTerm = std::make_pair(Term(), ""); }
299 : :
300 : 221005 : std::pair<Term, std::string> lastNamedTerm() { return d_lastNamedTerm; }
301 : :
302 : : /** Does name denote an abstract value? (of the form '@n' for numeral n). */
303 : : bool isAbstractValue(const std::string& name);
304 : :
305 : : /**
306 : : * Make real or int from numeral string.
307 : : *
308 : : * In particular, if arithmetic is enabled, but integers are disabled, then
309 : : * we construct a real. Otherwise, we construct an integer.
310 : : */
311 : : Term mkRealOrIntFromNumeral(const std::string& str);
312 : :
313 : : /**
314 : : * Smt2 parser provides its own checkDeclaration, which does the
315 : : * same as the base, but with some more helpful errors.
316 : : */
317 : 2048773 : void checkDeclaration(const std::string& name,
318 : : DeclarationCheck check,
319 : : SymbolType type = SYM_VARIABLE,
320 : : std::string notes = "")
321 : : {
322 : : // if the symbol is something like "-1", we'll give the user a helpful
323 : : // syntax hint. (-1 is a valid identifier in SMT-LIB, NOT unary minus.)
324 [ + + ]: 4005804 : if (name.length() > 1 && name[0] == '-'
325 [ + + ][ + + ]: 4005804 : && name.find_first_not_of("0123456789", 1) == std::string::npos)
[ + + ]
326 : : {
327 : 4 : std::stringstream ss;
328 : : ss << notes << "You may have intended to apply unary minus: `(- "
329 : 4 : << name.substr(1) << ")'\n";
330 : 4 : this->ParserState::checkDeclaration(name, check, type, ss.str());
331 : 4 : return;
332 : 4 : }
333 : 2048769 : this->ParserState::checkDeclaration(name, check, type, notes);
334 : : }
335 : : /**
336 : : * Notify that expression expr was given name std::string via a :named
337 : : * attribute.
338 : : */
339 : : void notifyNamedExpression(Term& expr, std::string name);
340 : :
341 : : // Throw a ParserException with msg appended with the current logic.
342 : 0 : inline void parseErrorLogic(const std::string& msg)
343 : : {
344 : 0 : const std::string withLogic = msg + getLogic().getLogicString();
345 : 0 : parseError(withLogic);
346 : 0 : }
347 : :
348 : : //------------------------- processing parse operators
349 : : /**
350 : : * Given a parse operator p, apply a type ascription to it. This method is run
351 : : * when we encounter "(as t type)" and information regarding t has been stored
352 : : * in p.
353 : : *
354 : : * This updates p to take into account the ascription. This may include:
355 : : * - Converting an (pre-ascribed) array constant specification "const" to
356 : : * an ascribed array constant specification (as const type) where type is
357 : : * (Array T1 T2) for some T1, T2.
358 : : * - Converting a (nullary or non-nullary) parametric datatype constructor to
359 : : * the specialized constructor for the given type.
360 : : * - Converting an empty set, universe set, or separation nil reference to
361 : : * the respective term of the given type.
362 : : * - If p's expression field is set, then we leave p unchanged, check if
363 : : * that expression has the given type and throw a parse error otherwise.
364 : : */
365 : : void parseOpApplyTypeAscription(ParseOp& p, Sort type);
366 : : /**
367 : : * This converts a ParseOp to expression, assuming it is a standalone term.
368 : : *
369 : : * In particular:
370 : : * - If p's expression field is set, then that expression is returned.
371 : : * - If p's name field is set, then we look up that name in the symbol table
372 : : * of this class.
373 : : * In other cases, a parse error is thrown.
374 : : */
375 : : Term parseOpToExpr(ParseOp& p);
376 : : /**
377 : : * Apply parse operator to list of arguments, and return the resulting
378 : : * expression.
379 : : *
380 : : * This method involves two phases.
381 : : * (1) Processing the operator represented by p,
382 : : * (2) Applying that operator to the set of arguments.
383 : : *
384 : : * For (1), this involves determining the kind of the overall expression. We
385 : : * may be in one the following cases:
386 : : * - If p's expression field is set, we may choose to prepend it to args, or
387 : : * otherwise determine the appropriate kind of the overall expression based on
388 : : * this expression.
389 : : * - If p's name field is set, then we get the appropriate symbol for that
390 : : * name, which may involve disambiguating that name if it is overloaded based
391 : : * on the types of args. We then determine the overall kind of the return
392 : : * expression based on that symbol.
393 : : * - p's kind field may be already set.
394 : : *
395 : : * For (2), we construct the overall expression, which may involve the
396 : : * following:
397 : : * - If p is an array constant specification (as const (Array T1 T2)), then
398 : : * we return the appropriate array constant based on args[0].
399 : : * - If p represents a tuple selector, then we infer the appropriate tuple
400 : : * selector expression based on the type of args[0].
401 : : * - If the overall kind of the expression is chainable, we may convert it
402 : : * to a left- or right-associative chain.
403 : : * - If the overall kind is SUB and args has size 1, then we return an
404 : : * application of NEG.
405 : : * - If the overall expression is a partial application, then we process this
406 : : * as a chain of HO_APPLY terms.
407 : : */
408 : : Term applyParseOp(const ParseOp& p, std::vector<Term>& args);
409 : : /**
410 : : * Returns a (parameterized) sort, given a name and args.
411 : : */
412 : : Sort getParametricSort(const std::string& name,
413 : : const std::vector<Sort>& args) override;
414 : : /**
415 : : * Returns a (indexed) sort, given a name and numeric indices.
416 : : */
417 : : Sort getIndexedSort(const std::string& name,
418 : : const std::vector<std::string>& numerals);
419 : : /** is closure? */
420 : : bool isClosure(const std::string& name);
421 : : //------------------------- end processing parse operators
422 : :
423 : : /**
424 : : * Handles a push command.
425 : : *
426 : : * @return An instance of `PushCommand`
427 : : */
428 : : std::unique_ptr<Cmd> handlePush(std::optional<uint32_t> nscopes);
429 : : /**
430 : : * Handles a pop command.
431 : : *
432 : : * @return An instance of `PopCommand`
433 : : */
434 : : std::unique_ptr<Cmd> handlePop(std::optional<uint32_t> nscopes);
435 : :
436 : : private:
437 : : void addArithmeticOperators();
438 : :
439 : : void addTranscendentalOperators();
440 : :
441 : : void addQuantifiersOperators();
442 : :
443 : : void addBitvectorOperators();
444 : :
445 : : void addFiniteFieldOperators();
446 : :
447 : : void addDatatypesOperators();
448 : :
449 : : void addStringOperators();
450 : :
451 : : void addFloatingPointOperators();
452 : :
453 : : void addSepOperators();
454 : :
455 : : /**
456 : : * Utility function to create a conjunction of expressions.
457 : : *
458 : : * @param es Expressions in the conjunction
459 : : * @return True if `es` is empty, `e` if `es` consists of a single element
460 : : * `e`, the conjunction of expressions otherwise.
461 : : */
462 : : Term mkAnd(const std::vector<Term>& es) const;
463 : : /**
464 : : * @return True if term t an integer value.
465 : : */
466 : : static bool isConstInt(const Term& t);
467 : : /**
468 : : * @return True if term t is a bit-vector value.
469 : : */
470 : : static bool isConstBv(const Term& t);
471 : :
472 : : /** Are we parsing a sygus file? */
473 : : bool d_isSygus;
474 : : /** are we using fresh binders? */
475 : : bool d_freshBinders;
476 : : /** Has the logic been set (either by forcing it or a set-logic command)? */
477 : : bool d_logicSet;
478 : : /** The current logic */
479 : : internal::LogicInfo d_logic;
480 : : /** Maps strings to the operator it is bound to */
481 : : std::unordered_map<std::string, Kind> d_operatorKindMap;
482 : : /** Maps strings to the skolem it is bound to */
483 : : std::unordered_map<std::string, SkolemId> d_skolemMap;
484 : : /**
485 : : * Maps indexed symbols to the kind of the operator (e.g. "extract" to
486 : : * BITVECTOR_EXTRACT).
487 : : */
488 : : std::unordered_map<std::string, Kind> d_indexedOpKindMap;
489 : : /** Closure map */
490 : : std::unordered_map<std::string, Kind> d_closureKindMap;
491 : : /** The last named term and its name */
492 : : std::pair<Term, std::string> d_lastNamedTerm;
493 : : /**
494 : : * A list of sygus grammar objects. We keep track of them here to ensure that
495 : : * they don't get deleted before the commands using them get invoked.
496 : : */
497 : : std::vector<std::unique_ptr<Grammar>> d_allocGrammars;
498 : : };
499 : :
500 : : } // namespace parser
501 : : } // namespace cvc5
502 : :
503 : : #endif
|
