1 /********************* */
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
12 ** \brief Definitions of SMT2 constants.
14 ** Definitions of SMT2 constants.
16 #include "parser/smt2/smt2.h"
20 #include "base/check.h"
21 #include "expr/type.h"
22 #include "options/options.h"
23 #include "parser/antlr_input.h"
24 #include "parser/parser.h"
25 #include "parser/smt2/smt2_input.h"
26 #include "util/bitvector.h"
28 // ANTLR defines these, which is really bad!
35 Smt2::Smt2(api::Solver
* solver
, Input
* input
, bool strictMode
, bool parseOnly
)
36 : Parser(solver
, input
, strictMode
, parseOnly
),
40 if (!strictModeEnabled())
46 void Smt2::addArithmeticOperators() {
47 addOperator(api::PLUS
, "+");
48 addOperator(api::MINUS
, "-");
49 // api::MINUS is converted to api::UMINUS if there is only a single operand
50 Parser::addOperator(api::UMINUS
);
51 addOperator(api::MULT
, "*");
52 addOperator(api::LT
, "<");
53 addOperator(api::LEQ
, "<=");
54 addOperator(api::GT
, ">");
55 addOperator(api::GEQ
, ">=");
57 if (!strictModeEnabled())
59 // NOTE: this operator is non-standard
60 addOperator(api::POW
, "^");
64 void Smt2::addTranscendentalOperators()
66 addOperator(api::EXPONENTIAL
, "exp");
67 addOperator(api::SINE
, "sin");
68 addOperator(api::COSINE
, "cos");
69 addOperator(api::TANGENT
, "tan");
70 addOperator(api::COSECANT
, "csc");
71 addOperator(api::SECANT
, "sec");
72 addOperator(api::COTANGENT
, "cot");
73 addOperator(api::ARCSINE
, "arcsin");
74 addOperator(api::ARCCOSINE
, "arccos");
75 addOperator(api::ARCTANGENT
, "arctan");
76 addOperator(api::ARCCOSECANT
, "arccsc");
77 addOperator(api::ARCSECANT
, "arcsec");
78 addOperator(api::ARCCOTANGENT
, "arccot");
79 addOperator(api::SQRT
, "sqrt");
82 void Smt2::addQuantifiersOperators()
84 if (!strictModeEnabled())
86 addOperator(api::INST_CLOSURE
, "inst-closure");
90 void Smt2::addBitvectorOperators() {
91 addOperator(api::BITVECTOR_CONCAT
, "concat");
92 addOperator(api::BITVECTOR_NOT
, "bvnot");
93 addOperator(api::BITVECTOR_AND
, "bvand");
94 addOperator(api::BITVECTOR_OR
, "bvor");
95 addOperator(api::BITVECTOR_NEG
, "bvneg");
96 addOperator(api::BITVECTOR_PLUS
, "bvadd");
97 addOperator(api::BITVECTOR_MULT
, "bvmul");
98 addOperator(api::BITVECTOR_UDIV
, "bvudiv");
99 addOperator(api::BITVECTOR_UREM
, "bvurem");
100 addOperator(api::BITVECTOR_SHL
, "bvshl");
101 addOperator(api::BITVECTOR_LSHR
, "bvlshr");
102 addOperator(api::BITVECTOR_ULT
, "bvult");
103 addOperator(api::BITVECTOR_NAND
, "bvnand");
104 addOperator(api::BITVECTOR_NOR
, "bvnor");
105 addOperator(api::BITVECTOR_XOR
, "bvxor");
106 addOperator(api::BITVECTOR_XNOR
, "bvxnor");
107 addOperator(api::BITVECTOR_COMP
, "bvcomp");
108 addOperator(api::BITVECTOR_SUB
, "bvsub");
109 addOperator(api::BITVECTOR_SDIV
, "bvsdiv");
110 addOperator(api::BITVECTOR_SREM
, "bvsrem");
111 addOperator(api::BITVECTOR_SMOD
, "bvsmod");
112 addOperator(api::BITVECTOR_ASHR
, "bvashr");
113 addOperator(api::BITVECTOR_ULE
, "bvule");
114 addOperator(api::BITVECTOR_UGT
, "bvugt");
115 addOperator(api::BITVECTOR_UGE
, "bvuge");
116 addOperator(api::BITVECTOR_SLT
, "bvslt");
117 addOperator(api::BITVECTOR_SLE
, "bvsle");
118 addOperator(api::BITVECTOR_SGT
, "bvsgt");
119 addOperator(api::BITVECTOR_SGE
, "bvsge");
120 addOperator(api::BITVECTOR_REDOR
, "bvredor");
121 addOperator(api::BITVECTOR_REDAND
, "bvredand");
123 addIndexedOperator(api::BITVECTOR_EXTRACT
, api::BITVECTOR_EXTRACT
, "extract");
124 addIndexedOperator(api::BITVECTOR_REPEAT
, api::BITVECTOR_REPEAT
, "repeat");
126 api::BITVECTOR_ZERO_EXTEND
, api::BITVECTOR_ZERO_EXTEND
, "zero_extend");
128 api::BITVECTOR_SIGN_EXTEND
, api::BITVECTOR_SIGN_EXTEND
, "sign_extend");
130 api::BITVECTOR_ROTATE_LEFT
, api::BITVECTOR_ROTATE_LEFT
, "rotate_left");
132 api::BITVECTOR_ROTATE_RIGHT
, api::BITVECTOR_ROTATE_RIGHT
, "rotate_right");
135 void Smt2::addDatatypesOperators()
137 Parser::addOperator(api::APPLY_CONSTRUCTOR
);
138 Parser::addOperator(api::APPLY_TESTER
);
139 Parser::addOperator(api::APPLY_SELECTOR
);
141 if (!strictModeEnabled())
143 addOperator(api::DT_SIZE
, "dt.size");
147 void Smt2::addStringOperators() {
150 getSolver()->mkTerm(api::REGEXP_STAR
, getSolver()->mkRegexpSigma()));
151 addOperator(api::STRING_CONCAT
, "str.++");
152 addOperator(api::STRING_LENGTH
, "str.len");
153 addOperator(api::STRING_SUBSTR
, "str.substr");
154 addOperator(api::STRING_CONTAINS
, "str.contains");
155 addOperator(api::STRING_CHARAT
, "str.at");
156 addOperator(api::STRING_INDEXOF
, "str.indexof");
157 addOperator(api::STRING_REPLACE
, "str.replace");
158 addOperator(api::STRING_PREFIX
, "str.prefixof");
159 addOperator(api::STRING_SUFFIX
, "str.suffixof");
160 addOperator(api::STRING_FROM_CODE
, "str.from_code");
161 addOperator(api::STRING_IS_DIGIT
, "str.is_digit");
162 addOperator(api::STRING_REPLACE_RE
, "str.replace_re");
163 addOperator(api::STRING_REPLACE_RE_ALL
, "str.replace_re_all");
164 if (!strictModeEnabled())
166 addOperator(api::STRING_UPDATE
, "str.update");
167 addOperator(api::STRING_TOLOWER
, "str.tolower");
168 addOperator(api::STRING_TOUPPER
, "str.toupper");
169 addOperator(api::STRING_REV
, "str.rev");
171 addOperator(api::SEQ_CONCAT
, "seq.++");
172 addOperator(api::SEQ_LENGTH
, "seq.len");
173 addOperator(api::SEQ_EXTRACT
, "seq.extract");
174 addOperator(api::SEQ_UPDATE
, "seq.update");
175 addOperator(api::SEQ_AT
, "seq.at");
176 addOperator(api::SEQ_CONTAINS
, "seq.contains");
177 addOperator(api::SEQ_INDEXOF
, "seq.indexof");
178 addOperator(api::SEQ_REPLACE
, "seq.replace");
179 addOperator(api::SEQ_PREFIX
, "seq.prefixof");
180 addOperator(api::SEQ_SUFFIX
, "seq.suffixof");
181 addOperator(api::SEQ_REV
, "seq.rev");
182 addOperator(api::SEQ_REPLACE_ALL
, "seq.replace_all");
183 addOperator(api::SEQ_UNIT
, "seq.unit");
184 addOperator(api::SEQ_NTH
, "seq.nth");
186 // at the moment, we only use this syntax for smt2.6
187 if (getLanguage() == language::input::LANG_SMTLIB_V2_6
188 || getLanguage() == language::input::LANG_SYGUS_V2
)
190 addOperator(api::STRING_FROM_INT
, "str.from_int");
191 addOperator(api::STRING_TO_INT
, "str.to_int");
192 addOperator(api::STRING_IN_REGEXP
, "str.in_re");
193 addOperator(api::STRING_TO_REGEXP
, "str.to_re");
194 addOperator(api::STRING_TO_CODE
, "str.to_code");
195 addOperator(api::STRING_REPLACE_ALL
, "str.replace_all");
199 addOperator(api::STRING_FROM_INT
, "int.to.str");
200 addOperator(api::STRING_TO_INT
, "str.to.int");
201 addOperator(api::STRING_IN_REGEXP
, "str.in.re");
202 addOperator(api::STRING_TO_REGEXP
, "str.to.re");
203 addOperator(api::STRING_TO_CODE
, "str.code");
204 addOperator(api::STRING_REPLACE_ALL
, "str.replaceall");
207 addOperator(api::REGEXP_CONCAT
, "re.++");
208 addOperator(api::REGEXP_UNION
, "re.union");
209 addOperator(api::REGEXP_INTER
, "re.inter");
210 addOperator(api::REGEXP_STAR
, "re.*");
211 addOperator(api::REGEXP_PLUS
, "re.+");
212 addOperator(api::REGEXP_OPT
, "re.opt");
213 addIndexedOperator(api::REGEXP_REPEAT
, api::REGEXP_REPEAT
, "re.^");
214 addIndexedOperator(api::REGEXP_LOOP
, api::REGEXP_LOOP
, "re.loop");
215 addOperator(api::REGEXP_RANGE
, "re.range");
216 addOperator(api::REGEXP_COMPLEMENT
, "re.comp");
217 addOperator(api::REGEXP_DIFF
, "re.diff");
218 addOperator(api::STRING_LT
, "str.<");
219 addOperator(api::STRING_LEQ
, "str.<=");
222 void Smt2::addFloatingPointOperators() {
223 addOperator(api::FLOATINGPOINT_FP
, "fp");
224 addOperator(api::FLOATINGPOINT_EQ
, "fp.eq");
225 addOperator(api::FLOATINGPOINT_ABS
, "fp.abs");
226 addOperator(api::FLOATINGPOINT_NEG
, "fp.neg");
227 addOperator(api::FLOATINGPOINT_PLUS
, "fp.add");
228 addOperator(api::FLOATINGPOINT_SUB
, "fp.sub");
229 addOperator(api::FLOATINGPOINT_MULT
, "fp.mul");
230 addOperator(api::FLOATINGPOINT_DIV
, "fp.div");
231 addOperator(api::FLOATINGPOINT_FMA
, "fp.fma");
232 addOperator(api::FLOATINGPOINT_SQRT
, "fp.sqrt");
233 addOperator(api::FLOATINGPOINT_REM
, "fp.rem");
234 addOperator(api::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
235 addOperator(api::FLOATINGPOINT_MIN
, "fp.min");
236 addOperator(api::FLOATINGPOINT_MAX
, "fp.max");
237 addOperator(api::FLOATINGPOINT_LEQ
, "fp.leq");
238 addOperator(api::FLOATINGPOINT_LT
, "fp.lt");
239 addOperator(api::FLOATINGPOINT_GEQ
, "fp.geq");
240 addOperator(api::FLOATINGPOINT_GT
, "fp.gt");
241 addOperator(api::FLOATINGPOINT_ISN
, "fp.isNormal");
242 addOperator(api::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
243 addOperator(api::FLOATINGPOINT_ISZ
, "fp.isZero");
244 addOperator(api::FLOATINGPOINT_ISINF
, "fp.isInfinite");
245 addOperator(api::FLOATINGPOINT_ISNAN
, "fp.isNaN");
246 addOperator(api::FLOATINGPOINT_ISNEG
, "fp.isNegative");
247 addOperator(api::FLOATINGPOINT_ISPOS
, "fp.isPositive");
248 addOperator(api::FLOATINGPOINT_TO_REAL
, "fp.to_real");
250 addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC
,
251 api::FLOATINGPOINT_TO_FP_GENERIC
,
253 addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
254 api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
257 api::FLOATINGPOINT_TO_UBV
, api::FLOATINGPOINT_TO_UBV
, "fp.to_ubv");
259 api::FLOATINGPOINT_TO_SBV
, api::FLOATINGPOINT_TO_SBV
, "fp.to_sbv");
261 if (!strictModeEnabled())
263 addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
264 api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
266 addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
267 api::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
269 addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL
,
270 api::FLOATINGPOINT_TO_FP_REAL
,
272 addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
273 api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
278 void Smt2::addSepOperators() {
279 addOperator(api::SEP_STAR
, "sep");
280 addOperator(api::SEP_PTO
, "pto");
281 addOperator(api::SEP_WAND
, "wand");
282 addOperator(api::SEP_EMP
, "emp");
283 Parser::addOperator(api::SEP_STAR
);
284 Parser::addOperator(api::SEP_PTO
);
285 Parser::addOperator(api::SEP_WAND
);
286 Parser::addOperator(api::SEP_EMP
);
289 void Smt2::addCoreSymbols()
291 defineType("Bool", d_solver
->getBooleanSort());
292 defineVar("true", d_solver
->mkTrue());
293 defineVar("false", d_solver
->mkFalse());
294 addOperator(api::AND
, "and");
295 addOperator(api::DISTINCT
, "distinct");
296 addOperator(api::EQUAL
, "=");
297 addOperator(api::IMPLIES
, "=>");
298 addOperator(api::ITE
, "ite");
299 addOperator(api::NOT
, "not");
300 addOperator(api::OR
, "or");
301 addOperator(api::XOR
, "xor");
304 void Smt2::addOperator(api::Kind kind
, const std::string
& name
)
306 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
308 Parser::addOperator(kind
);
309 operatorKindMap
[name
] = kind
;
312 void Smt2::addIndexedOperator(api::Kind tKind
,
314 const std::string
& name
)
316 Parser::addOperator(tKind
);
317 d_indexedOpKindMap
[name
] = opKind
;
320 api::Kind
Smt2::getOperatorKind(const std::string
& name
) const
322 // precondition: isOperatorEnabled(name)
323 return operatorKindMap
.find(name
)->second
;
326 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
327 return operatorKindMap
.find(name
) != operatorKindMap
.end();
330 bool Smt2::isTheoryEnabled(theory::TheoryId theory
) const
332 return d_logic
.isTheoryEnabled(theory
);
335 bool Smt2::isHoEnabled() const
337 return getLogic().isHigherOrder() && d_solver
->getOptions().getUfHo();
340 bool Smt2::logicIsSet() {
344 api::Term
Smt2::getExpressionForNameAndType(const std::string
& name
,
347 if (isAbstractValue(name
))
349 return mkAbstractValue(name
);
351 return Parser::getExpressionForNameAndType(name
, t
);
354 bool Smt2::getTesterName(api::Term cons
, std::string
& name
)
356 if ((v2_6() || sygus_v2()) && strictModeEnabled())
358 // 2.6 or above uses indexed tester symbols, if we are in strict mode,
359 // we do not automatically define is-cons for constructor cons.
362 std::stringstream ss
;
368 api::Term
Smt2::mkIndexedConstant(const std::string
& name
,
369 const std::vector
<uint64_t>& numerals
)
371 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
))
375 return d_solver
->mkPosInf(numerals
[0], numerals
[1]);
377 else if (name
== "-oo")
379 return d_solver
->mkNegInf(numerals
[0], numerals
[1]);
381 else if (name
== "NaN")
383 return d_solver
->mkNaN(numerals
[0], numerals
[1]);
385 else if (name
== "+zero")
387 return d_solver
->mkPosZero(numerals
[0], numerals
[1]);
389 else if (name
== "-zero")
391 return d_solver
->mkNegZero(numerals
[0], numerals
[1]);
395 if (d_logic
.isTheoryEnabled(theory::THEORY_BV
) && name
.find("bv") == 0)
397 std::string bvStr
= name
.substr(2);
398 return d_solver
->mkBitVector(numerals
[0], bvStr
, 10);
401 // NOTE: Theory parametric constants go here
403 parseError(std::string("Unknown indexed literal `") + name
+ "'");
407 api::Op
Smt2::mkIndexedOp(const std::string
& name
,
408 const std::vector
<uint64_t>& numerals
)
410 const auto& kIt
= d_indexedOpKindMap
.find(name
);
411 if (kIt
!= d_indexedOpKindMap
.end())
413 api::Kind k
= (*kIt
).second
;
414 if (numerals
.size() == 1)
416 return d_solver
->mkOp(k
, numerals
[0]);
418 else if (numerals
.size() == 2)
420 return d_solver
->mkOp(k
, numerals
[0], numerals
[1]);
424 parseError(std::string("Unknown indexed function `") + name
+ "'");
428 api::Term
Smt2::bindDefineFunRec(
429 const std::string
& fname
,
430 const std::vector
<std::pair
<std::string
, api::Sort
>>& sortedVarNames
,
432 std::vector
<api::Term
>& flattenVars
)
434 std::vector
<api::Sort
> sorts
;
435 for (const std::pair
<std::string
, api::Sort
>& svn
: sortedVarNames
)
437 sorts
.push_back(svn
.second
);
440 // make the flattened function type, add bound variables
441 // to flattenVars if the defined function was given a function return type.
442 api::Sort ft
= mkFlatFunctionType(sorts
, t
, flattenVars
);
445 return bindVar(fname
, ft
, ExprManager::VAR_FLAG_NONE
, true);
448 void Smt2::pushDefineFunRecScope(
449 const std::vector
<std::pair
<std::string
, api::Sort
>>& sortedVarNames
,
451 const std::vector
<api::Term
>& flattenVars
,
452 std::vector
<api::Term
>& bvs
,
455 pushScope(bindingLevel
);
457 // bound variables are those that are explicitly named in the preamble
458 // of the define-fun(s)-rec command, we define them here
459 for (const std::pair
<std::string
, api::Sort
>& svn
: sortedVarNames
)
461 api::Term v
= bindBoundVar(svn
.first
, svn
.second
);
465 bvs
.insert(bvs
.end(), flattenVars
.begin(), flattenVars
.end());
470 d_seenSetLogic
= false;
471 d_logic
= LogicInfo();
472 operatorKindMap
.clear();
473 d_lastNamedTerm
= std::pair
<api::Term
, std::string
>();
474 this->Parser::reset();
476 if( !strictModeEnabled() ) {
481 void Smt2::resetAssertions() {
482 // Remove all declarations except the ones at level 0.
483 while (this->scopeLevel() > 0) {
488 Smt2::SynthFunFactory::SynthFunFactory(
490 const std::string
& id
,
493 std::vector
<std::pair
<std::string
, api::Sort
>>& sortedVarNames
)
494 : d_smt2(smt2
), d_id(id
), d_sort(range
), d_isInv(isInv
)
498 smt2
->parseError("Must supply return type for synth-fun.");
500 if (range
.isFunction())
502 smt2
->parseError("Cannot use synth-fun with function return type.");
505 std::vector
<api::Sort
> varSorts
;
506 for (const std::pair
<std::string
, api::Sort
>& p
: sortedVarNames
)
508 varSorts
.push_back(p
.second
);
511 api::Sort funSort
= varSorts
.empty()
513 : d_smt2
->d_solver
->mkFunctionSort(varSorts
, range
);
515 // we do not allow overloading for synth fun
516 d_fun
= d_smt2
->bindBoundVar(id
, funSort
);
518 Debug("parser-sygus") << "Define synth fun : " << id
<< std::endl
;
520 d_smt2
->pushScope(true);
521 d_sygusVars
= d_smt2
->bindBoundVars(sortedVarNames
);
524 std::unique_ptr
<Command
> Smt2::SynthFunFactory::mkCommand(api::Grammar
* grammar
)
526 Debug("parser-sygus") << "...read synth fun " << d_id
<< std::endl
;
528 return std::unique_ptr
<Command
>(new SynthFunCommand(
529 d_smt2
->d_solver
, d_id
, d_fun
, d_sygusVars
, d_sort
, d_isInv
, grammar
));
532 std::unique_ptr
<Command
> Smt2::invConstraint(
533 const std::vector
<std::string
>& names
)
535 checkThatLogicIsSet();
536 Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl
;
537 Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl
;
539 if (names
.size() != 4)
542 "Bad syntax for inv-constraint: expected 4 "
546 std::vector
<api::Term
> terms
;
547 for (const std::string
& name
: names
)
549 if (!isDeclared(name
))
551 std::stringstream ss
;
552 ss
<< "Function " << name
<< " in inv-constraint is not defined.";
553 parseError(ss
.str());
556 terms
.push_back(getVariable(name
));
559 return std::unique_ptr
<Command
>(
560 new SygusInvConstraintCommand(api::termVectorToExprs(terms
)));
563 Command
* Smt2::setLogic(std::string name
, bool fromCommand
)
569 parseError("Only one set-logic is allowed.");
571 d_seenSetLogic
= true;
575 // If the logic is forced, we ignore all set-logic requests from commands.
576 return new EmptyCommand();
583 // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
586 if (!d_logic
.isQuantified())
588 warning("Logics in sygus are assumed to contain quantifiers.");
589 warning("Omit QF_ from the logic to avoid this warning.");
593 // Core theory belongs to every logic
596 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
597 Parser::addOperator(api::APPLY_UF
);
599 if (!strictModeEnabled() && d_logic
.hasCardinalityConstraints())
601 addOperator(api::CARDINALITY_CONSTRAINT
, "fmf.card");
602 addOperator(api::CARDINALITY_VALUE
, "fmf.card.val");
606 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
607 if(d_logic
.areIntegersUsed()) {
608 defineType("Int", d_solver
->getIntegerSort());
609 addArithmeticOperators();
610 addOperator(api::INTS_DIVISION
, "div");
611 addOperator(api::INTS_MODULUS
, "mod");
612 addOperator(api::ABS
, "abs");
613 addIndexedOperator(api::DIVISIBLE
, api::DIVISIBLE
, "divisible");
616 if (d_logic
.areRealsUsed())
618 defineType("Real", d_solver
->getRealSort());
619 addArithmeticOperators();
620 addOperator(api::DIVISION
, "/");
621 if (!strictModeEnabled())
623 addOperator(api::ABS
, "abs");
627 if (d_logic
.areIntegersUsed() && d_logic
.areRealsUsed())
629 addOperator(api::TO_INTEGER
, "to_int");
630 addOperator(api::IS_INTEGER
, "is_int");
631 addOperator(api::TO_REAL
, "to_real");
634 if (d_logic
.areTranscendentalsUsed())
636 defineVar("real.pi", d_solver
->mkTerm(api::PI
));
637 addTranscendentalOperators();
639 if (!strictModeEnabled())
641 // integer version of AND
642 addIndexedOperator(api::IAND
, api::IAND
, "iand");
646 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAYS
)) {
647 addOperator(api::SELECT
, "select");
648 addOperator(api::STORE
, "store");
649 addOperator(api::EQ_RANGE
, "eqrange");
652 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
653 addBitvectorOperators();
655 if (!strictModeEnabled() && d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)
656 && d_logic
.areIntegersUsed())
658 // Conversions between bit-vectors and integers
659 addOperator(api::BITVECTOR_TO_NAT
, "bv2nat");
661 api::INT_TO_BITVECTOR
, api::INT_TO_BITVECTOR
, "int2bv");
665 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
666 const std::vector
<api::Sort
> types
;
667 defineType("Tuple", d_solver
->mkTupleSort(types
));
668 addDatatypesOperators();
671 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
672 defineVar("emptyset", d_solver
->mkEmptySet(d_solver
->getNullSort()));
673 // the Boolean sort is a placeholder here since we don't have type info
674 // without type annotation
675 defineVar("univset", d_solver
->mkUniverseSet(d_solver
->getBooleanSort()));
677 addOperator(api::UNION
, "union");
678 addOperator(api::INTERSECTION
, "intersection");
679 addOperator(api::SETMINUS
, "setminus");
680 addOperator(api::SUBSET
, "subset");
681 addOperator(api::MEMBER
, "member");
682 addOperator(api::SINGLETON
, "singleton");
683 addOperator(api::INSERT
, "insert");
684 addOperator(api::CARD
, "card");
685 addOperator(api::COMPLEMENT
, "complement");
686 addOperator(api::CHOOSE
, "choose");
687 addOperator(api::IS_SINGLETON
, "is_singleton");
688 addOperator(api::JOIN
, "join");
689 addOperator(api::PRODUCT
, "product");
690 addOperator(api::TRANSPOSE
, "transpose");
691 addOperator(api::TCLOSURE
, "tclosure");
694 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
695 defineType("String", d_solver
->getStringSort());
696 defineType("RegLan", d_solver
->getRegExpSort());
697 defineType("Int", d_solver
->getIntegerSort());
699 if (getLanguage() == language::input::LANG_SMTLIB_V2_6
700 || getLanguage() == language::input::LANG_SYGUS_V2
)
702 defineVar("re.none", d_solver
->mkRegexpEmpty());
706 defineVar("re.nostr", d_solver
->mkRegexpEmpty());
708 defineVar("re.allchar", d_solver
->mkRegexpSigma());
710 // Boolean is a placeholder
711 defineVar("seq.empty",
712 d_solver
->mkEmptySequence(d_solver
->getBooleanSort()));
714 addStringOperators();
717 if(d_logic
.isQuantified()) {
718 addQuantifiersOperators();
721 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
722 defineType("RoundingMode", d_solver
->getRoundingModeSort());
723 defineType("Float16", d_solver
->mkFloatingPointSort(5, 11));
724 defineType("Float32", d_solver
->mkFloatingPointSort(8, 24));
725 defineType("Float64", d_solver
->mkFloatingPointSort(11, 53));
726 defineType("Float128", d_solver
->mkFloatingPointSort(15, 113));
728 defineVar("RNE", d_solver
->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN
));
729 defineVar("roundNearestTiesToEven",
730 d_solver
->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN
));
731 defineVar("RNA", d_solver
->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY
));
732 defineVar("roundNearestTiesToAway",
733 d_solver
->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY
));
734 defineVar("RTP", d_solver
->mkRoundingMode(api::ROUND_TOWARD_POSITIVE
));
735 defineVar("roundTowardPositive",
736 d_solver
->mkRoundingMode(api::ROUND_TOWARD_POSITIVE
));
737 defineVar("RTN", d_solver
->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE
));
738 defineVar("roundTowardNegative",
739 d_solver
->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE
));
740 defineVar("RTZ", d_solver
->mkRoundingMode(api::ROUND_TOWARD_ZERO
));
741 defineVar("roundTowardZero",
742 d_solver
->mkRoundingMode(api::ROUND_TOWARD_ZERO
));
744 addFloatingPointOperators();
747 if (d_logic
.isTheoryEnabled(theory::THEORY_SEP
)) {
748 // the Boolean sort is a placeholder here since we don't have type info
749 // without type annotation
750 defineVar("sep.nil", d_solver
->mkSepNil(d_solver
->getBooleanSort()));
756 new SetBenchmarkLogicCommand(sygus() ? d_logic
.getLogicString() : name
);
757 cmd
->setMuted(!fromCommand
);
759 } /* Smt2::setLogic() */
761 api::Grammar
* Smt2::mkGrammar(const std::vector
<api::Term
>& boundVars
,
762 const std::vector
<api::Term
>& ntSymbols
)
764 d_allocGrammars
.emplace_back(new api::Grammar(
765 std::move(d_solver
->mkSygusGrammar(boundVars
, ntSymbols
))));
766 return d_allocGrammars
.back().get();
769 bool Smt2::sygus() const
771 InputLanguage ilang
= getLanguage();
772 return ilang
== language::input::LANG_SYGUS_V2
;
775 bool Smt2::sygus_v2() const
777 return getLanguage() == language::input::LANG_SYGUS_V2
;
780 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
784 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
788 void Smt2::checkThatLogicIsSet()
792 if (strictModeEnabled())
794 parseError("set-logic must appear before this point.");
798 Command
* cmd
= nullptr;
801 cmd
= setLogic(getForcedLogic(), false);
805 warning("No set-logic command was given before this point.");
806 warning("CVC4 will make all theories available.");
808 "Consider setting a stricter logic for (likely) better "
810 warning("To suppress this warning in the future use (set-logic ALL).");
812 cmd
= setLogic("ALL", false);
819 void Smt2::checkLogicAllowsFreeSorts()
821 if (!d_logic
.isTheoryEnabled(theory::THEORY_UF
)
822 && !d_logic
.isTheoryEnabled(theory::THEORY_ARRAYS
)
823 && !d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)
824 && !d_logic
.isTheoryEnabled(theory::THEORY_SETS
))
826 parseErrorLogic("Free sort symbols not allowed in ");
830 void Smt2::checkLogicAllowsFunctions()
832 if (!d_logic
.isTheoryEnabled(theory::THEORY_UF
))
835 "Functions (of non-zero arity) cannot "
836 "be declared in logic "
837 + d_logic
.getLogicString() + " unless option --uf-ho is used");
841 /* The include are managed in the lexer but called in the parser */
842 // Inspired by http://www.antlr3.org/api/C/interop.html
844 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
845 Debug("parser") << "Including " << filename
<< std::endl
;
846 // Create a new input stream and take advantage of built in stream stacking
847 // in C target runtime.
849 pANTLR3_INPUT_STREAM in
;
850 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
851 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
852 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
853 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
854 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
856 Debug("parser") << "Can't open " << filename
<< std::endl
;
859 // Same thing as the predefined PUSHSTREAM(in);
860 lexer
->pushCharStream(lexer
, in
);
862 //lexer->rec->state->tokenStartCharIndex = -10;
863 //lexer->emit(lexer);
865 // Note that the input stream is not closed when it EOFs, I don't bother
866 // to do it here, but it is up to you to track streams created like this
867 // and destroy them when the whole parse session is complete. Remember that you
868 // don't want to do this until all tokens have been manipulated all the way through
869 // your tree parsers etc as the token does not store the text it just refers
870 // back to the input stream and trying to get the text for it will abort if you
871 // close the input stream too early.
873 //TODO what said before
877 void Smt2::includeFile(const std::string
& filename
) {
878 // security for online version
879 if(!canIncludeFile()) {
880 parseError("include-file feature was disabled for this run.");
884 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
885 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
886 // get the name of the current stream "Does it work inside an include?"
887 const std::string inputName
= ai
->getInputStreamName();
889 // Find the directory of the current input file
891 size_t pos
= inputName
.rfind('/');
892 if(pos
!= std::string::npos
) {
893 path
= std::string(inputName
, 0, pos
+ 1);
895 path
.append(filename
);
896 if(!newInputStream(path
, lexer
)) {
897 parseError("Couldn't open include file `" + path
+ "'");
900 bool Smt2::isAbstractValue(const std::string
& name
)
902 return name
.length() >= 2 && name
[0] == '@' && name
[1] != '0'
903 && name
.find_first_not_of("0123456789", 1) == std::string::npos
;
906 api::Term
Smt2::mkAbstractValue(const std::string
& name
)
908 assert(isAbstractValue(name
));
910 return d_solver
->mkAbstractValue(name
.substr(1));
913 InputLanguage
Smt2::getLanguage() const
915 return d_solver
->getOptions().getInputLanguage();
918 void Smt2::parseOpApplyTypeAscription(ParseOp
& p
, api::Sort type
)
920 Debug("parser") << "parseOpApplyTypeAscription : " << p
<< " " << type
922 // (as const (Array T1 T2))
923 if (p
.d_kind
== api::CONST_ARRAY
)
927 std::stringstream ss
;
928 ss
<< "expected array constant term, but cast is not of array type"
930 << "cast type: " << type
;
931 parseError(ss
.str());
936 if (p
.d_expr
.isNull())
938 Trace("parser-overloading")
939 << "Getting variable expression with name " << p
.d_name
<< " and type "
940 << type
<< std::endl
;
941 // get the variable expression for the type
942 if (isDeclared(p
.d_name
, SYM_VARIABLE
))
944 p
.d_expr
= getExpressionForNameAndType(p
.d_name
, type
);
945 p
.d_name
= std::string("");
947 if (p
.d_expr
.isNull())
949 std::stringstream ss
;
950 ss
<< "Could not resolve expression with name " << p
.d_name
951 << " and type " << type
<< std::endl
;
952 parseError(ss
.str());
955 Trace("parser-qid") << "Resolve ascription " << type
<< " on " << p
.d_expr
;
956 Trace("parser-qid") << " " << p
.d_expr
.getKind() << " " << p
.d_expr
.getSort();
957 Trace("parser-qid") << std::endl
;
958 // otherwise, we process the type ascription
959 p
.d_expr
= applyTypeAscription(p
.d_expr
, type
);
962 api::Term
Smt2::parseOpToExpr(ParseOp
& p
)
964 Debug("parser") << "parseOpToExpr: " << p
<< std::endl
;
966 if (p
.d_kind
!= api::NULL_EXPR
|| !p
.d_type
.isNull())
969 "Bad syntax for qualified identifier operator in term position.");
971 else if (!p
.d_expr
.isNull())
975 else if (!isDeclared(p
.d_name
, SYM_VARIABLE
))
977 std::stringstream ss
;
978 ss
<< "Symbol " << p
.d_name
<< " is not declared.";
979 parseError(ss
.str());
983 expr
= getExpressionForName(p
.d_name
);
985 assert(!expr
.isNull());
989 api::Term
Smt2::applyParseOp(ParseOp
& p
, std::vector
<api::Term
>& args
)
991 bool isBuiltinOperator
= false;
992 // the builtin kind of the overall return expression
993 api::Kind kind
= api::NULL_EXPR
;
994 // First phase: process the operator
995 if (Debug
.isOn("parser"))
997 Debug("parser") << "applyParseOp: " << p
<< " to:" << std::endl
;
998 for (std::vector
<api::Term
>::iterator i
= args
.begin(); i
!= args
.end();
1001 Debug("parser") << "++ " << *i
<< std::endl
;
1005 if (p
.d_kind
!= api::NULL_EXPR
)
1007 // It is a special case, e.g. tupSel or array constant specification.
1008 // We have to wait until the arguments are parsed to resolve it.
1010 else if (!p
.d_expr
.isNull())
1012 // An explicit operator, e.g. an apply function
1013 api::Kind fkind
= getKindForFunction(p
.d_expr
);
1014 if (fkind
!= api::UNDEFINED_KIND
)
1016 // Some operators may require a specific kind.
1017 // Testers are handled differently than other indexed operators,
1018 // since they require a kind.
1020 Debug("parser") << "Got function kind " << kind
<< " for expression "
1023 args
.insert(args
.begin(), p
.d_expr
);
1025 else if (!p
.d_op
.isNull())
1027 // it was given an operator
1032 isBuiltinOperator
= isOperatorEnabled(p
.d_name
);
1033 if (isBuiltinOperator
)
1035 // a builtin operator, convert to kind
1036 kind
= getOperatorKind(p
.d_name
);
1040 // A non-built-in function application, get the expression
1041 checkDeclaration(p
.d_name
, CHECK_DECLARED
, SYM_VARIABLE
);
1042 api::Term v
= getVariable(p
.d_name
);
1045 checkFunctionLike(v
);
1046 kind
= getKindForFunction(v
);
1047 args
.insert(args
.begin(), v
);
1051 // Overloaded symbol?
1052 // Could not find the expression. It may be an overloaded symbol,
1053 // in which case we may find it after knowing the types of its
1055 std::vector
<api::Sort
> argTypes
;
1056 for (std::vector
<api::Term
>::iterator i
= args
.begin(); i
!= args
.end();
1059 argTypes
.push_back((*i
).getSort());
1061 api::Term fop
= getOverloadedFunctionForTypes(p
.d_name
, argTypes
);
1064 checkFunctionLike(fop
);
1065 kind
= getKindForFunction(fop
);
1066 args
.insert(args
.begin(), fop
);
1071 "Cannot find unambiguous overloaded function for argument "
1077 // Second phase: apply the arguments to the parse op
1078 const Options
& opts
= d_solver
->getOptions();
1079 // handle special cases
1080 if (p
.d_kind
== api::CONST_ARRAY
&& !p
.d_type
.isNull())
1082 if (args
.size() != 1)
1084 parseError("Too many arguments to array constant.");
1086 api::Term constVal
= args
[0];
1087 if (!constVal
.isConst())
1089 // To parse array constants taking reals whose values are specified by
1090 // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
1091 // the fact that (/ 1 3) is the division of constants 1 and 3, and not
1092 // the resulting constant rational value. Thus, we must construct the
1093 // resulting rational here. This also is applied for integral real values
1094 // like 5.0 which are converted to (/ 5 1) to distinguish them from
1095 // integer constants. We must ensure numerator and denominator are
1096 // constant and the denominator is non-zero.
1097 if (constVal
.getKind() == api::DIVISION
&& constVal
[0].isConst()
1098 && constVal
[1].isConst()
1099 && !constVal
[1].getExpr().getConst
<Rational
>().isZero())
1101 std::stringstream sdiv
;
1102 sdiv
<< constVal
[0] << "/" << constVal
[1];
1103 constVal
= d_solver
->mkReal(sdiv
.str());
1105 if (!constVal
.isConst())
1107 std::stringstream ss
;
1108 ss
<< "expected constant term inside array constant, but found "
1109 << "nonconstant term:" << std::endl
1110 << "the term: " << constVal
;
1111 parseError(ss
.str());
1114 if (!p
.d_type
.getArrayElementSort().isComparableTo(constVal
.getSort()))
1116 std::stringstream ss
;
1117 ss
<< "type mismatch inside array constant term:" << std::endl
1118 << "array type: " << p
.d_type
<< std::endl
1119 << "expected const type: " << p
.d_type
.getArrayElementSort()
1121 << "computed const type: " << constVal
.getSort();
1122 parseError(ss
.str());
1124 api::Term ret
= d_solver
->mkConstArray(p
.d_type
, constVal
);
1125 Debug("parser") << "applyParseOp: return store all " << ret
<< std::endl
;
1128 else if (p
.d_kind
== api::APPLY_SELECTOR
&& !p
.d_expr
.isNull())
1130 // tuple selector case
1131 Integer x
= p
.d_expr
.getExpr().getConst
<Rational
>().getNumerator();
1132 if (!x
.fitsUnsignedInt())
1134 parseError("index of tupSel is larger than size of unsigned int");
1136 unsigned int n
= x
.toUnsignedInt();
1137 if (args
.size() != 1)
1139 parseError("tupSel should only be applied to one tuple argument");
1141 api::Sort t
= args
[0].getSort();
1144 parseError("tupSel applied to non-tuple");
1146 size_t length
= t
.getTupleLength();
1149 std::stringstream ss
;
1150 ss
<< "tuple is of length " << length
<< "; cannot access index " << n
;
1151 parseError(ss
.str());
1153 const api::Datatype
& dt
= t
.getDatatype();
1154 api::Term ret
= d_solver
->mkTerm(
1155 api::APPLY_SELECTOR
, dt
[0][n
].getSelectorTerm(), args
[0]);
1156 Debug("parser") << "applyParseOp: return selector " << ret
<< std::endl
;
1159 else if (p
.d_kind
!= api::NULL_EXPR
)
1161 // it should not have an expression or type specified at this point
1162 if (!p
.d_expr
.isNull() || !p
.d_type
.isNull())
1164 std::stringstream ss
;
1165 ss
<< "Could not process parsed qualified identifier kind " << p
.d_kind
;
1166 parseError(ss
.str());
1168 // otherwise it is a simple application
1171 else if (isBuiltinOperator
)
1173 if (!opts
.getUfHo() && (kind
== api::EQUAL
|| kind
== api::DISTINCT
))
1175 // need --uf-ho if these operators are applied over function args
1176 for (std::vector
<api::Term
>::iterator i
= args
.begin(); i
!= args
.end();
1179 if ((*i
).getSort().isFunction())
1182 "Cannot apply equalty to functions unless --uf-ho is set.");
1186 if (!strictModeEnabled() && (kind
== api::AND
|| kind
== api::OR
)
1187 && args
.size() == 1)
1189 // Unary AND/OR can be replaced with the argument.
1190 Debug("parser") << "applyParseOp: return unary " << args
[0] << std::endl
;
1193 else if (kind
== api::MINUS
&& args
.size() == 1)
1195 api::Term ret
= d_solver
->mkTerm(api::UMINUS
, args
[0]);
1196 Debug("parser") << "applyParseOp: return uminus " << ret
<< std::endl
;
1199 if (kind
== api::EQ_RANGE
&& d_solver
->getOption("arrays-exp") != "true")
1202 "eqrange predicate requires option --arrays-exp to be enabled.");
1204 api::Term ret
= d_solver
->mkTerm(kind
, args
);
1205 Debug("parser") << "applyParseOp: return default builtin " << ret
1210 if (args
.size() >= 2)
1212 // may be partially applied function, in this case we use HO_APPLY
1213 api::Sort argt
= args
[0].getSort();
1214 if (argt
.isFunction())
1216 unsigned arity
= argt
.getFunctionArity();
1217 if (args
.size() - 1 < arity
)
1219 if (!opts
.getUfHo())
1221 parseError("Cannot partially apply functions unless --uf-ho is set.");
1223 Debug("parser") << "Partial application of " << args
[0];
1224 Debug("parser") << " : #argTypes = " << arity
;
1225 Debug("parser") << ", #args = " << args
.size() - 1 << std::endl
;
1226 api::Term ret
= d_solver
->mkTerm(api::HO_APPLY
, args
);
1227 Debug("parser") << "applyParseOp: return curry higher order " << ret
1229 // must curry the partial application
1236 api::Term ret
= d_solver
->mkTerm(op
, args
);
1237 Debug("parser") << "applyParseOp: return op : " << ret
<< std::endl
;
1240 if (kind
== api::NULL_EXPR
)
1242 // should never happen in the new API
1243 parseError("do not know how to process parse op");
1245 Debug("parser") << "Try default term construction for kind " << kind
1246 << " #args = " << args
.size() << "..." << std::endl
;
1247 api::Term ret
= d_solver
->mkTerm(kind
, args
);
1248 Debug("parser") << "applyParseOp: return : " << ret
<< std::endl
;
1252 api::Term
Smt2::setNamedAttribute(api::Term
& expr
, const SExpr
& sexpr
)
1254 if (!sexpr
.isKeyword())
1256 parseError("improperly formed :named annotation");
1258 std::string name
= sexpr
.getValue();
1259 checkUserSymbol(name
);
1260 // ensure expr is a closed subterm
1261 if (expr
.getExpr().hasFreeVariable())
1263 std::stringstream ss
;
1264 ss
<< ":named annotations can only name terms that are closed";
1265 parseError(ss
.str());
1267 // check that sexpr is a fresh function symbol, and reserve it
1268 reserveSymbolAtAssertionLevel(name
);
1270 api::Term func
= bindVar(name
, expr
.getSort(), ExprManager::VAR_FLAG_DEFINED
);
1271 // remember the last term to have been given a :named attribute
1272 setLastNamedTerm(expr
, name
);
1276 api::Term
Smt2::mkAnd(const std::vector
<api::Term
>& es
)
1280 return d_solver
->mkTrue();
1282 else if (es
.size() == 1)
1288 return d_solver
->mkTerm(api::AND
, es
);
1292 } // namespace parser
1293 }/* CVC4 namespace */