1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Kshitij Bansal, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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"
18 #include "api/cvc4cpp.h"
19 #include "expr/type.h"
20 #include "options/options.h"
21 #include "parser/antlr_input.h"
22 #include "parser/parser.h"
23 #include "parser/smt1/smt1.h"
24 #include "parser/smt2/smt2_input.h"
25 #include "printer/sygus_print_callback.h"
26 #include "smt/command.h"
27 #include "util/bitvector.h"
31 // ANTLR defines these, which is really bad!
38 Smt2::Smt2(api::Solver
* solver
, Input
* input
, bool strictMode
, bool parseOnly
)
39 : Parser(solver
, input
, strictMode
, parseOnly
), d_logicSet(false)
41 if (!strictModeEnabled())
43 addTheory(Smt2::THEORY_CORE
);
47 void Smt2::addArithmeticOperators() {
48 Parser::addOperator(kind::PLUS
);
49 Parser::addOperator(kind::MINUS
);
50 Parser::addOperator(kind::UMINUS
);
51 Parser::addOperator(kind::MULT
);
52 Parser::addOperator(kind::LT
);
53 Parser::addOperator(kind::LEQ
);
54 Parser::addOperator(kind::GT
);
55 Parser::addOperator(kind::GEQ
);
57 // NOTE: this operator is non-standard
58 addOperator(kind::POW
, "^");
61 void Smt2::addTranscendentalOperators()
63 addOperator(kind::EXPONENTIAL
, "exp");
64 addOperator(kind::SINE
, "sin");
65 addOperator(kind::COSINE
, "cos");
66 addOperator(kind::TANGENT
, "tan");
67 addOperator(kind::COSECANT
, "csc");
68 addOperator(kind::SECANT
, "sec");
69 addOperator(kind::COTANGENT
, "cot");
70 addOperator(kind::ARCSINE
, "arcsin");
71 addOperator(kind::ARCCOSINE
, "arccos");
72 addOperator(kind::ARCTANGENT
, "arctan");
73 addOperator(kind::ARCCOSECANT
, "arccsc");
74 addOperator(kind::ARCSECANT
, "arcsec");
75 addOperator(kind::ARCCOTANGENT
, "arccot");
76 addOperator(kind::SQRT
, "sqrt");
79 void Smt2::addBitvectorOperators() {
80 addOperator(kind::BITVECTOR_CONCAT
, "concat");
81 addOperator(kind::BITVECTOR_NOT
, "bvnot");
82 addOperator(kind::BITVECTOR_AND
, "bvand");
83 addOperator(kind::BITVECTOR_OR
, "bvor");
84 addOperator(kind::BITVECTOR_NEG
, "bvneg");
85 addOperator(kind::BITVECTOR_PLUS
, "bvadd");
86 addOperator(kind::BITVECTOR_MULT
, "bvmul");
87 addOperator(kind::BITVECTOR_UDIV
, "bvudiv");
88 addOperator(kind::BITVECTOR_UREM
, "bvurem");
89 addOperator(kind::BITVECTOR_SHL
, "bvshl");
90 addOperator(kind::BITVECTOR_LSHR
, "bvlshr");
91 addOperator(kind::BITVECTOR_ULT
, "bvult");
92 addOperator(kind::BITVECTOR_NAND
, "bvnand");
93 addOperator(kind::BITVECTOR_NOR
, "bvnor");
94 addOperator(kind::BITVECTOR_XOR
, "bvxor");
95 addOperator(kind::BITVECTOR_XNOR
, "bvxnor");
96 addOperator(kind::BITVECTOR_COMP
, "bvcomp");
97 addOperator(kind::BITVECTOR_SUB
, "bvsub");
98 addOperator(kind::BITVECTOR_SDIV
, "bvsdiv");
99 addOperator(kind::BITVECTOR_SREM
, "bvsrem");
100 addOperator(kind::BITVECTOR_SMOD
, "bvsmod");
101 addOperator(kind::BITVECTOR_ASHR
, "bvashr");
102 addOperator(kind::BITVECTOR_ULE
, "bvule");
103 addOperator(kind::BITVECTOR_UGT
, "bvugt");
104 addOperator(kind::BITVECTOR_UGE
, "bvuge");
105 addOperator(kind::BITVECTOR_SLT
, "bvslt");
106 addOperator(kind::BITVECTOR_SLE
, "bvsle");
107 addOperator(kind::BITVECTOR_SGT
, "bvsgt");
108 addOperator(kind::BITVECTOR_SGE
, "bvsge");
109 addOperator(kind::BITVECTOR_REDOR
, "bvredor");
110 addOperator(kind::BITVECTOR_REDAND
, "bvredand");
112 Parser::addOperator(kind::BITVECTOR_BITOF
);
113 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
114 Parser::addOperator(kind::BITVECTOR_REPEAT
);
115 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
116 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
117 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
118 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
120 Parser::addOperator(kind::INT_TO_BITVECTOR
);
121 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
124 void Smt2::addStringOperators() {
125 addOperator(kind::STRING_CONCAT
, "str.++");
126 addOperator(kind::STRING_LENGTH
, "str.len");
127 addOperator(kind::STRING_SUBSTR
, "str.substr" );
128 addOperator(kind::STRING_STRCTN
, "str.contains" );
129 addOperator(kind::STRING_CHARAT
, "str.at" );
130 addOperator(kind::STRING_STRIDOF
, "str.indexof" );
131 addOperator(kind::STRING_STRREPL
, "str.replace" );
132 addOperator(kind::STRING_PREFIX
, "str.prefixof" );
133 addOperator(kind::STRING_SUFFIX
, "str.suffixof" );
134 // at the moment, we only use this syntax for smt2.6.1
135 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
)
137 addOperator(kind::STRING_ITOS
, "str.from-int");
138 addOperator(kind::STRING_STOI
, "str.to-int");
139 addOperator(kind::STRING_IN_REGEXP
, "str.in-re");
140 addOperator(kind::STRING_TO_REGEXP
, "str.to-re");
144 addOperator(kind::STRING_ITOS
, "int.to.str");
145 addOperator(kind::STRING_STOI
, "str.to.int");
146 addOperator(kind::STRING_IN_REGEXP
, "str.in.re");
147 addOperator(kind::STRING_TO_REGEXP
, "str.to.re");
150 addOperator(kind::REGEXP_CONCAT
, "re.++");
151 addOperator(kind::REGEXP_UNION
, "re.union");
152 addOperator(kind::REGEXP_INTER
, "re.inter");
153 addOperator(kind::REGEXP_STAR
, "re.*");
154 addOperator(kind::REGEXP_PLUS
, "re.+");
155 addOperator(kind::REGEXP_OPT
, "re.opt");
156 addOperator(kind::REGEXP_RANGE
, "re.range");
157 addOperator(kind::REGEXP_LOOP
, "re.loop");
158 addOperator(kind::STRING_CODE
, "str.code");
159 addOperator(kind::STRING_LT
, "str.<");
160 addOperator(kind::STRING_LEQ
, "str.<=");
163 void Smt2::addFloatingPointOperators() {
164 addOperator(kind::FLOATINGPOINT_FP
, "fp");
165 addOperator(kind::FLOATINGPOINT_EQ
, "fp.eq");
166 addOperator(kind::FLOATINGPOINT_ABS
, "fp.abs");
167 addOperator(kind::FLOATINGPOINT_NEG
, "fp.neg");
168 addOperator(kind::FLOATINGPOINT_PLUS
, "fp.add");
169 addOperator(kind::FLOATINGPOINT_SUB
, "fp.sub");
170 addOperator(kind::FLOATINGPOINT_MULT
, "fp.mul");
171 addOperator(kind::FLOATINGPOINT_DIV
, "fp.div");
172 addOperator(kind::FLOATINGPOINT_FMA
, "fp.fma");
173 addOperator(kind::FLOATINGPOINT_SQRT
, "fp.sqrt");
174 addOperator(kind::FLOATINGPOINT_REM
, "fp.rem");
175 addOperator(kind::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
176 addOperator(kind::FLOATINGPOINT_MIN
, "fp.min");
177 addOperator(kind::FLOATINGPOINT_MAX
, "fp.max");
178 addOperator(kind::FLOATINGPOINT_LEQ
, "fp.leq");
179 addOperator(kind::FLOATINGPOINT_LT
, "fp.lt");
180 addOperator(kind::FLOATINGPOINT_GEQ
, "fp.geq");
181 addOperator(kind::FLOATINGPOINT_GT
, "fp.gt");
182 addOperator(kind::FLOATINGPOINT_ISN
, "fp.isNormal");
183 addOperator(kind::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
184 addOperator(kind::FLOATINGPOINT_ISZ
, "fp.isZero");
185 addOperator(kind::FLOATINGPOINT_ISINF
, "fp.isInfinite");
186 addOperator(kind::FLOATINGPOINT_ISNAN
, "fp.isNaN");
187 addOperator(kind::FLOATINGPOINT_ISNEG
, "fp.isNegative");
188 addOperator(kind::FLOATINGPOINT_ISPOS
, "fp.isPositive");
189 addOperator(kind::FLOATINGPOINT_TO_REAL
, "fp.to_real");
191 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_GENERIC
);
192 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
193 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
194 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
195 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
196 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
197 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
198 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
201 void Smt2::addSepOperators() {
202 addOperator(kind::SEP_STAR
, "sep");
203 addOperator(kind::SEP_PTO
, "pto");
204 addOperator(kind::SEP_WAND
, "wand");
205 addOperator(kind::SEP_EMP
, "emp");
206 Parser::addOperator(kind::SEP_STAR
);
207 Parser::addOperator(kind::SEP_PTO
);
208 Parser::addOperator(kind::SEP_WAND
);
209 Parser::addOperator(kind::SEP_EMP
);
212 void Smt2::addTheory(Theory theory
) {
215 addOperator(kind::SELECT
, "select");
216 addOperator(kind::STORE
, "store");
219 case THEORY_BITVECTORS
:
220 addBitvectorOperators();
224 defineType("Bool", getExprManager()->booleanType());
225 defineVar("true", getExprManager()->mkConst(true));
226 defineVar("false", getExprManager()->mkConst(false));
227 Parser::addOperator(kind::AND
);
228 Parser::addOperator(kind::DISTINCT
);
229 Parser::addOperator(kind::EQUAL
);
230 Parser::addOperator(kind::IMPLIES
);
231 Parser::addOperator(kind::ITE
);
232 Parser::addOperator(kind::NOT
);
233 Parser::addOperator(kind::OR
);
234 Parser::addOperator(kind::XOR
);
237 case THEORY_REALS_INTS
:
238 defineType("Real", getExprManager()->realType());
239 Parser::addOperator(kind::DIVISION
);
240 addOperator(kind::TO_INTEGER
, "to_int");
241 addOperator(kind::IS_INTEGER
, "is_int");
242 addOperator(kind::TO_REAL
, "to_real");
243 // falling through on purpose, to add Ints part of Reals_Ints
245 defineType("Int", getExprManager()->integerType());
246 addArithmeticOperators();
247 addOperator(kind::INTS_DIVISION
, "div");
248 addOperator(kind::INTS_MODULUS
, "mod");
249 addOperator(kind::ABS
, "abs");
250 Parser::addOperator(kind::DIVISIBLE
);
254 defineType("Real", getExprManager()->realType());
255 addArithmeticOperators();
256 Parser::addOperator(kind::DIVISION
);
259 case THEORY_TRANSCENDENTALS
: addTranscendentalOperators(); break;
261 case THEORY_QUANTIFIERS
:
265 addOperator(kind::UNION
, "union");
266 addOperator(kind::INTERSECTION
, "intersection");
267 addOperator(kind::SETMINUS
, "setminus");
268 addOperator(kind::SUBSET
, "subset");
269 addOperator(kind::MEMBER
, "member");
270 addOperator(kind::SINGLETON
, "singleton");
271 addOperator(kind::INSERT
, "insert");
272 addOperator(kind::CARD
, "card");
273 addOperator(kind::COMPLEMENT
, "complement");
274 addOperator(kind::JOIN
, "join");
275 addOperator(kind::PRODUCT
, "product");
276 addOperator(kind::TRANSPOSE
, "transpose");
277 addOperator(kind::TCLOSURE
, "tclosure");
280 case THEORY_DATATYPES
:
282 const std::vector
<Type
> types
;
283 defineType("Tuple", getExprManager()->mkTupleType(types
));
284 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
285 Parser::addOperator(kind::APPLY_TESTER
);
286 Parser::addOperator(kind::APPLY_SELECTOR
);
287 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
292 defineType("String", getExprManager()->stringType());
293 defineType("RegLan", getExprManager()->regExpType());
294 defineType("Int", getExprManager()->integerType());
295 addStringOperators();
299 Parser::addOperator(kind::APPLY_UF
);
303 defineType("RoundingMode", getExprManager()->roundingModeType());
304 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
305 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
306 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
307 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
308 addFloatingPointOperators();
316 std::stringstream ss
;
317 ss
<< "internal error: unsupported theory " << theory
;
318 throw ParserException(ss
.str());
322 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
323 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
325 Parser::addOperator(kind
);
326 operatorKindMap
[name
] = kind
;
329 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
330 // precondition: isOperatorEnabled(name)
331 return operatorKindMap
.find(name
)->second
;
334 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
335 return operatorKindMap
.find(name
) != operatorKindMap
.end();
338 bool Smt2::isTheoryEnabled(Theory theory
) const {
341 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAYS
);
342 case THEORY_BITVECTORS
:
343 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
346 case THEORY_DATATYPES
:
347 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
349 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
350 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
352 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
353 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
354 case THEORY_REALS_INTS
:
355 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
356 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
357 case THEORY_QUANTIFIERS
:
358 return d_logic
.isQuantified();
360 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
362 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
364 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
366 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
368 return d_logic
.isTheoryEnabled(theory::THEORY_SEP
);
370 std::stringstream ss
;
371 ss
<< "internal error: unsupported theory " << theory
;
372 throw ParserException(ss
.str());
376 bool Smt2::logicIsSet() {
380 Expr
Smt2::getExpressionForNameAndType(const std::string
& name
, Type t
) {
381 if(sygus() && name
[0]=='-' &&
382 name
.find_first_not_of("0123456789", 1) == std::string::npos
) {
383 //allow unary minus in sygus
384 return getExprManager()->mkConst(Rational(name
));
385 }else if(isAbstractValue(name
)) {
386 return mkAbstractValue(name
);
388 return Parser::getExpressionForNameAndType(name
, t
);
392 Expr
Smt2::mkDefineFunRec(
393 const std::string
& fname
,
394 const std::vector
<std::pair
<std::string
, Type
> >& sortedVarNames
,
396 std::vector
<Expr
>& flattenVars
)
398 std::vector
<Type
> sorts
;
399 for (const std::pair
<std::string
, CVC4::Type
>& svn
: sortedVarNames
)
401 sorts
.push_back(svn
.second
);
404 // make the flattened function type, add bound variables
405 // to flattenVars if the defined function was given a function return type.
406 Type ft
= mkFlatFunctionType(sorts
, t
, flattenVars
);
409 return mkVar(fname
, ft
, ExprManager::VAR_FLAG_NONE
, true);
412 void Smt2::pushDefineFunRecScope(
413 const std::vector
<std::pair
<std::string
, Type
> >& sortedVarNames
,
415 const std::vector
<Expr
>& flattenVars
,
416 std::vector
<Expr
>& bvs
,
419 pushScope(bindingLevel
);
421 // bound variables are those that are explicitly named in the preamble
422 // of the define-fun(s)-rec command, we define them here
423 for (const std::pair
<std::string
, CVC4::Type
>& svn
: sortedVarNames
)
425 Expr v
= mkBoundVar(svn
.first
, svn
.second
);
429 bvs
.insert(bvs
.end(), flattenVars
.begin(), flattenVars
.end());
434 d_logic
= LogicInfo();
435 operatorKindMap
.clear();
436 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
437 this->Parser::reset();
439 if( !strictModeEnabled() ) {
440 addTheory(Smt2::THEORY_CORE
);
444 void Smt2::resetAssertions() {
445 // Remove all declarations except the ones at level 0.
446 while (this->scopeLevel() > 0) {
451 void Smt2::setLogic(std::string name
) {
454 // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
455 if(name
== "Arrays") {
457 }else if(name
== "Reals") {
463 if(logicIsForced()) {
464 d_logic
= getForcedLogic();
469 // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
472 if (!d_logic
.isQuantified())
474 warning("Logics in sygus are assumed to contain quantifiers.");
475 warning("Omit QF_ from the logic to avoid this warning.");
477 // get unlocked copy, modify, copy and relock
478 LogicInfo
log(d_logic
.getUnlockedCopy());
479 log
.enableQuantifiers();
480 log
.enableTheory(theory::THEORY_UF
);
481 log
.enableTheory(theory::THEORY_DATATYPES
);
482 log
.enableIntegers();
483 log
.enableHigherOrder();
488 // Core theory belongs to every logic
489 addTheory(THEORY_CORE
);
491 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
492 addTheory(THEORY_UF
);
495 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
496 if(d_logic
.areIntegersUsed()) {
497 if(d_logic
.areRealsUsed()) {
498 addTheory(THEORY_REALS_INTS
);
500 addTheory(THEORY_INTS
);
502 } else if(d_logic
.areRealsUsed()) {
503 addTheory(THEORY_REALS
);
506 if (d_logic
.areTranscendentalsUsed())
508 addTheory(THEORY_TRANSCENDENTALS
);
512 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAYS
)) {
513 addTheory(THEORY_ARRAYS
);
516 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
517 addTheory(THEORY_BITVECTORS
);
520 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
521 addTheory(THEORY_DATATYPES
);
524 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
525 addTheory(THEORY_SETS
);
528 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
529 addTheory(THEORY_STRINGS
);
532 if(d_logic
.isQuantified()) {
533 addTheory(THEORY_QUANTIFIERS
);
536 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
537 addTheory(THEORY_FP
);
540 if (d_logic
.isTheoryEnabled(theory::THEORY_SEP
)) {
541 addTheory(THEORY_SEP
);
544 }/* Smt2::setLogic() */
546 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
550 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
554 void Smt2::checkThatLogicIsSet() {
555 if( ! logicIsSet() ) {
556 if(strictModeEnabled()) {
557 parseError("set-logic must appear before this point.");
559 warning("No set-logic command was given before this point.");
560 warning("CVC4 will make all theories available.");
561 warning("Consider setting a stricter logic for (likely) better performance.");
562 warning("To suppress this warning in the future use (set-logic ALL).");
566 Command
* c
= new SetBenchmarkLogicCommand("ALL");
573 /* The include are managed in the lexer but called in the parser */
574 // Inspired by http://www.antlr3.org/api/C/interop.html
576 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
577 Debug("parser") << "Including " << filename
<< std::endl
;
578 // Create a new input stream and take advantage of built in stream stacking
579 // in C target runtime.
581 pANTLR3_INPUT_STREAM in
;
582 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
583 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
584 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
585 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
586 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
588 Debug("parser") << "Can't open " << filename
<< std::endl
;
591 // Same thing as the predefined PUSHSTREAM(in);
592 lexer
->pushCharStream(lexer
, in
);
594 //lexer->rec->state->tokenStartCharIndex = -10;
595 //lexer->emit(lexer);
597 // Note that the input stream is not closed when it EOFs, I don't bother
598 // to do it here, but it is up to you to track streams created like this
599 // and destroy them when the whole parse session is complete. Remember that you
600 // don't want to do this until all tokens have been manipulated all the way through
601 // your tree parsers etc as the token does not store the text it just refers
602 // back to the input stream and trying to get the text for it will abort if you
603 // close the input stream too early.
605 //TODO what said before
609 void Smt2::includeFile(const std::string
& filename
) {
610 // security for online version
611 if(!canIncludeFile()) {
612 parseError("include-file feature was disabled for this run.");
616 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
617 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
618 // get the name of the current stream "Does it work inside an include?"
619 const std::string inputName
= ai
->getInputStreamName();
621 // Find the directory of the current input file
623 size_t pos
= inputName
.rfind('/');
624 if(pos
!= std::string::npos
) {
625 path
= std::string(inputName
, 0, pos
+ 1);
627 path
.append(filename
);
628 if(!newInputStream(path
, lexer
)) {
629 parseError("Couldn't open include file `" + path
+ "'");
633 void Smt2::mkSygusVar(const std::string
& name
, const Type
& type
, bool isPrimed
)
637 d_sygusVars
.push_back(mkBoundVar(name
, type
));
639 #ifdef CVC4_ASSERTIONS
642 d_sygusVarPrimed
.push_back(mkBoundVar(name
, type
));
647 void Smt2::mkSygusConstantsForType( const Type
& type
, std::vector
<CVC4::Expr
>& ops
) {
648 if( type
.isInteger() ){
649 ops
.push_back(getExprManager()->mkConst(Rational(0)));
650 ops
.push_back(getExprManager()->mkConst(Rational(1)));
651 }else if( type
.isBitVector() ){
652 unsigned sz
= ((BitVectorType
)type
).getSize();
653 BitVector
bval0(sz
, (unsigned int)0);
654 ops
.push_back( getExprManager()->mkConst(bval0
) );
655 BitVector
bval1(sz
, (unsigned int)1);
656 ops
.push_back( getExprManager()->mkConst(bval1
) );
657 }else if( type
.isBoolean() ){
658 ops
.push_back(getExprManager()->mkConst(true));
659 ops
.push_back(getExprManager()->mkConst(false));
664 // This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
665 // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
666 void Smt2::processSygusGTerm( CVC4::SygusGTerm
& sgt
, int index
,
667 std::vector
< CVC4::Datatype
>& datatypes
,
668 std::vector
< CVC4::Type
>& sorts
,
669 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
670 std::vector
< std::vector
<std::string
> >& cnames
,
671 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
672 std::vector
< bool >& allow_const
,
673 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
674 std::vector
<CVC4::Expr
>& sygus_vars
,
675 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
, std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
,
676 CVC4::Type
& ret
, bool isNested
){
677 if( sgt
.d_gterm_type
==SygusGTerm::gterm_op
|| sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
678 Debug("parser-sygus") << "Add " << sgt
.d_expr
<< " to datatype " << index
680 << (sgt
.d_gterm_type
== SygusGTerm::gterm_let
)
683 Kind newKind
= kind::UNDEFINED_KIND
;
684 //convert to UMINUS if one child of MINUS
685 if( sgt
.d_children
.size()==1 && sgt
.d_expr
==getExprManager()->operatorOf(kind::MINUS
) ){
686 oldKind
= kind::MINUS
;
687 newKind
= kind::UMINUS
;
689 if( newKind
!=kind::UNDEFINED_KIND
){
690 Expr newExpr
= getExprManager()->operatorOf(newKind
);
691 Debug("parser-sygus") << "Replace " << sgt
.d_expr
<< " with " << newExpr
<< std::endl
;
692 sgt
.d_expr
= newExpr
;
693 std::string oldName
= kind::kindToString(oldKind
);
694 std::string newName
= kind::kindToString(newKind
);
696 if((pos
= sgt
.d_name
.find(oldName
, pos
)) != std::string::npos
){
697 sgt
.d_name
.replace(pos
, oldName
.length(), newName
);
700 ops
[index
].push_back( sgt
.d_expr
);
701 cnames
[index
].push_back( sgt
.d_name
);
702 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
703 for( unsigned i
=0; i
<sgt
.d_children
.size(); i
++ ){
704 std::stringstream ss
;
705 ss
<< datatypes
[index
].getName() << "_" << ops
[index
].size() << "_arg_" << i
;
706 std::string sub_dname
= ss
.str();
707 //add datatype for child
709 pushSygusDatatypeDef( null_type
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
710 int sub_dt_index
= datatypes
.size()-1;
713 processSygusGTerm( sgt
.d_children
[i
], sub_dt_index
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
714 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
, true );
715 //process the nested gterm (either pop the last datatype, or flatten the argument)
716 Type tt
= processSygusNestedGTerm( sub_dt_index
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
717 sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
);
718 cargs
[index
].back().push_back(tt
);
720 //if let, must create operator
721 if( sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
722 processSygusLetConstructor( sgt
.d_let_vars
, index
, datatypes
, sorts
, ops
, cnames
, cargs
,
723 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
);
725 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_constant
){
726 if( sgt
.getNumChildren()!=0 ){
727 parseError("Bad syntax for Sygus Constant.");
729 std::vector
< Expr
> consts
;
730 mkSygusConstantsForType( sgt
.d_type
, consts
);
731 Debug("parser-sygus") << "...made " << consts
.size() << " constants." << std::endl
;
732 for( unsigned i
=0; i
<consts
.size(); i
++ ){
733 std::stringstream ss
;
735 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
736 ops
[index
].push_back( consts
[i
] );
737 cnames
[index
].push_back( ss
.str() );
738 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
740 allow_const
[index
] = true;
741 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_variable
|| sgt
.d_gterm_type
==SygusGTerm::gterm_input_variable
){
742 if( sgt
.getNumChildren()!=0 ){
743 parseError("Bad syntax for Sygus Variable.");
745 Debug("parser-sygus") << "...process " << sygus_vars
.size() << " variables." << std::endl
;
746 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
747 if( sygus_vars
[i
].getType()==sgt
.d_type
){
748 std::stringstream ss
;
750 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
751 ops
[index
].push_back( sygus_vars
[i
] );
752 cnames
[index
].push_back( ss
.str() );
753 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
756 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_nested_sort
){
758 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_unresolved
){
760 if( isUnresolvedType(sgt
.d_name
) ){
761 ret
= getSort(sgt
.d_name
);
763 //nested, unresolved symbol...fail
764 std::stringstream ss
;
765 ss
<< "Cannot handle nested unresolved symbol " << sgt
.d_name
<< std::endl
;
766 parseError(ss
.str());
769 //will resolve when adding constructors
770 unresolved_gterm_sym
[index
].push_back(sgt
.d_name
);
772 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_ignore
){
777 bool Smt2::pushSygusDatatypeDef( Type t
, std::string
& dname
,
778 std::vector
< CVC4::Datatype
>& datatypes
,
779 std::vector
< CVC4::Type
>& sorts
,
780 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
781 std::vector
< std::vector
<std::string
> >& cnames
,
782 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
783 std::vector
< bool >& allow_const
,
784 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
786 datatypes
.push_back(Datatype(dname
));
787 ops
.push_back(std::vector
<Expr
>());
788 cnames
.push_back(std::vector
<std::string
>());
789 cargs
.push_back(std::vector
<std::vector
<CVC4::Type
> >());
790 allow_const
.push_back(false);
791 unresolved_gterm_sym
.push_back(std::vector
< std::string
>());
795 bool Smt2::popSygusDatatypeDef( std::vector
< CVC4::Datatype
>& datatypes
,
796 std::vector
< CVC4::Type
>& sorts
,
797 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
798 std::vector
< std::vector
<std::string
> >& cnames
,
799 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
800 std::vector
< bool >& allow_const
,
801 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
803 datatypes
.pop_back();
807 allow_const
.pop_back();
808 unresolved_gterm_sym
.pop_back();
812 Type
Smt2::processSygusNestedGTerm( int sub_dt_index
, std::string
& sub_dname
, std::vector
< CVC4::Datatype
>& datatypes
,
813 std::vector
< CVC4::Type
>& sorts
,
814 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
815 std::vector
< std::vector
<std::string
> >& cnames
,
816 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
817 std::vector
< bool >& allow_const
,
818 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
819 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
820 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
, Type sub_ret
) {
822 Debug("parser-sygus") << "Argument is ";
824 //then, it is the datatype we constructed, which should have a single constructor
825 t
= mkUnresolvedType(sub_dname
);
826 Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t
<< std::endl
;
827 Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs
[sub_dt_index
].size() << std::endl
;
828 if( cargs
[sub_dt_index
].empty() ){
829 parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
831 Expr sop
= ops
[sub_dt_index
][0];
833 if( sop
.getKind() != kind::BUILTIN
&& ( sop
.isConst() || cargs
[sub_dt_index
][0].empty() ) ){
834 curr_t
= sop
.getType();
835 Debug("parser-sygus") << ": it is constant/0-arg cons " << sop
<< " with type " << sop
.getType() << ", debug=" << sop
.isConst() << " " << cargs
[sub_dt_index
][0].size() << std::endl
;
836 // only cache if it is a singleton datatype (has unique expr)
837 if (ops
[sub_dt_index
].size() == 1)
839 sygus_to_builtin_expr
[t
] = sop
;
840 // store that term sop has dedicated sygus type t
841 if (d_sygus_bound_var_type
.find(sop
) == d_sygus_bound_var_type
.end())
843 d_sygus_bound_var_type
[sop
] = t
;
847 std::vector
< Expr
> children
;
848 if( sop
.getKind() != kind::BUILTIN
){
849 children
.push_back( sop
);
851 for( unsigned i
=0; i
<cargs
[sub_dt_index
][0].size(); i
++ ){
852 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[sub_dt_index
][0][i
] );
853 if( it
==sygus_to_builtin_expr
.end() ){
854 if( sygus_to_builtin
.find( cargs
[sub_dt_index
][0][i
] )==sygus_to_builtin
.end() ){
855 std::stringstream ss
;
856 ss
<< "Missing builtin type for type " << cargs
[sub_dt_index
][0][i
] << "!" << std::endl
;
857 ss
<< "Builtin types are currently : " << std::endl
;
858 for( std::map
< CVC4::Type
, CVC4::Type
>::iterator itb
= sygus_to_builtin
.begin(); itb
!= sygus_to_builtin
.end(); ++itb
){
859 ss
<< " " << itb
->first
<< " -> " << itb
->second
<< std::endl
;
861 parseError(ss
.str());
863 Type bt
= sygus_to_builtin
[cargs
[sub_dt_index
][0][i
]];
864 Debug("parser-sygus") << ": child " << i
<< " introduce type elem for " << cargs
[sub_dt_index
][0][i
] << " " << bt
<< std::endl
;
865 std::stringstream ss
;
866 ss
<< t
<< "_x_" << i
;
867 Expr bv
= mkBoundVar(ss
.str(), bt
);
868 children
.push_back( bv
);
869 d_sygus_bound_var_type
[bv
] = cargs
[sub_dt_index
][0][i
];
871 Debug("parser-sygus") << ": child " << i
<< " existing sygus to builtin expr : " << it
->second
<< std::endl
;
872 children
.push_back( it
->second
);
875 Kind sk
= sop
.getKind() != kind::BUILTIN
? kind::APPLY
: getExprManager()->operatorToKind(sop
);
876 Debug("parser-sygus") << ": operator " << sop
<< " with " << sop
.getKind() << " " << sk
<< std::endl
;
877 Expr e
= getExprManager()->mkExpr( sk
, children
);
878 Debug("parser-sygus") << ": constructed " << e
<< ", which has type " << e
.getType() << std::endl
;
879 curr_t
= e
.getType();
880 sygus_to_builtin_expr
[t
] = e
;
882 sorts
[sub_dt_index
] = curr_t
;
883 sygus_to_builtin
[t
] = curr_t
;
885 Debug("parser-sygus") << "simple argument " << t
<< std::endl
;
886 Debug("parser-sygus") << "...removing " << datatypes
.back().getName() << std::endl
;
887 //otherwise, datatype was unecessary
888 //pop argument datatype definition
889 popSygusDatatypeDef( datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
894 void Smt2::processSygusLetConstructor( std::vector
< CVC4::Expr
>& let_vars
,
896 std::vector
< CVC4::Datatype
>& datatypes
,
897 std::vector
< CVC4::Type
>& sorts
,
898 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
899 std::vector
< std::vector
<std::string
> >& cnames
,
900 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
901 std::vector
<CVC4::Expr
>& sygus_vars
,
902 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
903 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
) {
904 std::vector
< CVC4::Expr
> let_define_args
;
906 int dindex
= cargs
[index
].size()-1;
907 Debug("parser-sygus") << "Process let constructor for datatype " << datatypes
[index
].getName() << ", #subtypes = " << cargs
[index
][dindex
].size() << std::endl
;
908 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
909 Debug("parser-sygus") << " " << i
<< " : " << cargs
[index
][dindex
][i
] << std::endl
;
910 if( i
+1==cargs
[index
][dindex
].size() ){
911 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[index
][dindex
][i
] );
912 if( it
!=sygus_to_builtin_expr
.end() ){
913 let_body
= it
->second
;
915 std::stringstream ss
;
916 ss
<< datatypes
[index
].getName() << "_body";
917 let_body
= mkBoundVar(ss
.str(), sygus_to_builtin
[cargs
[index
][dindex
][i
]]);
918 d_sygus_bound_var_type
[let_body
] = cargs
[index
][dindex
][i
];
922 Debug("parser-sygus") << std::endl
;
923 Debug("parser-sygus") << "Body is " << let_body
<< std::endl
;
924 Debug("parser-sygus") << "# let vars = " << let_vars
.size() << std::endl
;
925 for( unsigned i
=0; i
<let_vars
.size(); i
++ ){
926 Debug("parser-sygus") << " let var " << i
<< " : " << let_vars
[i
] << " " << let_vars
[i
].getType() << std::endl
;
927 let_define_args
.push_back( let_vars
[i
] );
930 Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
931 for( unsigned i=start_index; i<datatypes.size(); i++ ){
932 Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
933 if( !cargs[i].empty() ){
934 Debug("parser-sygus") << " operator 0 is " << ops[i][0] << std::endl;
935 Debug("parser-sygus") << " cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
936 for( unsigned j=0; j<cargs[i][0].size(); j++ ){
937 Type bt = sygus_to_builtin[cargs[i][0][j]];
938 Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
943 //last argument is the return, pop
944 cargs
[index
][dindex
].pop_back();
945 collectSygusLetArgs( let_body
, cargs
[index
][dindex
], let_define_args
);
947 Debug("parser-sygus") << "Make define-fun with "
948 << cargs
[index
][dindex
].size()
949 << " operator arguments and " << let_define_args
.size()
950 << " provided arguments..." << std::endl
;
951 if (cargs
[index
][dindex
].size() != let_define_args
.size())
953 std::stringstream ss
;
954 ss
<< "Wrong number of let body terms." << std::endl
;
955 parseError(ss
.str());
957 std::vector
<CVC4::Type
> fsorts
;
958 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
959 Debug("parser-sygus") << " " << i
<< " : " << let_define_args
[i
] << " " << let_define_args
[i
].getType() << " " << cargs
[index
][dindex
][i
] << std::endl
;
960 fsorts
.push_back(let_define_args
[i
].getType());
963 Type ft
= getExprManager()->mkFunctionType(fsorts
, let_body
.getType());
964 std::stringstream ss
;
965 ss
<< datatypes
[index
].getName() << "_let";
966 Expr let_func
= mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
967 d_sygus_defined_funs
.push_back( let_func
);
968 preemptCommand( new DefineFunctionCommand(ss
.str(), let_func
, let_define_args
, let_body
) );
970 ops
[index
].pop_back();
971 ops
[index
].push_back( let_func
);
972 cnames
[index
].pop_back();
973 cnames
[index
].push_back(ss
.str());
975 //mark function as let constructor
976 d_sygus_let_func_to_vars
[let_func
].insert( d_sygus_let_func_to_vars
[let_func
].end(), let_define_args
.begin(), let_define_args
.end() );
977 d_sygus_let_func_to_body
[let_func
] = let_body
;
978 d_sygus_let_func_to_num_input_vars
[let_func
] = let_vars
.size();
982 void Smt2::collectSygusLetArgs( CVC4::Expr e
, std::vector
< CVC4::Type
>& sygusArgs
, std::vector
< CVC4::Expr
>& builtinArgs
) {
983 if( e
.getKind()==kind::BOUND_VARIABLE
){
984 if( std::find( builtinArgs
.begin(), builtinArgs
.end(), e
)==builtinArgs
.end() ){
985 builtinArgs
.push_back( e
);
986 sygusArgs
.push_back( d_sygus_bound_var_type
[e
] );
987 if( d_sygus_bound_var_type
[e
].isNull() ){
988 std::stringstream ss
;
989 ss
<< "While constructing body of let gterm, can't map " << e
<< " to sygus type." << std::endl
;
990 parseError(ss
.str());
994 for( unsigned i
=0; i
<e
.getNumChildren(); i
++ ){
995 collectSygusLetArgs( e
[i
], sygusArgs
, builtinArgs
);
1000 void Smt2::setSygusStartIndex( std::string
& fun
, int startIndex
,
1001 std::vector
< CVC4::Datatype
>& datatypes
,
1002 std::vector
< CVC4::Type
>& sorts
,
1003 std::vector
< std::vector
<CVC4::Expr
> >& ops
) {
1005 CVC4::Datatype tmp_dt
= datatypes
[0];
1006 Type tmp_sort
= sorts
[0];
1007 std::vector
< Expr
> tmp_ops
;
1008 tmp_ops
.insert( tmp_ops
.end(), ops
[0].begin(), ops
[0].end() );
1009 datatypes
[0] = datatypes
[startIndex
];
1010 sorts
[0] = sorts
[startIndex
];
1012 ops
[0].insert( ops
[0].end(), ops
[startIndex
].begin(), ops
[startIndex
].end() );
1013 datatypes
[startIndex
] = tmp_dt
;
1014 sorts
[startIndex
] = tmp_sort
;
1015 ops
[startIndex
].clear();
1016 ops
[startIndex
].insert( ops
[startIndex
].begin(), tmp_ops
.begin(), tmp_ops
.end() );
1017 }else if( startIndex
<0 ){
1018 std::stringstream ss
;
1019 ss
<< "warning: no symbol named Start for synth-fun " << fun
<< std::endl
;
1024 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
1025 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
,
1026 std::vector
<std::string
>& unresolved_gterm_sym
,
1027 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
) {
1028 Debug("parser-sygus") << "Making sygus datatype " << dt
.getName() << std::endl
;
1029 Debug("parser-sygus") << " add constructors..." << std::endl
;
1031 Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt
.getName() << std::endl
;
1032 Debug("parser-sygus") << " add constructors..." << std::endl
;
1033 // size of cnames changes, this loop must check size
1034 for (unsigned i
= 0; i
< cnames
.size(); i
++)
1036 bool is_dup
= false;
1037 bool is_dup_op
= false;
1038 for (unsigned j
= 0; j
< i
; j
++)
1040 if( ops
[i
]==ops
[j
] ){
1042 if( cargs
[i
].size()==cargs
[j
].size() ){
1044 for( unsigned k
=0; k
<cargs
[i
].size(); k
++ ){
1045 if( cargs
[i
][k
]!=cargs
[j
][k
] ){
1056 Debug("parser-sygus") << "SYGUS CONS " << i
<< " : ";
1058 Debug("parser-sygus") << "--> Duplicate gterm : " << ops
[i
] << std::endl
;
1059 ops
.erase( ops
.begin() + i
, ops
.begin() + i
+ 1 );
1060 cnames
.erase( cnames
.begin() + i
, cnames
.begin() + i
+ 1 );
1061 cargs
.erase( cargs
.begin() + i
, cargs
.begin() + i
+ 1 );
1066 std::shared_ptr
<SygusPrintCallback
> spc
;
1069 Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops
[i
]
1071 // make into define-fun
1072 std::vector
<Type
> ltypes
;
1073 for (unsigned j
= 0, size
= cargs
[i
].size(); j
< size
; j
++)
1075 ltypes
.push_back(sygus_to_builtin
[cargs
[i
][j
]]);
1077 std::vector
<Expr
> largs
;
1078 Expr lbvl
= makeSygusBoundVarList(dt
, i
, ltypes
, largs
);
1080 // make the let_body
1081 std::vector
<Expr
> children
;
1082 if (ops
[i
].getKind() != kind::BUILTIN
)
1084 children
.push_back(ops
[i
]);
1086 children
.insert(children
.end(), largs
.begin(), largs
.end());
1087 Kind sk
= ops
[i
].getKind() != kind::BUILTIN
1089 : getExprManager()->operatorToKind(ops
[i
]);
1090 Expr body
= getExprManager()->mkExpr(sk
, children
);
1091 // replace by lambda
1092 ops
[i
] = getExprManager()->mkExpr(kind::LAMBDA
, lbvl
, body
);
1093 Debug("parser-sygus") << " ...replace op : " << ops
[i
] << std::endl
;
1094 // callback prints as the expression
1095 spc
= std::make_shared
<printer::SygusExprPrintCallback
>(body
, largs
);
1099 std::map
<Expr
, Expr
>::iterator it
=
1100 d_sygus_let_func_to_body
.find(ops
[i
]);
1101 if (it
!= d_sygus_let_func_to_body
.end())
1103 Debug("parser-sygus") << "--> Let expression " << ops
[i
] << std::endl
;
1104 Expr let_body
= it
->second
;
1105 std::vector
<Expr
> let_args
= d_sygus_let_func_to_vars
[ops
[i
]];
1106 unsigned let_num_input_args
=
1107 d_sygus_let_func_to_num_input_vars
[ops
[i
]];
1108 // the operator is just the body for the arguments
1109 std::vector
<Type
> ltypes
;
1110 for (unsigned j
= 0, size
= let_args
.size(); j
< size
; j
++)
1112 ltypes
.push_back(let_args
[j
].getType());
1114 std::vector
<Expr
> largs
;
1115 Expr lbvl
= makeSygusBoundVarList(dt
, i
, ltypes
, largs
);
1116 Expr sbody
= let_body
.substitute(let_args
, largs
);
1117 ops
[i
] = getExprManager()->mkExpr(kind::LAMBDA
, lbvl
, sbody
);
1118 Debug("parser-sygus") << " ...replace op : " << ops
[i
] << std::endl
;
1119 // callback prints as a let expression
1120 spc
= std::make_shared
<printer::SygusLetExprPrintCallback
>(
1121 let_body
, let_args
, let_num_input_args
);
1123 else if (ops
[i
].getType().isBitVector() && ops
[i
].isConst())
1125 Debug("parser-sygus") << "--> Bit-vector constant " << ops
[i
] << " ("
1126 << cnames
[i
] << ")" << std::endl
;
1127 // Since there are multiple output formats for bit-vectors and
1128 // we are required by sygus standards to print in the exact input
1129 // format given by the user, we use a print callback to custom print
1131 spc
= std::make_shared
<printer::SygusNamedPrintCallback
>(cnames
[i
]);
1133 else if (isDefinedFunction(ops
[i
]))
1135 Debug("parser-sygus") << "--> Defined function " << ops
[i
]
1137 // turn f into (lammbda (x) (f x))
1138 // in a degenerate case, ops[i] may be a defined constant,
1139 // in which case we do not replace by a lambda.
1140 if (ops
[i
].getType().isFunction())
1142 std::vector
<Type
> ftypes
=
1143 static_cast<FunctionType
>(ops
[i
].getType()).getArgTypes();
1144 std::vector
<Expr
> largs
;
1145 Expr lbvl
= makeSygusBoundVarList(dt
, i
, ftypes
, largs
);
1146 largs
.insert(largs
.begin(), ops
[i
]);
1147 Expr body
= getExprManager()->mkExpr(kind::APPLY
, largs
);
1148 ops
[i
] = getExprManager()->mkExpr(kind::LAMBDA
, lbvl
, body
);
1149 Debug("parser-sygus") << " ...replace op : " << ops
[i
]
1154 ops
[i
] = getExprManager()->mkExpr(kind::APPLY
, ops
[i
]);
1155 Debug("parser-sygus") << " ...replace op : " << ops
[i
]
1158 // keep a callback to say it should be printed with the defined name
1159 spc
= std::make_shared
<printer::SygusNamedPrintCallback
>(cnames
[i
]);
1163 Debug("parser-sygus") << "--> Default case " << ops
[i
] << std::endl
;
1166 // must rename to avoid duplication
1167 std::stringstream ss
;
1168 ss
<< dt
.getName() << "_" << i
<< "_" << cnames
[i
];
1169 cnames
[i
] = ss
.str();
1170 Debug("parser-sygus") << " construct the datatype " << cnames
[i
] << "..."
1172 // add the sygus constructor
1173 dt
.addSygusConstructor(ops
[i
], cnames
[i
], cargs
[i
], spc
);
1174 Debug("parser-sygus") << " finished constructing the datatype"
1179 Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl
;
1180 if( !unresolved_gterm_sym
.empty() ){
1181 std::vector
< Type
> types
;
1182 Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym
.size() << " symbols..." << std::endl
;
1183 for( unsigned i
=0; i
<unresolved_gterm_sym
.size(); i
++ ){
1184 Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym
[i
] << std::endl
;
1185 if( isUnresolvedType(unresolved_gterm_sym
[i
]) ){
1186 Debug("parser-sygus") << " it is an unresolved type." << std::endl
;
1187 Type t
= getSort(unresolved_gterm_sym
[i
]);
1188 if( std::find( types
.begin(), types
.end(), t
)==types
.end() ){
1189 types
.push_back( t
);
1191 Type bt
= dt
.getSygusType();
1192 Debug("parser-sygus") << ": make identity function for " << bt
<< ", argument type " << t
<< std::endl
;
1194 std::stringstream ss
;
1196 Expr var
= mkBoundVar(ss
.str(), bt
);
1197 std::vector
<Expr
> lchildren
;
1198 lchildren
.push_back(
1199 getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, var
));
1200 lchildren
.push_back(var
);
1201 Expr id_op
= getExprManager()->mkExpr(kind::LAMBDA
, lchildren
);
1203 // empty sygus callback (should not be printed)
1204 std::shared_ptr
<SygusPrintCallback
> sepc
=
1205 std::make_shared
<printer::SygusEmptyPrintCallback
>();
1207 //make the sygus argument list
1208 std::vector
< Type
> id_carg
;
1209 id_carg
.push_back( t
);
1210 dt
.addSygusConstructor(id_op
, unresolved_gterm_sym
[i
], id_carg
, sepc
);
1213 ops
.push_back( id_op
);
1216 Debug("parser-sygus") << " ignore. (likely a free let variable)" << std::endl
;
1222 Expr
Smt2::makeSygusBoundVarList(Datatype
& dt
,
1224 const std::vector
<Type
>& ltypes
,
1225 std::vector
<Expr
>& lvars
)
1227 for (unsigned j
= 0, size
= ltypes
.size(); j
< size
; j
++)
1229 std::stringstream ss
;
1230 ss
<< dt
.getName() << "_x_" << i
<< "_" << j
;
1231 Expr v
= mkBoundVar(ss
.str(), ltypes
[j
]);
1234 return getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, lvars
);
1237 const void Smt2::getSygusInvVars(FunctionType t
,
1238 std::vector
<Expr
>& vars
,
1239 std::vector
<Expr
>& primed_vars
)
1241 std::vector
<Type
> argTypes
= t
.getArgTypes();
1242 ExprManager
* em
= getExprManager();
1243 for (const Type
& ti
: argTypes
)
1245 vars
.push_back(em
->mkBoundVar(ti
));
1246 d_sygusVars
.push_back(vars
.back());
1247 std::stringstream ss
;
1248 ss
<< vars
.back() << "'";
1249 primed_vars
.push_back(em
->mkBoundVar(ss
.str(), ti
));
1250 d_sygusVars
.push_back(primed_vars
.back());
1251 #ifdef CVC4_ASSERTIONS
1252 bool find_new_declared_var
= false;
1253 for (const Expr
& e
: d_sygusVarPrimed
)
1255 if (e
.getType() == ti
)
1257 d_sygusVarPrimed
.erase(
1258 std::find(d_sygusVarPrimed
.begin(), d_sygusVarPrimed
.end(), e
));
1259 find_new_declared_var
= true;
1263 if (!find_new_declared_var
)
1266 ss
<< "warning: decleared primed variables do not match invariant's "
1274 const void Smt2::addSygusFunSymbol( Type t
, Expr synth_fun
){
1275 // When constructing the synthesis conjecture, we quantify on the
1276 // (higher-order) bound variable synth_fun.
1277 d_sygusFunSymbols
.push_back(synth_fun
);
1279 // Variable "sfproxy" carries the type, which may be a SyGuS datatype
1280 // that corresponds to syntactic restrictions.
1281 Expr sym
= mkBoundVar("sfproxy", t
);
1282 std::vector
< Expr
> attr_value
;
1283 attr_value
.push_back(sym
);
1285 new SetUserAttributeCommand("sygus-synth-grammar", synth_fun
, attr_value
);
1286 cattr
->setMuted(true);
1287 preemptCommand(cattr
);
1290 InputLanguage
Smt2::getLanguage() const
1292 ExprManager
* em
= getExprManager();
1293 return em
->getOptions().getInputLanguage();
1296 }/* CVC4::parser namespace */
1297 }/* CVC4 namespace */