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-2017 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"
19 #include "expr/type.h"
20 #include "parser/antlr_input.h"
21 #include "parser/parser.h"
22 #include "parser/smt1/smt1.h"
23 #include "parser/smt2/smt2_input.h"
24 #include "smt/command.h"
25 #include "util/bitvector.h"
29 // ANTLR defines these, which is really bad!
36 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
37 Parser(exprManager
,input
,strictMode
,parseOnly
),
39 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
40 if( !strictModeEnabled() ) {
41 addTheory(Smt2::THEORY_CORE
);
45 void Smt2::setLanguage(InputLanguage lang
) {
46 ((Smt2Input
*) getInput())->setLanguage(lang
);
49 void Smt2::addArithmeticOperators() {
50 Parser::addOperator(kind::PLUS
);
51 Parser::addOperator(kind::MINUS
);
52 Parser::addOperator(kind::UMINUS
);
53 Parser::addOperator(kind::MULT
);
54 Parser::addOperator(kind::LT
);
55 Parser::addOperator(kind::LEQ
);
56 Parser::addOperator(kind::GT
);
57 Parser::addOperator(kind::GEQ
);
59 addOperator(kind::POW
, "^");
60 addOperator(kind::EXPONENTIAL
, "exp");
61 addOperator(kind::SINE
, "sin");
62 addOperator(kind::COSINE
, "cos");
63 addOperator(kind::TANGENT
, "tan");
66 void Smt2::addBitvectorOperators() {
67 addOperator(kind::BITVECTOR_CONCAT
, "concat");
68 addOperator(kind::BITVECTOR_NOT
, "bvnot");
69 addOperator(kind::BITVECTOR_AND
, "bvand");
70 addOperator(kind::BITVECTOR_OR
, "bvor");
71 addOperator(kind::BITVECTOR_NEG
, "bvneg");
72 addOperator(kind::BITVECTOR_PLUS
, "bvadd");
73 addOperator(kind::BITVECTOR_MULT
, "bvmul");
74 addOperator(kind::BITVECTOR_UDIV
, "bvudiv");
75 addOperator(kind::BITVECTOR_UREM
, "bvurem");
76 addOperator(kind::BITVECTOR_SHL
, "bvshl");
77 addOperator(kind::BITVECTOR_LSHR
, "bvlshr");
78 addOperator(kind::BITVECTOR_ULT
, "bvult");
79 addOperator(kind::BITVECTOR_NAND
, "bvnand");
80 addOperator(kind::BITVECTOR_NOR
, "bvnor");
81 addOperator(kind::BITVECTOR_XOR
, "bvxor");
82 addOperator(kind::BITVECTOR_XNOR
, "bvxnor");
83 addOperator(kind::BITVECTOR_COMP
, "bvcomp");
84 addOperator(kind::BITVECTOR_SUB
, "bvsub");
85 addOperator(kind::BITVECTOR_SDIV
, "bvsdiv");
86 addOperator(kind::BITVECTOR_SREM
, "bvsrem");
87 addOperator(kind::BITVECTOR_SMOD
, "bvsmod");
88 addOperator(kind::BITVECTOR_ASHR
, "bvashr");
89 addOperator(kind::BITVECTOR_ULE
, "bvule");
90 addOperator(kind::BITVECTOR_UGT
, "bvugt");
91 addOperator(kind::BITVECTOR_UGE
, "bvuge");
92 addOperator(kind::BITVECTOR_SLT
, "bvslt");
93 addOperator(kind::BITVECTOR_SLE
, "bvsle");
94 addOperator(kind::BITVECTOR_SGT
, "bvsgt");
95 addOperator(kind::BITVECTOR_SGE
, "bvsge");
96 addOperator(kind::BITVECTOR_REDOR
, "bvredor");
97 addOperator(kind::BITVECTOR_REDAND
, "bvredand");
99 Parser::addOperator(kind::BITVECTOR_BITOF
);
100 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
101 Parser::addOperator(kind::BITVECTOR_REPEAT
);
102 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
103 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
104 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
105 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
107 Parser::addOperator(kind::INT_TO_BITVECTOR
);
108 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
111 void Smt2::addStringOperators() {
112 addOperator(kind::STRING_CONCAT
, "str.++");
113 addOperator(kind::STRING_LENGTH
, "str.len");
114 addOperator(kind::STRING_SUBSTR
, "str.substr" );
115 addOperator(kind::STRING_STRCTN
, "str.contains" );
116 addOperator(kind::STRING_CHARAT
, "str.at" );
117 addOperator(kind::STRING_STRIDOF
, "str.indexof" );
118 addOperator(kind::STRING_STRREPL
, "str.replace" );
119 addOperator(kind::STRING_PREFIX
, "str.prefixof" );
120 addOperator(kind::STRING_SUFFIX
, "str.suffixof" );
121 addOperator(kind::STRING_ITOS
, "int.to.str" );
122 addOperator(kind::STRING_STOI
, "str.to.int" );
123 addOperator(kind::STRING_IN_REGEXP
, "str.in.re");
124 addOperator(kind::STRING_TO_REGEXP
, "str.to.re");
125 addOperator(kind::REGEXP_CONCAT
, "re.++");
126 addOperator(kind::REGEXP_UNION
, "re.union");
127 addOperator(kind::REGEXP_INTER
, "re.inter");
128 addOperator(kind::REGEXP_STAR
, "re.*");
129 addOperator(kind::REGEXP_PLUS
, "re.+");
130 addOperator(kind::REGEXP_OPT
, "re.opt");
131 addOperator(kind::REGEXP_RANGE
, "re.range");
132 addOperator(kind::REGEXP_LOOP
, "re.loop");
135 void Smt2::addFloatingPointOperators() {
136 addOperator(kind::FLOATINGPOINT_FP
, "fp");
137 addOperator(kind::FLOATINGPOINT_EQ
, "fp.eq");
138 addOperator(kind::FLOATINGPOINT_ABS
, "fp.abs");
139 addOperator(kind::FLOATINGPOINT_NEG
, "fp.neg");
140 addOperator(kind::FLOATINGPOINT_PLUS
, "fp.add");
141 addOperator(kind::FLOATINGPOINT_SUB
, "fp.sub");
142 addOperator(kind::FLOATINGPOINT_MULT
, "fp.mul");
143 addOperator(kind::FLOATINGPOINT_DIV
, "fp.div");
144 addOperator(kind::FLOATINGPOINT_FMA
, "fp.fma");
145 addOperator(kind::FLOATINGPOINT_SQRT
, "fp.sqrt");
146 addOperator(kind::FLOATINGPOINT_REM
, "fp.rem");
147 addOperator(kind::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
148 addOperator(kind::FLOATINGPOINT_MIN
, "fp.min");
149 addOperator(kind::FLOATINGPOINT_MAX
, "fp.max");
150 addOperator(kind::FLOATINGPOINT_LEQ
, "fp.leq");
151 addOperator(kind::FLOATINGPOINT_LT
, "fp.lt");
152 addOperator(kind::FLOATINGPOINT_GEQ
, "fp.geq");
153 addOperator(kind::FLOATINGPOINT_GT
, "fp.gt");
154 addOperator(kind::FLOATINGPOINT_ISN
, "fp.isNormal");
155 addOperator(kind::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
156 addOperator(kind::FLOATINGPOINT_ISZ
, "fp.isZero");
157 addOperator(kind::FLOATINGPOINT_ISINF
, "fp.isInfinite");
158 addOperator(kind::FLOATINGPOINT_ISNAN
, "fp.isNaN");
159 addOperator(kind::FLOATINGPOINT_ISNEG
, "fp.isNegative");
160 addOperator(kind::FLOATINGPOINT_ISPOS
, "fp.isPositive");
161 addOperator(kind::FLOATINGPOINT_TO_REAL
, "fp.to_real");
163 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
164 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
165 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
166 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
167 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
168 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
169 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
172 void Smt2::addSepOperators() {
173 addOperator(kind::SEP_STAR
, "sep");
174 addOperator(kind::SEP_PTO
, "pto");
175 addOperator(kind::SEP_WAND
, "wand");
176 addOperator(kind::SEP_EMP
, "emp");
177 Parser::addOperator(kind::SEP_STAR
);
178 Parser::addOperator(kind::SEP_PTO
);
179 Parser::addOperator(kind::SEP_WAND
);
180 Parser::addOperator(kind::SEP_EMP
);
183 void Smt2::addTheory(Theory theory
) {
186 addOperator(kind::SELECT
, "select");
187 addOperator(kind::STORE
, "store");
190 case THEORY_BITVECTORS
:
191 addBitvectorOperators();
195 defineType("Bool", getExprManager()->booleanType());
196 defineVar("true", getExprManager()->mkConst(true));
197 defineVar("false", getExprManager()->mkConst(false));
198 Parser::addOperator(kind::AND
);
199 Parser::addOperator(kind::DISTINCT
);
200 Parser::addOperator(kind::EQUAL
);
201 Parser::addOperator(kind::IMPLIES
);
202 Parser::addOperator(kind::ITE
);
203 Parser::addOperator(kind::NOT
);
204 Parser::addOperator(kind::OR
);
205 Parser::addOperator(kind::XOR
);
208 case THEORY_REALS_INTS
:
209 defineType("Real", getExprManager()->realType());
210 Parser::addOperator(kind::DIVISION
);
211 addOperator(kind::TO_INTEGER
, "to_int");
212 addOperator(kind::IS_INTEGER
, "is_int");
213 addOperator(kind::TO_REAL
, "to_real");
214 // falling through on purpose, to add Ints part of Reals_Ints
216 defineType("Int", getExprManager()->integerType());
217 addArithmeticOperators();
218 addOperator(kind::INTS_DIVISION
, "div");
219 addOperator(kind::INTS_MODULUS
, "mod");
220 addOperator(kind::ABS
, "abs");
221 Parser::addOperator(kind::DIVISIBLE
);
225 defineType("Real", getExprManager()->realType());
226 addArithmeticOperators();
227 Parser::addOperator(kind::DIVISION
);
230 case THEORY_QUANTIFIERS
:
234 addOperator(kind::UNION
, "union");
235 addOperator(kind::INTERSECTION
, "intersection");
236 addOperator(kind::SETMINUS
, "setminus");
237 addOperator(kind::SUBSET
, "subset");
238 addOperator(kind::MEMBER
, "member");
239 addOperator(kind::SINGLETON
, "singleton");
240 addOperator(kind::INSERT
, "insert");
241 addOperator(kind::CARD
, "card");
242 addOperator(kind::COMPLEMENT
, "complement");
245 case THEORY_DATATYPES
:
246 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
247 Parser::addOperator(kind::APPLY_TESTER
);
248 Parser::addOperator(kind::APPLY_SELECTOR
);
249 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
253 defineType("String", getExprManager()->stringType());
254 defineType("Int", getExprManager()->integerType());
255 addStringOperators();
259 Parser::addOperator(kind::APPLY_UF
);
263 defineType("RoundingMode", getExprManager()->roundingModeType());
264 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
265 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
266 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
267 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
268 addFloatingPointOperators();
276 std::stringstream ss
;
277 ss
<< "internal error: unsupported theory " << theory
;
278 throw ParserException(ss
.str());
282 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
283 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
285 Parser::addOperator(kind
);
286 operatorKindMap
[name
] = kind
;
289 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
290 // precondition: isOperatorEnabled(name)
291 return operatorKindMap
.find(name
)->second
;
294 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
295 return operatorKindMap
.find(name
) != operatorKindMap
.end();
298 bool Smt2::isTheoryEnabled(Theory theory
) const {
301 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
302 case THEORY_BITVECTORS
:
303 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
306 case THEORY_DATATYPES
:
307 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
309 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
310 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
312 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
313 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
314 case THEORY_REALS_INTS
:
315 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
316 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
317 case THEORY_QUANTIFIERS
:
318 return d_logic
.isQuantified();
320 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
322 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
324 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
326 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
328 return d_logic
.isTheoryEnabled(theory::THEORY_SEP
);
330 std::stringstream ss
;
331 ss
<< "internal error: unsupported theory " << theory
;
332 throw ParserException(ss
.str());
336 bool Smt2::logicIsSet() {
340 Expr
Smt2::getExpressionForNameAndType(const std::string
& name
, Type t
) {
341 if(sygus() && name
[0]=='-' &&
342 name
.find_first_not_of("0123456789", 1) == std::string::npos
) {
343 //allow unary minus in sygus
344 return getExprManager()->mkConst(Rational(name
));
345 }else if(isAbstractValue(name
)) {
346 return mkAbstractValue(name
);
348 return Parser::getExpressionForNameAndType(name
, t
);
354 d_logic
= LogicInfo();
355 operatorKindMap
.clear();
356 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
357 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
358 this->Parser::reset();
360 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
361 if( !strictModeEnabled() ) {
362 addTheory(Smt2::THEORY_CORE
);
366 void Smt2::resetAssertions() {
367 this->Parser::reset();
370 void Smt2::setLogic(std::string name
) {
372 // sygus by default requires UF, datatypes, and LIA
373 if(name
== "Arrays") {
375 } else if(name
== "Reals") {
377 } else if(name
== "LIA") {
379 } else if(name
== "LRA") {
381 } else if(name
== "LIRA") {
383 } else if(name
== "BV") {
385 } else if(name
== "SLIA") {
387 } else if(name
== "SAT") {
389 } else if(name
== "ALL" || name
== "ALL_SUPPORTED") {
392 std::stringstream ss
;
393 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
394 parseError(ss
.str());
399 if(logicIsForced()) {
400 d_logic
= getForcedLogic();
405 // Core theory belongs to every logic
406 addTheory(THEORY_CORE
);
408 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
409 addTheory(THEORY_UF
);
412 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
413 if(d_logic
.areIntegersUsed()) {
414 if(d_logic
.areRealsUsed()) {
415 addTheory(THEORY_REALS_INTS
);
417 addTheory(THEORY_INTS
);
419 } else if(d_logic
.areRealsUsed()) {
420 addTheory(THEORY_REALS
);
424 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
425 addTheory(THEORY_ARRAYS
);
428 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
429 addTheory(THEORY_BITVECTORS
);
432 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
433 addTheory(THEORY_DATATYPES
);
436 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
437 addTheory(THEORY_SETS
);
440 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
441 addTheory(THEORY_STRINGS
);
444 if(d_logic
.isQuantified()) {
445 addTheory(THEORY_QUANTIFIERS
);
448 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
449 addTheory(THEORY_FP
);
452 if (d_logic
.isTheoryEnabled(theory::THEORY_SEP
)) {
453 addTheory(THEORY_SEP
);
456 }/* Smt2::setLogic() */
458 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
462 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
466 void Smt2::checkThatLogicIsSet() {
467 if( ! logicIsSet() ) {
468 if(strictModeEnabled()) {
469 parseError("set-logic must appear before this point.");
471 warning("No set-logic command was given before this point.");
472 warning("CVC4 will make all theories available.");
473 warning("Consider setting a stricter logic for (likely) better performance.");
474 warning("To suppress this warning in the future use (set-logic ALL).");
478 Command
* c
= new SetBenchmarkLogicCommand("ALL");
485 /* The include are managed in the lexer but called in the parser */
486 // Inspired by http://www.antlr3.org/api/C/interop.html
488 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
489 Debug("parser") << "Including " << filename
<< std::endl
;
490 // Create a new input stream and take advantage of built in stream stacking
491 // in C target runtime.
493 pANTLR3_INPUT_STREAM in
;
494 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
495 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
496 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
497 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
498 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
500 Debug("parser") << "Can't open " << filename
<< std::endl
;
503 // Same thing as the predefined PUSHSTREAM(in);
504 lexer
->pushCharStream(lexer
, in
);
506 //lexer->rec->state->tokenStartCharIndex = -10;
507 //lexer->emit(lexer);
509 // Note that the input stream is not closed when it EOFs, I don't bother
510 // to do it here, but it is up to you to track streams created like this
511 // and destroy them when the whole parse session is complete. Remember that you
512 // don't want to do this until all tokens have been manipulated all the way through
513 // your tree parsers etc as the token does not store the text it just refers
514 // back to the input stream and trying to get the text for it will abort if you
515 // close the input stream too early.
517 //TODO what said before
521 void Smt2::includeFile(const std::string
& filename
) {
522 // security for online version
523 if(!canIncludeFile()) {
524 parseError("include-file feature was disabled for this run.");
528 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
529 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
530 // get the name of the current stream "Does it work inside an include?"
531 const std::string inputName
= ai
->getInputStreamName();
533 // Find the directory of the current input file
535 size_t pos
= inputName
.rfind('/');
536 if(pos
!= std::string::npos
) {
537 path
= std::string(inputName
, 0, pos
+ 1);
539 path
.append(filename
);
540 if(!newInputStream(path
, lexer
)) {
541 parseError("Couldn't open include file `" + path
+ "'");
545 Expr
Smt2::mkSygusVar(const std::string
& name
, const Type
& type
, bool isPrimed
) {
546 Expr e
= mkBoundVar(name
, type
);
547 d_sygusVars
.push_back(e
);
548 d_sygusVarPrimed
[e
] = false;
550 std::stringstream ss
;
552 Expr ep
= mkBoundVar(ss
.str(), type
);
553 d_sygusVars
.push_back(ep
);
554 d_sygusVarPrimed
[ep
] = true;
559 void Smt2::mkSygusConstantsForType( const Type
& type
, std::vector
<CVC4::Expr
>& ops
) {
560 if( type
.isInteger() ){
561 ops
.push_back(getExprManager()->mkConst(Rational(0)));
562 ops
.push_back(getExprManager()->mkConst(Rational(1)));
563 }else if( type
.isBitVector() ){
564 unsigned sz
= ((BitVectorType
)type
).getSize();
565 BitVector
bval0(sz
, (unsigned int)0);
566 ops
.push_back( getExprManager()->mkConst(bval0
) );
567 BitVector
bval1(sz
, (unsigned int)1);
568 ops
.push_back( getExprManager()->mkConst(bval1
) );
569 }else if( type
.isBoolean() ){
570 ops
.push_back(getExprManager()->mkConst(true));
571 ops
.push_back(getExprManager()->mkConst(false));
576 // 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)
577 // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
578 void Smt2::processSygusGTerm( CVC4::SygusGTerm
& sgt
, int index
,
579 std::vector
< CVC4::Datatype
>& datatypes
,
580 std::vector
< CVC4::Type
>& sorts
,
581 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
582 std::vector
< std::vector
<std::string
> >& cnames
,
583 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
584 std::vector
< bool >& allow_const
,
585 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
586 std::vector
<CVC4::Expr
>& sygus_vars
,
587 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
, std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
,
588 CVC4::Type
& ret
, bool isNested
){
589 if( sgt
.d_gterm_type
==SygusGTerm::gterm_op
|| sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
590 Debug("parser-sygus") << "Add " << sgt
.d_expr
<< " to datatype " << index
<< std::endl
;
592 Kind newKind
= kind::UNDEFINED_KIND
;
593 //convert to UMINUS if one child of MINUS
594 if( sgt
.d_children
.size()==1 && sgt
.d_expr
==getExprManager()->operatorOf(kind::MINUS
) ){
595 oldKind
= kind::MINUS
;
596 newKind
= kind::UMINUS
;
599 //convert to IFF if boolean EQUAL
600 if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
601 Type ctn = sgt.d_children[0].d_type;
602 std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
603 if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
604 oldKind = kind::EQUAL;
609 if( newKind
!=kind::UNDEFINED_KIND
){
610 Expr newExpr
= getExprManager()->operatorOf(newKind
);
611 Debug("parser-sygus") << "Replace " << sgt
.d_expr
<< " with " << newExpr
<< std::endl
;
612 sgt
.d_expr
= newExpr
;
613 std::string oldName
= kind::kindToString(oldKind
);
614 std::string newName
= kind::kindToString(newKind
);
616 if((pos
= sgt
.d_name
.find(oldName
, pos
)) != std::string::npos
){
617 sgt
.d_name
.replace(pos
, oldName
.length(), newName
);
620 ops
[index
].push_back( sgt
.d_expr
);
621 cnames
[index
].push_back( sgt
.d_name
);
622 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
623 for( unsigned i
=0; i
<sgt
.d_children
.size(); i
++ ){
624 std::stringstream ss
;
625 ss
<< datatypes
[index
].getName() << "_" << ops
[index
].size() << "_arg_" << i
;
626 std::string sub_dname
= ss
.str();
627 //add datatype for child
629 pushSygusDatatypeDef( null_type
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
630 int sub_dt_index
= datatypes
.size()-1;
633 processSygusGTerm( sgt
.d_children
[i
], sub_dt_index
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
634 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
, true );
635 //process the nested gterm (either pop the last datatype, or flatten the argument)
636 Type tt
= processSygusNestedGTerm( sub_dt_index
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
637 sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
);
638 cargs
[index
].back().push_back(tt
);
640 //if let, must create operator
641 if( sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
642 processSygusLetConstructor( sgt
.d_let_vars
, index
, datatypes
, sorts
, ops
, cnames
, cargs
,
643 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
);
645 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_constant
){
646 if( sgt
.getNumChildren()!=0 ){
647 parseError("Bad syntax for Sygus Constant.");
649 std::vector
< Expr
> consts
;
650 mkSygusConstantsForType( sgt
.d_type
, consts
);
651 Debug("parser-sygus") << "...made " << consts
.size() << " constants." << std::endl
;
652 for( unsigned i
=0; i
<consts
.size(); i
++ ){
653 std::stringstream ss
;
655 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
656 ops
[index
].push_back( consts
[i
] );
657 cnames
[index
].push_back( ss
.str() );
658 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
660 allow_const
[index
] = true;
661 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_variable
|| sgt
.d_gterm_type
==SygusGTerm::gterm_input_variable
){
662 if( sgt
.getNumChildren()!=0 ){
663 parseError("Bad syntax for Sygus Variable.");
665 Debug("parser-sygus") << "...process " << sygus_vars
.size() << " variables." << std::endl
;
666 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
667 if( sygus_vars
[i
].getType()==sgt
.d_type
){
668 std::stringstream ss
;
670 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
671 ops
[index
].push_back( sygus_vars
[i
] );
672 cnames
[index
].push_back( ss
.str() );
673 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
676 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_nested_sort
){
678 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_unresolved
){
680 if( isUnresolvedType(sgt
.d_name
) ){
681 ret
= getSort(sgt
.d_name
);
683 //nested, unresolved symbol...fail
684 std::stringstream ss
;
685 ss
<< "Cannot handle nested unresolved symbol " << sgt
.d_name
<< std::endl
;
686 parseError(ss
.str());
689 //will resolve when adding constructors
690 unresolved_gterm_sym
[index
].push_back(sgt
.d_name
);
692 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_ignore
){
697 bool Smt2::pushSygusDatatypeDef( Type t
, std::string
& dname
,
698 std::vector
< CVC4::Datatype
>& datatypes
,
699 std::vector
< CVC4::Type
>& sorts
,
700 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
701 std::vector
< std::vector
<std::string
> >& cnames
,
702 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
703 std::vector
< bool >& allow_const
,
704 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
706 datatypes
.push_back(Datatype(dname
));
707 ops
.push_back(std::vector
<Expr
>());
708 cnames
.push_back(std::vector
<std::string
>());
709 cargs
.push_back(std::vector
<std::vector
<CVC4::Type
> >());
710 allow_const
.push_back(false);
711 unresolved_gterm_sym
.push_back(std::vector
< std::string
>());
715 bool Smt2::popSygusDatatypeDef( std::vector
< CVC4::Datatype
>& datatypes
,
716 std::vector
< CVC4::Type
>& sorts
,
717 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
718 std::vector
< std::vector
<std::string
> >& cnames
,
719 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
720 std::vector
< bool >& allow_const
,
721 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
723 datatypes
.pop_back();
727 allow_const
.pop_back();
728 unresolved_gterm_sym
.pop_back();
732 Type
Smt2::processSygusNestedGTerm( int sub_dt_index
, std::string
& sub_dname
, std::vector
< CVC4::Datatype
>& datatypes
,
733 std::vector
< CVC4::Type
>& sorts
,
734 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
735 std::vector
< std::vector
<std::string
> >& cnames
,
736 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
737 std::vector
< bool >& allow_const
,
738 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
739 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
740 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
, Type sub_ret
) {
742 Debug("parser-sygus") << "Argument is ";
744 //then, it is the datatype we constructed, which should have a single constructor
745 t
= mkUnresolvedType(sub_dname
);
746 Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t
<< std::endl
;
747 Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs
[sub_dt_index
].size() << std::endl
;
748 if( cargs
[sub_dt_index
].empty() ){
749 parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
751 Expr sop
= ops
[sub_dt_index
][0];
753 if( sop
.getKind() != kind::BUILTIN
&& ( sop
.isConst() || cargs
[sub_dt_index
][0].empty() ) ){
754 curr_t
= sop
.getType();
755 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
;
756 sygus_to_builtin_expr
[t
] = sop
;
757 //store that term sop has dedicated sygus type t
758 if( d_sygus_bound_var_type
.find( sop
)==d_sygus_bound_var_type
.end() ){
759 d_sygus_bound_var_type
[sop
] = t
;
762 std::vector
< Expr
> children
;
763 if( sop
.getKind() != kind::BUILTIN
){
764 children
.push_back( sop
);
766 for( unsigned i
=0; i
<cargs
[sub_dt_index
][0].size(); i
++ ){
767 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[sub_dt_index
][0][i
] );
768 if( it
==sygus_to_builtin_expr
.end() ){
769 if( sygus_to_builtin
.find( cargs
[sub_dt_index
][0][i
] )==sygus_to_builtin
.end() ){
770 std::stringstream ss
;
771 ss
<< "Missing builtin type for type " << cargs
[sub_dt_index
][0][i
] << "!" << std::endl
;
772 ss
<< "Builtin types are currently : " << std::endl
;
773 for( std::map
< CVC4::Type
, CVC4::Type
>::iterator itb
= sygus_to_builtin
.begin(); itb
!= sygus_to_builtin
.end(); ++itb
){
774 ss
<< " " << itb
->first
<< " -> " << itb
->second
<< std::endl
;
776 parseError(ss
.str());
778 Type bt
= sygus_to_builtin
[cargs
[sub_dt_index
][0][i
]];
779 Debug("parser-sygus") << ": child " << i
<< " introduce type elem for " << cargs
[sub_dt_index
][0][i
] << " " << bt
<< std::endl
;
780 std::stringstream ss
;
781 ss
<< t
<< "_x_" << i
;
782 Expr bv
= mkBoundVar(ss
.str(), bt
);
783 children
.push_back( bv
);
784 d_sygus_bound_var_type
[bv
] = cargs
[sub_dt_index
][0][i
];
786 Debug("parser-sygus") << ": child " << i
<< " existing sygus to builtin expr : " << it
->second
<< std::endl
;
787 children
.push_back( it
->second
);
790 Kind sk
= sop
.getKind() != kind::BUILTIN
? kind::APPLY
: getExprManager()->operatorToKind(sop
);
791 Debug("parser-sygus") << ": operator " << sop
<< " with " << sop
.getKind() << " " << sk
<< std::endl
;
792 Expr e
= getExprManager()->mkExpr( sk
, children
);
793 Debug("parser-sygus") << ": constructed " << e
<< ", which has type " << e
.getType() << std::endl
;
794 curr_t
= e
.getType();
795 sygus_to_builtin_expr
[t
] = e
;
797 sorts
[sub_dt_index
] = curr_t
;
798 sygus_to_builtin
[t
] = curr_t
;
800 Debug("parser-sygus") << "simple argument " << t
<< std::endl
;
801 Debug("parser-sygus") << "...removing " << datatypes
.back().getName() << std::endl
;
802 //otherwise, datatype was unecessary
803 //pop argument datatype definition
804 popSygusDatatypeDef( datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
809 void Smt2::processSygusLetConstructor( std::vector
< CVC4::Expr
>& let_vars
,
811 std::vector
< CVC4::Datatype
>& datatypes
,
812 std::vector
< CVC4::Type
>& sorts
,
813 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
814 std::vector
< std::vector
<std::string
> >& cnames
,
815 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
816 std::vector
<CVC4::Expr
>& sygus_vars
,
817 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
818 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
) {
819 std::vector
< CVC4::Expr
> let_define_args
;
821 int dindex
= cargs
[index
].size()-1;
822 Debug("parser-sygus") << "Process let constructor for datatype " << datatypes
[index
].getName() << ", #subtypes = " << cargs
[index
][dindex
].size() << std::endl
;
823 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
824 Debug("parser-sygus") << " " << i
<< " : " << cargs
[index
][dindex
][i
] << std::endl
;
825 if( i
+1==cargs
[index
][dindex
].size() ){
826 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[index
][dindex
][i
] );
827 if( it
!=sygus_to_builtin_expr
.end() ){
828 let_body
= it
->second
;
830 std::stringstream ss
;
831 ss
<< datatypes
[index
].getName() << "_body";
832 let_body
= mkBoundVar(ss
.str(), sygus_to_builtin
[cargs
[index
][dindex
][i
]]);
833 d_sygus_bound_var_type
[let_body
] = cargs
[index
][dindex
][i
];
837 Debug("parser-sygus") << std::endl
;
838 Debug("parser-sygus") << "Body is " << let_body
<< std::endl
;
839 Debug("parser-sygus") << "# let vars = " << let_vars
.size() << std::endl
;
840 for( unsigned i
=0; i
<let_vars
.size(); i
++ ){
841 Debug("parser-sygus") << " let var " << i
<< " : " << let_vars
[i
] << " " << let_vars
[i
].getType() << std::endl
;
842 let_define_args
.push_back( let_vars
[i
] );
845 Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
846 for( unsigned i=start_index; i<datatypes.size(); i++ ){
847 Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
848 if( !cargs[i].empty() ){
849 Debug("parser-sygus") << " operator 0 is " << ops[i][0] << std::endl;
850 Debug("parser-sygus") << " cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
851 for( unsigned j=0; j<cargs[i][0].size(); j++ ){
852 Type bt = sygus_to_builtin[cargs[i][0][j]];
853 Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
858 //last argument is the return, pop
859 cargs
[index
][dindex
].pop_back();
860 collectSygusLetArgs( let_body
, cargs
[index
][dindex
], let_define_args
);
862 Debug("parser-sygus") << "Make define-fun with " << cargs
[index
][dindex
].size() << " arguments..." << std::endl
;
863 std::vector
<CVC4::Type
> fsorts
;
864 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
865 Debug("parser-sygus") << " " << i
<< " : " << let_define_args
[i
] << " " << let_define_args
[i
].getType() << " " << cargs
[index
][dindex
][i
] << std::endl
;
866 fsorts
.push_back(let_define_args
[i
].getType());
869 Type ft
= getExprManager()->mkFunctionType(fsorts
, let_body
.getType());
870 std::stringstream ss
;
871 ss
<< datatypes
[index
].getName() << "_let";
872 Expr let_func
= mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
873 d_sygus_defined_funs
.push_back( let_func
);
874 preemptCommand( new DefineFunctionCommand(ss
.str(), let_func
, let_define_args
, let_body
) );
876 ops
[index
].pop_back();
877 ops
[index
].push_back( let_func
);
878 cnames
[index
].pop_back();
879 cnames
[index
].push_back(ss
.str());
881 //mark function as let constructor
882 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() );
883 d_sygus_let_func_to_body
[let_func
] = let_body
;
884 d_sygus_let_func_to_num_input_vars
[let_func
] = let_vars
.size();
888 void Smt2::collectSygusLetArgs( CVC4::Expr e
, std::vector
< CVC4::Type
>& sygusArgs
, std::vector
< CVC4::Expr
>& builtinArgs
) {
889 if( e
.getKind()==kind::BOUND_VARIABLE
){
890 if( std::find( builtinArgs
.begin(), builtinArgs
.end(), e
)==builtinArgs
.end() ){
891 builtinArgs
.push_back( e
);
892 sygusArgs
.push_back( d_sygus_bound_var_type
[e
] );
893 if( d_sygus_bound_var_type
[e
].isNull() ){
894 std::stringstream ss
;
895 ss
<< "While constructing body of let gterm, can't map " << e
<< " to sygus type." << std::endl
;
896 parseError(ss
.str());
900 for( unsigned i
=0; i
<e
.getNumChildren(); i
++ ){
901 collectSygusLetArgs( e
[i
], sygusArgs
, builtinArgs
);
906 void Smt2::setSygusStartIndex( std::string
& fun
, int startIndex
,
907 std::vector
< CVC4::Datatype
>& datatypes
,
908 std::vector
< CVC4::Type
>& sorts
,
909 std::vector
< std::vector
<CVC4::Expr
> >& ops
) {
911 CVC4::Datatype tmp_dt
= datatypes
[0];
912 Type tmp_sort
= sorts
[0];
913 std::vector
< Expr
> tmp_ops
;
914 tmp_ops
.insert( tmp_ops
.end(), ops
[0].begin(), ops
[0].end() );
915 datatypes
[0] = datatypes
[startIndex
];
916 sorts
[0] = sorts
[startIndex
];
918 ops
[0].insert( ops
[0].end(), ops
[startIndex
].begin(), ops
[startIndex
].end() );
919 datatypes
[startIndex
] = tmp_dt
;
920 sorts
[startIndex
] = tmp_sort
;
921 ops
[startIndex
].clear();
922 ops
[startIndex
].insert( ops
[startIndex
].begin(), tmp_ops
.begin(), tmp_ops
.end() );
923 }else if( startIndex
<0 ){
924 std::stringstream ss
;
925 ss
<< "warning: no symbol named Start for synth-fun " << fun
<< std::endl
;
930 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
931 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
,
932 std::vector
<std::string
>& unresolved_gterm_sym
,
933 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
) {
934 Debug("parser-sygus") << "Making sygus datatype " << dt
.getName() << std::endl
;
935 Debug("parser-sygus") << " add constructors..." << std::endl
;
936 std::vector
<std::string
> df_name
;
937 std::vector
<CVC4::Expr
> df_op
;
938 std::vector
< std::vector
<Expr
> > df_let_args
;
939 std::vector
< Expr
> df_let_body
;
940 //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin,
941 // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars,
942 // df_name, df_op, df_let_args, df_let_body );
944 Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt
.getName() << std::endl
;
945 Debug("parser-sygus") << " add constructors..." << std::endl
;
946 for( int i
=0; i
<(int)cnames
.size(); i
++ ){
948 bool is_dup_op
= false;
950 std::vector
< Expr
> let_args
;
951 unsigned let_num_input_args
= 0;
952 for( int j
=0; j
<i
; j
++ ){
953 if( ops
[i
]==ops
[j
] ){
955 if( cargs
[i
].size()==cargs
[j
].size() ){
957 for( unsigned k
=0; k
<cargs
[i
].size(); k
++ ){
958 if( cargs
[i
][k
]!=cargs
[j
][k
] ){
970 Debug("parser-sygus") << "--> Duplicate gterm : " << ops
[i
] << " at " << i
<< std::endl
;
971 ops
.erase( ops
.begin() + i
, ops
.begin() + i
+ 1 );
972 cnames
.erase( cnames
.begin() + i
, cnames
.begin() + i
+ 1 );
973 cargs
.erase( cargs
.begin() + i
, cargs
.begin() + i
+ 1 );
975 }else if( is_dup_op
){
976 Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops
[i
] << " at " << i
<< std::endl
;
977 //make into define-fun
978 std::vector
<CVC4::Type
> fsorts
;
979 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
980 Type bt
= sygus_to_builtin
[cargs
[i
][j
]];
981 std::stringstream ss
;
982 ss
<< dt
.getName() << "_x_" << i
<< "_" << j
;
983 Expr v
= mkBoundVar(ss
.str(), bt
);
984 let_args
.push_back( v
);
985 fsorts
.push_back( bt
);
986 Debug("parser-sygus") << ": var " << i
<< " " << v
<< " with type " << bt
<< " from " << cargs
[i
][j
] << std::endl
;
989 std::vector
< Expr
> children
;
990 if( ops
[i
].getKind() != kind::BUILTIN
){
991 children
.push_back( ops
[i
] );
993 children
.insert( children
.end(), let_args
.begin(), let_args
.end() );
994 Kind sk
= ops
[i
].getKind() != kind::BUILTIN
? kind::APPLY
: getExprManager()->operatorToKind(ops
[i
]);
995 Debug("parser-sygus") << ": replace " << ops
[i
] << " " << ops
[i
].getKind() << " " << sk
<< std::endl
;
996 let_body
= getExprManager()->mkExpr( sk
, children
);
997 Debug("parser-sygus") << ": new body of function is " << let_body
<< std::endl
;
999 Type ft
= getExprManager()->mkFunctionType(fsorts
, let_body
.getType());
1000 Debug("parser-sygus") << ": function type is " << ft
<< std::endl
;
1001 std::stringstream ss
;
1002 ss
<< dt
.getName() << "_df_" << i
;
1003 //replace operator and name
1004 ops
[i
] = mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
1005 cnames
[i
] = ss
.str();
1006 // indicate we need a define function
1007 df_name
.push_back( ss
.str() );
1008 df_op
.push_back( ops
[i
] );
1009 df_let_args
.push_back( let_args
);
1010 df_let_body
.push_back( let_body
);
1012 //d_sygus_defined_funs.push_back( ops[i] );
1013 //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
1014 dt
.addSygusConstructor( ops
[i
], cnames
[i
], cargs
[i
], let_body
, let_args
, 0 );
1016 std::map
< CVC4::Expr
, CVC4::Expr
>::iterator it
= d_sygus_let_func_to_body
.find( ops
[i
] );
1017 if( it
!=d_sygus_let_func_to_body
.end() ){
1018 let_body
= it
->second
;
1019 let_args
.insert( let_args
.end(), d_sygus_let_func_to_vars
[ops
[i
]].begin(), d_sygus_let_func_to_vars
[ops
[i
]].end() );
1020 let_num_input_args
= d_sygus_let_func_to_num_input_vars
[ops
[i
]];
1022 dt
.addSygusConstructor( ops
[i
], cnames
[i
], cargs
[i
], let_body
, let_args
, let_num_input_args
);
1026 Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl
;
1027 if( !unresolved_gterm_sym
.empty() ){
1028 std::vector
< Type
> types
;
1029 Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym
.size() << " symbols..." << std::endl
;
1030 for( unsigned i
=0; i
<unresolved_gterm_sym
.size(); i
++ ){
1031 Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym
[i
] << std::endl
;
1032 if( isUnresolvedType(unresolved_gterm_sym
[i
]) ){
1033 Debug("parser-sygus") << " it is an unresolved type." << std::endl
;
1034 Type t
= getSort(unresolved_gterm_sym
[i
]);
1035 if( std::find( types
.begin(), types
.end(), t
)==types
.end() ){
1036 types
.push_back( t
);
1038 Type bt
= dt
.getSygusType();
1039 Debug("parser-sygus") << ": make identity function for " << bt
<< ", argument type " << t
<< std::endl
;
1040 std::stringstream ss
;
1042 Expr let_body
= mkBoundVar(ss
.str(), bt
);
1043 std::vector
< Expr
> let_args
;
1044 let_args
.push_back( let_body
);
1045 //make the identity function
1046 Type ft
= getExprManager()->mkFunctionType(bt
, bt
);
1047 std::stringstream ssid
;
1048 ssid
<< unresolved_gterm_sym
[i
] << "_id";
1049 Expr id_op
= mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
1050 // indicate we need a define function
1051 df_name
.push_back( ssid
.str() );
1052 df_op
.push_back( id_op
);
1053 df_let_args
.push_back( let_args
);
1054 df_let_body
.push_back( let_body
);
1056 //d_sygus_defined_funs.push_back( id_op );
1057 //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
1058 //make the sygus argument list
1059 std::vector
< Type
> id_carg
;
1060 id_carg
.push_back( t
);
1061 dt
.addSygusConstructor( id_op
, unresolved_gterm_sym
[i
], id_carg
, let_body
, let_args
, 0 );
1063 ops
.push_back( id_op
);
1066 Debug("parser-sygus") << " ignore. (likely a free let variable)" << std::endl
;
1072 for( unsigned i
=0; i
<df_name
.size(); i
++ ){
1073 d_sygus_defined_funs
.push_back( df_op
[i
] );
1074 preemptCommand( new DefineFunctionCommand(df_name
[i
], df_op
[i
], df_let_args
[i
], df_let_body
[i
]) );
1078 const void Smt2::getSygusPrimedVars( std::vector
<Expr
>& vars
, bool isPrimed
) {
1079 for( unsigned i
=0; i
<d_sygusVars
.size(); i
++ ){
1080 Expr v
= d_sygusVars
[i
];
1081 std::map
< Expr
, bool >::iterator it
= d_sygusVarPrimed
.find( v
);
1082 if( it
!=d_sygusVarPrimed
.end() ){
1083 if( it
->second
==isPrimed
){
1084 vars
.push_back( v
);
1087 //should never happen
1092 const void Smt2::addSygusFunSymbol( Type t
, Expr synth_fun
){
1093 //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute
1094 Expr sym
= mkBoundVar("sfproxy", t
);
1095 d_sygusFunSymbols
.push_back(sym
);
1097 std::vector
< Expr
> attr_value
;
1098 attr_value
.push_back( synth_fun
);
1099 Command
* cattr
= new SetUserAttributeCommand("sygus-synth-fun", sym
, attr_value
);
1100 cattr
->setMuted(true);
1101 preemptCommand(cattr
);
1104 }/* CVC4::parser namespace */
1105 }/* CVC4 namespace */