-
Notifications
You must be signed in to change notification settings - Fork 48
/
SMTLIB2.hpp
494 lines (414 loc) · 15 KB
/
SMTLIB2.hpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file SMTLIB.hpp
* Defines class SMTLIB.
*/
#ifndef __SMTLIB2__
#define __SMTLIB2__
#include "Forwards.hpp"
#include "Lib/Set.hpp"
#include "Kernel/Signature.hpp"
#include "Kernel/OperatorType.hpp"
#include "Kernel/Term.hpp"
#include "Shell/LispParser.hpp"
namespace Parse {
using namespace Lib;
using namespace Kernel;
using namespace Shell;
class SMTLIB2 {
public:
SMTLIB2(const Options& opts);
/** Parse from an open stream */
void parse(istream& str);
/** Parse a ready lisp expression */
void parse(LExpr* bench);
/** Formulas obtained during parsing:
* 1) equations collected from "define-fun"
* 2) general formulas collected from "assert"
*
* Global signature in env is updated on the fly.
*
* We don't know what the conjecture is.
**/
UnitList* getFormulas() const { return _formulas; }
/**
* Return the parsed logic (or LO_INVALID if not set).
*/
SMTLIBLogic getLogic() const {
return _logic;
}
const vstring& getStatus() const {
return _statusStr;
}
private:
static const char * s_smtlibLogicNameStrings[];
/**
* Maps a string to a SmtlibLogic value.
*/
static SMTLIBLogic getLogicFromString(const vstring& str);
/**
* Have we seen "set-logic" entry yet?
*/
bool _logicSet;
/**
* The advertised logic.
*/
SMTLIBLogic _logic;
/**
* Logics which contains only reals allow numerals (like '123') to be understood as reals.
* When both Ints and Reals are mixed numerals are Ints and decimals (like '123.0') are reals.
*
* This is determined based on the advertised logic (and not the actual content of the file).
*/
bool _numeralsAreReal;
/**
* Handle "set-logic" entry.
*/
void readLogic(const vstring& logicStr);
/** Content of the ":status: info entry. */
vstring _statusStr;
/** Content of the ":source: info entry. */
vstring _sourceInfo;
enum BuiltInSorts
{
BS_ARRAY,
BS_BOOL,
BS_INT,
BS_REAL,
BS_INVALID
};
static const char * s_builtInSortNameStrings[];
/**
* Maps smtlib built-in sort name to BuiltInSorts value.
*/
static BuiltInSorts getBuiltInSortFromString(const vstring& str);
/**
* Test string for being either a built-in sort
* or a sort already declared or defined within this parser object.
*/
bool isAlreadyKnownSortSymbol(const vstring& name);
/** Maps smtlib name of a declared sort to its arity.
*
* Declared sorts are just names with arity-many "argument slots".
* However, this is just a way to make new sorts from old ones.
* There is no implied semantic relation to the argument sorts.
*/
DHMap<vstring,unsigned> _declaredSorts;
/**
* Handle "declare-sort" entry.
*/
void readDeclareSort(const vstring& name, const vstring& arity);
/**
* Sort definition is a macro (with arguments) for a complex sort expression.
*
* We don't parse the definition until it is used.
*
* Then a lookup context is created mapping
* symbolic arguments from the definition to actual arguments from the invocation
* and the invocation is parsed as the defined body in this context.
*/
struct SortDefinition {
SortDefinition() : args(0), body(0) {}
SortDefinition(LExprList* args, LExpr* body)
: args(args), body(body) {}
LExprList* args;
LExpr* body;
};
/**
* Maps smtlib name of a defined sort to its SortDefinition struct.
*/
DHMap<vstring,SortDefinition> _sortDefinitions;
/**
* Handle "define-sort" entry.
*/
void readDefineSort(const vstring& name, LExprList* args, LExpr* body);
/**
* Take an smtlib sort expression, evaluate it in the context of previous
* sort declarations and definitions,
* register any missing sort in vampire and return vampire's sort id
* corresponding to the give expression.
*/
TermList declareSort(LExpr* sExpr);
/**
* Some built-in symbols represent functions with result of sort Bool.
* They are listed here.
*/
enum FormulaSymbol
{
FS_LESS,
FS_LESS_EQ,
FS_EQ,
FS_IMPLIES,
FS_GREATER,
FS_GREATER_EQ,
FS_AND,
FS_DISTINCT,
FS_EXISTS,
FS_FALSE,
FS_FORALL,
FS_IS_INT,
FS_NOT,
FS_OR,
FS_TRUE,
FS_XOR,
FS_USER_PRED_SYMBOL
};
static const char * s_formulaSymbolNameStrings[];
/**
* Lookup to see if vstring is a built-in FormulaSymbol.
*/
static FormulaSymbol getBuiltInFormulaSymbol(const vstring& str);
/**
* Some built-in symbols represent functions with not-Bool result of sort
* and are listed here.
*/
enum TermSymbol
{
TS_MULTIPLY,
TS_PLUS,
TS_MINUS,
TS_DIVIDE,
TS_ABS,
TS_DIV,
TS_ITE,
TS_LET,
TS_MATCH,
TS_MOD,
TS_SELECT,
TS_STORE,
TS_TO_INT,
TS_TO_REAL,
TS_USER_FUNCTION
};
static const char * s_termSymbolNameStrings[];
/**
* Lookup to see if vstring is a built-in TermSymbol.
*/
static TermSymbol getBuiltInTermSymbol(const vstring& str);
/**
* Is the given vstring a built-in FormulaSymbol, built-in TermSymbol or a declared function?
*/
bool isAlreadyKnownFunctionSymbol(const vstring& name);
/** <vampire signature id, is_function flag (otherwise it is a predicate) > */
typedef std::pair<unsigned,bool> DeclaredFunction;
/** functions are implicitly declared also when they are defined (see below) */
DHMap<vstring, DeclaredFunction> _declaredFunctions;
/**
* Given a symbol name, range sort (which can be Bool) and argSorts,
* register a new function (or predicate) symbol in vampire,
* store the ensuing DeclaredFunction in _declaredFunctions
* and return it.
*/
DeclaredFunction declareFunctionOrPredicate(const vstring& name, TermList rangeSort, const TermStack& argSorts);
/**
* Handle "declare-fun" entry.
*
* Declaring a function just extends the signature.
*/
void readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort);
/**
* Handle "define-fun" entry.
*
* Defining a function extends the signature and adds the new function's definition into _formulas.
*/
void readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort, LExpr* body, bool recursive = false);
void readDeclareDatatype(LExpr* sort, LExprList* datatype);
void readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool codatatype = false);
TermAlgebraConstructor* buildTermAlgebraConstructor(vstring constrName, TermList taSort,
Stack<vstring> destructorNames, TermStack argSorts);
/**
* Parse result of parsing an smtlib term (which can be of sort Bool and therefore represented in vampire by a formula)
*/
struct ParseResult {
/** Construct special separator value */
ParseResult() : formula(true), frm(nullptr) {
sort = TermList(0, true);
}
bool isSeparator() { return sort.isSpecialVar() && formula && !frm; }
bool isSharedTerm() { return !formula && (!trm.isTerm() || trm.term()->shared()); }
/** Construct ParseResult from a formula */
ParseResult(Formula* frm) : sort(AtomicSort::boolSort()), formula(true), frm(frm) {}
/** Construct ParseResult from a term of a given sort */
ParseResult(TermList sort, TermList trm) : sort(sort), formula(false), trm(trm) {}
TermList sort;
bool formula;
/** The label assigned to this formula using the ":named" annotation of SMT-LIB2;
* empty string means no label. */
vstring label;
union {
Formula* frm;
TermList trm;
};
/**
* Try interpreting ParseResult as a formula
* (which may involve unwrapping a formula special term
* or wrapping a Bool sorted term as BoolTermFormula)
* and indicate success by returning true.
*/
bool asFormula(Formula*& resFrm);
/**
* Interpret ParseResult as term
* and return its vampire sort (which may be Sorts::SRT_BOOL).
*/
TermList asTerm(TermList& resTrm);
/**
* Records a label for the formula represented by this `ParserResult`,
* resulting from a ":named" SMT-LIB2 annotation.
*/
void setLabel(vstring l){ label = l; }
/**
* Helper that attaches a label to a `Formula`
* if a label is recorded for this `ParserResult`.
* Returns the formula.
*/
Formula* attachLabelToFormula(Formula* frm);
vstring toString();
};
/** Return Theory::Interpretation for overloaded arithmetic comparison operators based on their argSort (either Int or Real) */
Interpretation getFormulaSymbolInterpretation(FormulaSymbol fs, TermList firstArgSort);
/** Return Theory::Interpretation for overloaded unary minus operator based on its argSort (either Int or Real) */
Interpretation getUnaryMinusInterpretation(TermList argSort);
/** Return Theory::Interpretation for overloaded arithmetic operators based on its argSort (either Int or Real) */
Interpretation getTermSymbolInterpretation(TermSymbol ts, TermList firstArgSort);
// global parsing data structures -- BEGIN
/** For generating fresh vampire variables */
unsigned _nextVar;
/** < termlist, vampire sort id > */
typedef pair<TermList,TermList> SortedTerm;
/** mast an identifier to SortedTerm */
typedef DHMap<vstring,SortedTerm> TermLookup;
typedef Stack<TermLookup*> Scopes;
/** Stack of parsing contexts:
* for variables from quantifiers and
* for symbols bound by let (which are variables from smtlib perspective,
* but require a true function/predicate symbol by vampire )
*/
Scopes _scopes;
/**
* Stack of partial results used by parseTermOrFormula below.
*/
Stack<ParseResult> _results;
/**
* Possible operations during parsing a term.
*/
enum ParseOperation {
// general top level parsing request
PO_PARSE, // takes LExpr*
// when parsing "(something args...)" the following operation will be scheduled for "something"
PO_PARSE_APPLICATION, // takes LExpr* (the whole term again, for better error reporting)
// after "(something args...)" is parsed the following makes sure that there is exactly one proper result on the result stack above a previously inserted separator
PO_CHECK_ARITY, // takes LExpr* (again the whole, just for error reporting)
// this is a special operation for handling :named labels
PO_LABEL, // takes a LExpr* of the label to be applied to the top _result
// these two are intermediate cases for handling let
PO_LET_PREPARE_LOOKUP, // takes LExpr* (the whole let expression again, why not)
PO_LET_END, // takes LExpr* (the whole let expression again, why not)
PO_MATCH_CASE_START, // takes LExpr*, a list containing the matched term, pattern, case
PO_MATCH_CASE_END, // takes LExpr*, a list containing the matched term, pattern, case
PO_MATCH_END // takes LExpr* (the whole match again)
};
/**
* Main smtlib term parsing stack.
*/
Stack<pair<ParseOperation,LExpr*> > _todo;
// global parsing data structures -- END
// a few helper functions enabling the body of parseTermOrFormula be of reasonable size
void complainAboutArgShortageOrWrongSorts(const vstring& symbolClass, LExpr* exp) NO_RETURN;
void parseLetBegin(LExpr* exp);
void parseLetPrepareLookup(LExpr* exp);
void parseLetEnd(LExpr* exp);
bool isTermAlgebraConstructor(const vstring& name);
void parseMatchBegin(LExpr* exp);
void parseMatchCaseStart(LExpr* exp);
void parseMatchCaseEnd(LExpr* exp);
void parseMatchEnd(LExpr* exp);
void parseQuantBegin(LExpr* exp);
void parseAnnotatedTerm(LExpr* exp);
/** Scope's are filled by forall, exists, and let */
bool parseAsScopeLookup(const vstring& id);
/** Currently either numeral or decimal */
bool parseAsSpecConstant(const vstring& id);
/** Declared or defined functions (and predicates) - which includes 0-arity ones */
bool parseAsUserDefinedSymbol(const vstring& id, LExpr* exp);
/** Whatever is built-in and looks like a formula from vampire perspective (see FormulaSymbol)
* - includes the second half of parsing quantifiers */
bool parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp);
/** Whatever is built-in and looks like a term from vampire perspective (see TermSymbol)
* - excludes parts for dealing with let */
bool parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp);
/** Parsing things like "((_ divisible 5) x)" */
void parseRankedFunctionApplication(LExpr* exp);
/**
* Main term parsing routine.
* Assumes "global parsing data structures" initialized.
* Returns the body's value as a ParseResult.
*
* Currently unsupported features (see http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf):
* - qualified identifiers "(as f s)"
* - hexadecimal, binary and string spec_constants
* - :named expressions "(! (> x y) :named p1)" cause a user error.
* They could also be ignored, but smtlib dictates that
* 1) the named term has to be closed (needs an extra check),
* 2) the new name can be used elsewhere (also already in the term being parsed in the in-order traversal)
* So the proper behavior would be more difficult to support.
* - "define-funs-rec" and "define-fun-rec"; syntactically these would be fine,
* but any reasonable use will rely on some well-founded semantics which can only be supported with care
*
* Ignored feature:
* - quantifier patterns: " (forall (( x0 A) (x1 A) (x2 A)) (! (=> (and (r x0 x1) (r x1 x2 )) (r x0 x2 )) : pattern ((r x0 x1) (r x1 x2 )) : pattern ((p x0 a)) ))
* the patter information is lost and the pattern data is not checked semantically.
*
* Violates standard:
* - requires variables under a single quantifier to be distinct
* - the rule that "variables cannot have the same name as a theory function symbol in the same scope" is currently ignored
*/
ParseResult parseTermOrFormula(LExpr* body);
/**
* Handle "assert" entry.
*
* On success results in a single formula added to _formulas.
*/
void readAssert(LExpr* body);
/**
* Unofficial command
*
* Behaves like conjecture declaration in TPTP
*/
void readAssertNot(LExpr* body);
/**
* Unofficial command
*
* Behaves like assert, but marks body clause as external theory axiom.
* Assumes that body is already fully simplified (as this is usual the case for theory axioms).
*/
void readAssertTheory(LExpr* body);
/**
* Unofficial command
*
* Behaves like conjecture declaration in TPTP
*/
void colorSymbol(const vstring& name, Color color);
/**
* Units collected during parsing.
*/
UnitList* _formulas;
/**
* To support a mechanism for dealing with large arithmetic constants.
* Adapted from the tptp parser.
*/
Set<vstring> _overflow;
/**
* Toplevel parsing dispatch for a benchmark.
*/
void readBenchmark(LExprList* bench);
};
}
#endif // __SMTLIB2__