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-2016 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"
27 // ANTLR defines these, which is really bad!
34 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
35 Parser(exprManager
,input
,strictMode
,parseOnly
),
38 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
39 if( !strictModeEnabled() ) {
40 addTheory(Smt2::THEORY_CORE
);
44 void Smt2::setLanguage(InputLanguage lang
) {
45 ((Smt2Input
*) getInput())->setLanguage(lang
);
48 void Smt2::addArithmeticOperators() {
49 Parser::addOperator(kind::PLUS
);
50 Parser::addOperator(kind::MINUS
);
51 Parser::addOperator(kind::UMINUS
);
52 Parser::addOperator(kind::MULT
);
53 Parser::addOperator(kind::LT
);
54 Parser::addOperator(kind::LEQ
);
55 Parser::addOperator(kind::GT
);
56 Parser::addOperator(kind::GEQ
);
59 void Smt2::addBitvectorOperators() {
60 addOperator(kind::BITVECTOR_CONCAT
, "concat");
61 addOperator(kind::BITVECTOR_NOT
, "bvnot");
62 addOperator(kind::BITVECTOR_AND
, "bvand");
63 addOperator(kind::BITVECTOR_OR
, "bvor");
64 addOperator(kind::BITVECTOR_NEG
, "bvneg");
65 addOperator(kind::BITVECTOR_PLUS
, "bvadd");
66 addOperator(kind::BITVECTOR_MULT
, "bvmul");
67 addOperator(kind::BITVECTOR_UDIV
, "bvudiv");
68 addOperator(kind::BITVECTOR_UREM
, "bvurem");
69 addOperator(kind::BITVECTOR_SHL
, "bvshl");
70 addOperator(kind::BITVECTOR_LSHR
, "bvlshr");
71 addOperator(kind::BITVECTOR_ULT
, "bvult");
72 addOperator(kind::BITVECTOR_NAND
, "bvnand");
73 addOperator(kind::BITVECTOR_NOR
, "bvnor");
74 addOperator(kind::BITVECTOR_XOR
, "bvxor");
75 addOperator(kind::BITVECTOR_XNOR
, "bvxnor");
76 addOperator(kind::BITVECTOR_COMP
, "bvcomp");
77 addOperator(kind::BITVECTOR_SUB
, "bvsub");
78 addOperator(kind::BITVECTOR_SDIV
, "bvsdiv");
79 addOperator(kind::BITVECTOR_SREM
, "bvsrem");
80 addOperator(kind::BITVECTOR_SMOD
, "bvsmod");
81 addOperator(kind::BITVECTOR_ASHR
, "bvashr");
82 addOperator(kind::BITVECTOR_ULE
, "bvule");
83 addOperator(kind::BITVECTOR_UGT
, "bvugt");
84 addOperator(kind::BITVECTOR_UGE
, "bvuge");
85 addOperator(kind::BITVECTOR_SLT
, "bvslt");
86 addOperator(kind::BITVECTOR_SLE
, "bvsle");
87 addOperator(kind::BITVECTOR_SGT
, "bvsgt");
88 addOperator(kind::BITVECTOR_SGE
, "bvsge");
89 addOperator(kind::BITVECTOR_REDOR
, "bvredor");
90 addOperator(kind::BITVECTOR_REDAND
, "bvredand");
92 Parser::addOperator(kind::BITVECTOR_BITOF
);
93 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
94 Parser::addOperator(kind::BITVECTOR_REPEAT
);
95 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
96 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
97 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
98 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
100 Parser::addOperator(kind::INT_TO_BITVECTOR
);
101 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
104 void Smt2::addStringOperators() {
105 addOperator(kind::STRING_CONCAT
, "str.++");
106 addOperator(kind::STRING_LENGTH
, "str.len");
107 addOperator(kind::STRING_SUBSTR
, "str.substr" );
108 addOperator(kind::STRING_STRCTN
, "str.contains" );
109 addOperator(kind::STRING_CHARAT
, "str.at" );
110 addOperator(kind::STRING_STRIDOF
, "str.indexof" );
111 addOperator(kind::STRING_STRREPL
, "str.replace" );
112 addOperator(kind::STRING_PREFIX
, "str.prefixof" );
113 addOperator(kind::STRING_SUFFIX
, "str.suffixof" );
114 addOperator(kind::STRING_ITOS
, "int.to.str" );
115 addOperator(kind::STRING_STOI
, "str.to.int" );
116 addOperator(kind::STRING_U16TOS
, "u16.to.str" );
117 addOperator(kind::STRING_STOU16
, "str.to.u16" );
118 addOperator(kind::STRING_U32TOS
, "u32.to.str" );
119 addOperator(kind::STRING_STOU32
, "str.to.u32" );
120 addOperator(kind::STRING_IN_REGEXP
, "str.in.re");
121 addOperator(kind::STRING_TO_REGEXP
, "str.to.re");
122 addOperator(kind::REGEXP_CONCAT
, "re.++");
123 addOperator(kind::REGEXP_UNION
, "re.union");
124 addOperator(kind::REGEXP_INTER
, "re.inter");
125 addOperator(kind::REGEXP_STAR
, "re.*");
126 addOperator(kind::REGEXP_PLUS
, "re.+");
127 addOperator(kind::REGEXP_OPT
, "re.opt");
128 addOperator(kind::REGEXP_RANGE
, "re.range");
129 addOperator(kind::REGEXP_LOOP
, "re.loop");
132 void Smt2::addFloatingPointOperators() {
133 addOperator(kind::FLOATINGPOINT_FP
, "fp");
134 addOperator(kind::FLOATINGPOINT_EQ
, "fp.eq");
135 addOperator(kind::FLOATINGPOINT_ABS
, "fp.abs");
136 addOperator(kind::FLOATINGPOINT_NEG
, "fp.neg");
137 addOperator(kind::FLOATINGPOINT_PLUS
, "fp.add");
138 addOperator(kind::FLOATINGPOINT_SUB
, "fp.sub");
139 addOperator(kind::FLOATINGPOINT_MULT
, "fp.mul");
140 addOperator(kind::FLOATINGPOINT_DIV
, "fp.div");
141 addOperator(kind::FLOATINGPOINT_FMA
, "fp.fma");
142 addOperator(kind::FLOATINGPOINT_SQRT
, "fp.sqrt");
143 addOperator(kind::FLOATINGPOINT_REM
, "fp.rem");
144 addOperator(kind::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
145 addOperator(kind::FLOATINGPOINT_MIN
, "fp.min");
146 addOperator(kind::FLOATINGPOINT_MAX
, "fp.max");
147 addOperator(kind::FLOATINGPOINT_LEQ
, "fp.leq");
148 addOperator(kind::FLOATINGPOINT_LT
, "fp.lt");
149 addOperator(kind::FLOATINGPOINT_GEQ
, "fp.geq");
150 addOperator(kind::FLOATINGPOINT_GT
, "fp.gt");
151 addOperator(kind::FLOATINGPOINT_ISN
, "fp.isNormal");
152 addOperator(kind::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
153 addOperator(kind::FLOATINGPOINT_ISZ
, "fp.isZero");
154 addOperator(kind::FLOATINGPOINT_ISINF
, "fp.isInfinite");
155 addOperator(kind::FLOATINGPOINT_ISNAN
, "fp.isNaN");
156 addOperator(kind::FLOATINGPOINT_ISNEG
, "fp.isNegative");
157 addOperator(kind::FLOATINGPOINT_ISPOS
, "fp.isPositive");
158 addOperator(kind::FLOATINGPOINT_TO_REAL
, "fp.to_real");
160 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
161 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
162 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
163 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
164 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
165 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
166 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
169 void Smt2::addSepOperators() {
170 //addOperator(kind::SEP_NIL, "sep.nil");
171 addOperator(kind::SEP_STAR
, "sep");
172 addOperator(kind::SEP_PTO
, "pto");
173 addOperator(kind::SEP_WAND
, "wand");
174 addOperator(kind::EMP_STAR
, "emp");
175 //Parser::addOperator(kind::SEP_NIL);
176 Parser::addOperator(kind::SEP_STAR
);
177 Parser::addOperator(kind::SEP_PTO
);
178 Parser::addOperator(kind::SEP_WAND
);
179 Parser::addOperator(kind::EMP_STAR
);
182 void Smt2::addTheory(Theory theory
) {
185 addOperator(kind::SELECT
, "select");
186 addOperator(kind::STORE
, "store");
189 case THEORY_BITVECTORS
:
190 addBitvectorOperators();
194 defineType("Bool", getExprManager()->booleanType());
195 defineVar("true", getExprManager()->mkConst(true));
196 defineVar("false", getExprManager()->mkConst(false));
197 Parser::addOperator(kind::AND
);
198 Parser::addOperator(kind::DISTINCT
);
199 Parser::addOperator(kind::EQUAL
);
200 Parser::addOperator(kind::IFF
);
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");
244 case THEORY_DATATYPES
:
245 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
246 Parser::addOperator(kind::APPLY_TESTER
);
247 Parser::addOperator(kind::APPLY_SELECTOR
);
248 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
252 defineType("String", getExprManager()->stringType());
253 defineType("Int", getExprManager()->integerType());
254 addStringOperators();
258 Parser::addOperator(kind::APPLY_UF
);
262 defineType("RoundingMode", getExprManager()->roundingModeType());
263 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
264 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
265 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
266 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
267 addFloatingPointOperators();
275 std::stringstream ss
;
276 ss
<< "internal error: unsupported theory " << theory
;
277 throw ParserException(ss
.str());
281 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
282 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
284 Parser::addOperator(kind
);
285 operatorKindMap
[name
] = kind
;
288 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
289 // precondition: isOperatorEnabled(name)
290 return operatorKindMap
.find(name
)->second
;
293 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
294 return operatorKindMap
.find(name
) != operatorKindMap
.end();
297 bool Smt2::isTheoryEnabled(Theory theory
) const {
300 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
301 case THEORY_BITVECTORS
:
302 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
305 case THEORY_DATATYPES
:
306 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
308 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
309 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
311 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
312 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
313 case THEORY_REALS_INTS
:
314 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
315 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
316 case THEORY_QUANTIFIERS
:
317 return d_logic
.isQuantified();
319 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
321 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
323 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
325 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
327 return d_logic
.isTheoryEnabled(theory::THEORY_SEP
);
329 std::stringstream ss
;
330 ss
<< "internal error: unsupported theory " << theory
;
331 throw ParserException(ss
.str());
335 bool Smt2::logicIsSet() {
341 d_logic
= LogicInfo();
342 operatorKindMap
.clear();
343 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
344 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
345 this->Parser::reset();
347 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
348 if( !strictModeEnabled() ) {
349 addTheory(Smt2::THEORY_CORE
);
353 void Smt2::resetAssertions() {
354 this->Parser::reset();
357 void Smt2::setLogic(std::string name
) {
359 if(name
== "Arrays") {
361 } else if(name
== "Reals") {
363 } else if(name
== "LIA") {
365 } else if(name
== "LRA") {
367 } else if(name
== "LIRA") {
369 } else if(name
== "BV") {
371 } else if(name
== "SLIA") {
373 } else if(name
== "ALL_SUPPORTED") {
376 std::stringstream ss
;
377 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
378 parseError(ss
.str());
383 if(logicIsForced()) {
384 d_logic
= getForcedLogic();
389 // Core theory belongs to every logic
390 addTheory(THEORY_CORE
);
392 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
393 addTheory(THEORY_UF
);
396 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
397 if(d_logic
.areIntegersUsed()) {
398 if(d_logic
.areRealsUsed()) {
399 addTheory(THEORY_REALS_INTS
);
401 addTheory(THEORY_INTS
);
403 } else if(d_logic
.areRealsUsed()) {
404 addTheory(THEORY_REALS
);
408 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
409 addTheory(THEORY_ARRAYS
);
412 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
413 addTheory(THEORY_BITVECTORS
);
416 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
417 addTheory(THEORY_DATATYPES
);
420 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
421 addTheory(THEORY_SETS
);
424 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
425 addTheory(THEORY_STRINGS
);
428 if(d_logic
.isQuantified()) {
429 addTheory(THEORY_QUANTIFIERS
);
432 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
433 addTheory(THEORY_FP
);
436 if (d_logic
.isTheoryEnabled(theory::THEORY_SEP
)) {
437 addTheory(THEORY_SEP
);
440 }/* Smt2::setLogic() */
442 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
446 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
450 void Smt2::checkThatLogicIsSet() {
451 if( ! logicIsSet() ) {
452 if(strictModeEnabled()) {
453 parseError("set-logic must appear before this point.");
458 warning("No set-logic command was given before this point.");
459 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
460 warning("Consider setting a stricter logic for (likely) better performance.");
461 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
463 setLogic("ALL_SUPPORTED");
466 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
473 /* The include are managed in the lexer but called in the parser */
474 // Inspired by http://www.antlr3.org/api/C/interop.html
476 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
477 Debug("parser") << "Including " << filename
<< std::endl
;
478 // Create a new input stream and take advantage of built in stream stacking
479 // in C target runtime.
481 pANTLR3_INPUT_STREAM in
;
482 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
483 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
484 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
485 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
486 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
488 Debug("parser") << "Can't open " << filename
<< std::endl
;
491 // Same thing as the predefined PUSHSTREAM(in);
492 lexer
->pushCharStream(lexer
, in
);
494 //lexer->rec->state->tokenStartCharIndex = -10;
495 //lexer->emit(lexer);
497 // Note that the input stream is not closed when it EOFs, I don't bother
498 // to do it here, but it is up to you to track streams created like this
499 // and destroy them when the whole parse session is complete. Remember that you
500 // don't want to do this until all tokens have been manipulated all the way through
501 // your tree parsers etc as the token does not store the text it just refers
502 // back to the input stream and trying to get the text for it will abort if you
503 // close the input stream too early.
505 //TODO what said before
509 void Smt2::includeFile(const std::string
& filename
) {
510 // security for online version
511 if(!canIncludeFile()) {
512 parseError("include-file feature was disabled for this run.");
516 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
517 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
518 // get the name of the current stream "Does it work inside an include?"
519 const std::string inputName
= ai
->getInputStreamName();
521 // Find the directory of the current input file
523 size_t pos
= inputName
.rfind('/');
524 if(pos
!= std::string::npos
) {
525 path
= std::string(inputName
, 0, pos
+ 1);
527 path
.append(filename
);
528 if(!newInputStream(path
, lexer
)) {
529 parseError("Couldn't open include file `" + path
+ "'");
533 Expr
Smt2::mkSygusVar(const std::string
& name
, const Type
& type
, bool isPrimed
) {
534 Expr e
= mkBoundVar(name
, type
);
535 d_sygusVars
.push_back(e
);
536 d_sygusVarPrimed
[e
] = false;
538 std::stringstream ss
;
540 Expr ep
= mkBoundVar(ss
.str(), type
);
541 d_sygusVars
.push_back(ep
);
542 d_sygusVarPrimed
[ep
] = true;
547 void collectSygusGrammarTypesFor( Type range
, std::vector
< Type
>& types
, std::map
< Type
, std::vector
< DatatypeConstructorArg
> >& sels
){
548 if( !range
.isBoolean() ){
549 if( std::find( types
.begin(), types
.end(), range
)==types
.end() ){
550 Debug("parser-sygus") << "...will make grammar for " << range
<< std::endl
;
551 types
.push_back( range
);
552 if( range
.isDatatype() ){
553 const Datatype
& dt
= ((DatatypeType
)range
).getDatatype();
554 for( unsigned i
=0; i
<dt
.getNumConstructors(); i
++ ){
555 for( unsigned j
=0; j
<dt
[i
].getNumArgs(); j
++ ){
556 Type crange
= ((SelectorType
)dt
[i
][j
].getType()).getRangeType();
557 sels
[crange
].push_back( dt
[i
][j
] );
558 collectSygusGrammarTypesFor( crange
, types
, sels
);
566 void Smt2::mkSygusDefaultGrammar( const Type
& range
, Expr
& bvl
, const std::string
& fun
, std::vector
<CVC4::Datatype
>& datatypes
,
567 std::vector
<Type
>& sorts
, std::vector
< std::vector
<Expr
> >& ops
, std::vector
<Expr
> sygus_vars
, int& startIndex
) {
569 //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
570 // parseError("No default grammar for type.");
573 Debug("parser-sygus") << "Construct default grammar for " << fun
<< " " << range
<< std::endl
;
574 std::map
< CVC4::Type
, CVC4::Type
> sygus_to_builtin
;
576 std::vector
< Type
> types
;
577 std::map
< Type
, std::vector
< DatatypeConstructorArg
> > sels
;
578 //types for each of the variables
579 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
580 collectSygusGrammarTypesFor( sygus_vars
[i
].getType(), types
, sels
);
582 //types connected to range
583 collectSygusGrammarTypesFor( range
, types
, sels
);
585 //name of boolean sort
586 std::stringstream ssb
;
587 ssb
<< fun
<< "_Bool";
588 std::string dbname
= ssb
.str();
589 Type unres_bt
= mkUnresolvedType(ssb
.str());
591 std::vector
< Type
> unres_types
;
592 std::map
< Type
, Type
> type_to_unres
;
593 for( unsigned i
=0; i
<types
.size(); i
++ ){
594 std::stringstream ss
;
595 ss
<< fun
<< "_" << types
[i
];
596 std::string dname
= ss
.str();
597 datatypes
.push_back(Datatype(dname
));
598 ops
.push_back(std::vector
<Expr
>());
599 //make unresolved type
600 Type unres_t
= mkUnresolvedType(dname
);
601 unres_types
.push_back(unres_t
);
602 type_to_unres
[types
[i
]] = unres_t
;
603 sygus_to_builtin
[unres_t
] = types
[i
];
605 for( unsigned i
=0; i
<types
.size(); i
++ ){
606 Debug("parser-sygus") << "Make grammar for " << types
[i
] << " " << unres_types
[i
] << std::endl
;
607 std::vector
<std::string
> cnames
;
608 std::vector
<std::vector
<CVC4::Type
> > cargs
;
609 std::vector
<std::string
> unresolved_gterm_sym
;
610 Type unres_t
= unres_types
[i
];
612 for( unsigned j
=0; j
<sygus_vars
.size(); j
++ ){
613 if( sygus_vars
[j
].getType()==types
[i
] ){
614 std::stringstream ss
;
616 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
617 ops
[i
].push_back( sygus_vars
[j
] );
618 cnames
.push_back( ss
.str() );
619 cargs
.push_back( std::vector
< CVC4::Type
>() );
623 std::vector
< Expr
> consts
;
624 mkSygusConstantsForType( types
[i
], consts
);
625 for( unsigned j
=0; j
<consts
.size(); j
++ ){
626 std::stringstream ss
;
628 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
629 ops
[i
].push_back( consts
[j
] );
630 cnames
.push_back( ss
.str() );
631 cargs
.push_back( std::vector
< CVC4::Type
>() );
634 CVC4::Kind k
= kind::ITE
;
635 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
636 ops
[i
].push_back(getExprManager()->operatorOf(k
));
637 cnames
.push_back( kind::kindToString(k
) );
638 cargs
.push_back( std::vector
< CVC4::Type
>() );
639 cargs
.back().push_back(unres_bt
);
640 cargs
.back().push_back(unres_t
);
641 cargs
.back().push_back(unres_t
);
643 if( types
[i
].isInteger() ){
644 for( unsigned j
=0; j
<2; j
++ ){
645 CVC4::Kind k
= j
==0 ? kind::PLUS
: kind::MINUS
;
646 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
647 ops
[i
].push_back(getExprManager()->operatorOf(k
));
648 cnames
.push_back(kind::kindToString(k
));
649 cargs
.push_back( std::vector
< CVC4::Type
>() );
650 cargs
.back().push_back(unres_t
);
651 cargs
.back().push_back(unres_t
);
653 }else if( types
[i
].isDatatype() ){
654 Debug("parser-sygus") << "...add for constructors" << std::endl
;
655 const Datatype
& dt
= ((DatatypeType
)types
[i
]).getDatatype();
656 for( unsigned k
=0; k
<dt
.getNumConstructors(); k
++ ){
657 Debug("parser-sygus") << "...for " << dt
[k
].getName() << std::endl
;
658 ops
[i
].push_back( dt
[k
].getConstructor() );
659 cnames
.push_back( dt
[k
].getName() );
660 cargs
.push_back( std::vector
< CVC4::Type
>() );
661 for( unsigned j
=0; j
<dt
[k
].getNumArgs(); j
++ ){
662 Type crange
= ((SelectorType
)dt
[k
][j
].getType()).getRangeType();
663 //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
664 cargs
.back().push_back( type_to_unres
[crange
] );
668 std::stringstream sserr
;
669 sserr
<< "No implementation for default Sygus grammar of type " << types
[i
] << std::endl
;
670 warning(sserr
.str());
672 //add for all selectors to this type
673 if( !sels
[types
[i
]].empty() ){
674 Debug("parser-sygus") << "...add for selectors" << std::endl
;
675 for( unsigned j
=0; j
<sels
[types
[i
]].size(); j
++ ){
676 Debug("parser-sygus") << "...for " << sels
[types
[i
]][j
].getName() << std::endl
;
677 Type arg_type
= ((SelectorType
)sels
[types
[i
]][j
].getType()).getDomain();
678 ops
[i
].push_back( sels
[types
[i
]][j
].getSelector() );
679 cnames
.push_back( sels
[types
[i
]][j
].getName() );
680 cargs
.push_back( std::vector
< CVC4::Type
>() );
681 //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
682 cargs
.back().push_back( type_to_unres
[arg_type
] );
685 Debug("parser-sygus") << "...make datatype " << datatypes
.back() << std::endl
;
686 datatypes
[i
].setSygus( types
[i
], bvl
, true, true );
687 mkSygusDatatype( datatypes
[i
], ops
[i
], cnames
, cargs
, unresolved_gterm_sym
, sygus_to_builtin
);
688 sorts
.push_back( types
[i
] );
689 //set start index if applicable
690 if( types
[i
]==range
){
696 Type btype
= getExprManager()->booleanType();
697 datatypes
.push_back(Datatype(dbname
));
698 ops
.push_back(std::vector
<Expr
>());
699 std::vector
<std::string
> cnames
;
700 std::vector
<std::vector
<CVC4::Type
> > cargs
;
701 std::vector
<std::string
> unresolved_gterm_sym
;
702 Debug("parser-sygus") << "Make grammar for " << btype
<< " " << datatypes
.back() << std::endl
;
704 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
705 if( sygus_vars
[i
].getType().isBoolean() ){
706 std::stringstream ss
;
708 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
709 ops
.back().push_back( sygus_vars
[i
] );
710 cnames
.push_back( ss
.str() );
711 cargs
.push_back( std::vector
< CVC4::Type
>() );
714 //add constants if no variables and no connected types
715 if( ops
.back().empty() && types
.empty() ){
716 std::vector
< Expr
> consts
;
717 mkSygusConstantsForType( btype
, consts
);
718 for( unsigned j
=0; j
<consts
.size(); j
++ ){
719 std::stringstream ss
;
721 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
722 ops
.back().push_back( consts
[j
] );
723 cnames
.push_back( ss
.str() );
724 cargs
.push_back( std::vector
< CVC4::Type
>() );
728 for( unsigned i
=0; i
<3; i
++ ){
729 CVC4::Kind k
= i
==0 ? kind::NOT
: ( i
==1 ? kind::AND
: kind::OR
);
730 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
731 ops
.back().push_back(getExprManager()->operatorOf(k
));
732 cnames
.push_back(kind::kindToString(k
));
733 cargs
.push_back( std::vector
< CVC4::Type
>() );
735 cargs
.back().push_back(unres_bt
);
736 }else if( k
==kind::AND
|| k
==kind::OR
){
737 cargs
.back().push_back(unres_bt
);
738 cargs
.back().push_back(unres_bt
);
741 //add predicates for types
742 for( unsigned i
=0; i
<types
.size(); i
++ ){
743 Debug("parser-sygus") << "...add predicates for " << types
[i
] << std::endl
;
744 //add equality per type
745 CVC4::Kind k
= kind::EQUAL
;
746 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
747 ops
.back().push_back(getExprManager()->operatorOf(k
));
748 std::stringstream ss
;
749 ss
<< kind::kindToString(k
) << "_" << types
[i
];
750 cnames
.push_back(ss
.str());
751 cargs
.push_back( std::vector
< CVC4::Type
>() );
752 cargs
.back().push_back(unres_types
[i
]);
753 cargs
.back().push_back(unres_types
[i
]);
754 //type specific predicates
755 if( types
[i
].isInteger() ){
756 CVC4::Kind k
= kind::LEQ
;
757 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
758 ops
.back().push_back(getExprManager()->operatorOf(k
));
759 cnames
.push_back(kind::kindToString(k
));
760 cargs
.push_back( std::vector
< CVC4::Type
>() );
761 cargs
.back().push_back(unres_types
[i
]);
762 cargs
.back().push_back(unres_types
[i
]);
763 }else if( types
[i
].isDatatype() ){
765 Debug("parser-sygus") << "...add for testers" << std::endl
;
766 const Datatype
& dt
= ((DatatypeType
)types
[i
]).getDatatype();
767 for( unsigned k
=0; k
<dt
.getNumConstructors(); k
++ ){
768 Debug("parser-sygus") << "...for " << dt
[k
].getTesterName() << std::endl
;
769 ops
.back().push_back(dt
[k
].getTester());
770 cnames
.push_back(dt
[k
].getTesterName());
771 cargs
.push_back( std::vector
< CVC4::Type
>() );
772 cargs
.back().push_back(unres_types
[i
]);
777 startIndex
= sorts
.size();
779 Debug("parser-sygus") << "...make datatype " << datatypes
.back() << std::endl
;
780 datatypes
.back().setSygus( btype
, bvl
, true, true );
781 mkSygusDatatype( datatypes
.back(), ops
.back(), cnames
, cargs
, unresolved_gterm_sym
, sygus_to_builtin
);
782 sorts
.push_back( btype
);
784 Debug("parser-sygus") << "...finished make default grammar for " << fun
<< " " << range
<< std::endl
;
787 void Smt2::mkSygusConstantsForType( const Type
& type
, std::vector
<CVC4::Expr
>& ops
) {
788 if( type
.isInteger() ){
789 ops
.push_back(getExprManager()->mkConst(Rational(0)));
790 ops
.push_back(getExprManager()->mkConst(Rational(1)));
791 }else if( type
.isBitVector() ){
792 unsigned sz
= ((BitVectorType
)type
).getSize();
793 BitVector
bval0(sz
, (unsigned int)0);
794 ops
.push_back( getExprManager()->mkConst(bval0
) );
795 BitVector
bval1(sz
, (unsigned int)1);
796 ops
.push_back( getExprManager()->mkConst(bval1
) );
797 }else if( type
.isBoolean() ){
798 ops
.push_back(getExprManager()->mkConst(true));
799 ops
.push_back(getExprManager()->mkConst(false));
804 // 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)
805 // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
806 void Smt2::processSygusGTerm( CVC4::SygusGTerm
& sgt
, int index
,
807 std::vector
< CVC4::Datatype
>& datatypes
,
808 std::vector
< CVC4::Type
>& sorts
,
809 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
810 std::vector
< std::vector
<std::string
> >& cnames
,
811 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
812 std::vector
< bool >& allow_const
,
813 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
814 std::vector
<CVC4::Expr
>& sygus_vars
,
815 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
, std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
,
816 CVC4::Type
& ret
, bool isNested
){
817 if( sgt
.d_gterm_type
==SygusGTerm::gterm_op
|| sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
818 Debug("parser-sygus") << "Add " << sgt
.d_expr
<< " to datatype " << index
<< std::endl
;
820 Kind newKind
= kind::UNDEFINED_KIND
;
821 //convert to UMINUS if one child of MINUS
822 if( sgt
.d_children
.size()==1 && sgt
.d_expr
==getExprManager()->operatorOf(kind::MINUS
) ){
823 oldKind
= kind::MINUS
;
824 newKind
= kind::UMINUS
;
826 //convert to IFF if boolean EQUAL
827 if( sgt
.d_expr
==getExprManager()->operatorOf(kind::EQUAL
) ){
828 Type ctn
= sgt
.d_children
[0].d_type
;
829 std::map
< CVC4::Type
, CVC4::Type
>::iterator it
= sygus_to_builtin
.find( ctn
);
830 if( it
!= sygus_to_builtin
.end() && it
->second
.isBoolean() ){
831 oldKind
= kind::EQUAL
;
835 if( newKind
!=kind::UNDEFINED_KIND
){
836 Expr newExpr
= getExprManager()->operatorOf(newKind
);
837 Debug("parser-sygus") << "Replace " << sgt
.d_expr
<< " with " << newExpr
<< std::endl
;
838 sgt
.d_expr
= newExpr
;
839 std::string oldName
= kind::kindToString(oldKind
);
840 std::string newName
= kind::kindToString(newKind
);
842 if((pos
= sgt
.d_name
.find(oldName
, pos
)) != std::string::npos
){
843 sgt
.d_name
.replace(pos
, oldName
.length(), newName
);
846 ops
[index
].push_back( sgt
.d_expr
);
847 cnames
[index
].push_back( sgt
.d_name
);
848 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
849 for( unsigned i
=0; i
<sgt
.d_children
.size(); i
++ ){
850 std::stringstream ss
;
851 ss
<< datatypes
[index
].getName() << "_" << ops
[index
].size() << "_arg_" << i
;
852 std::string sub_dname
= ss
.str();
853 //add datatype for child
855 pushSygusDatatypeDef( null_type
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
856 int sub_dt_index
= datatypes
.size()-1;
859 processSygusGTerm( sgt
.d_children
[i
], sub_dt_index
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
860 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
, true );
861 //process the nested gterm (either pop the last datatype, or flatten the argument)
862 Type tt
= processSygusNestedGTerm( sub_dt_index
, sub_dname
, datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
,
863 sygus_to_builtin
, sygus_to_builtin_expr
, sub_ret
);
864 cargs
[index
].back().push_back(tt
);
866 //if let, must create operator
867 if( sgt
.d_gterm_type
==SygusGTerm::gterm_let
){
868 processSygusLetConstructor( sgt
.d_let_vars
, index
, datatypes
, sorts
, ops
, cnames
, cargs
,
869 sygus_vars
, sygus_to_builtin
, sygus_to_builtin_expr
);
871 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_constant
){
872 if( sgt
.getNumChildren()!=0 ){
873 parseError("Bad syntax for Sygus Constant.");
875 std::vector
< Expr
> consts
;
876 mkSygusConstantsForType( sgt
.d_type
, consts
);
877 Debug("parser-sygus") << "...made " << consts
.size() << " constants." << std::endl
;
878 for( unsigned i
=0; i
<consts
.size(); i
++ ){
879 std::stringstream ss
;
881 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
882 ops
[index
].push_back( consts
[i
] );
883 cnames
[index
].push_back( ss
.str() );
884 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
886 allow_const
[index
] = true;
887 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_variable
|| sgt
.d_gterm_type
==SygusGTerm::gterm_input_variable
){
888 if( sgt
.getNumChildren()!=0 ){
889 parseError("Bad syntax for Sygus Variable.");
891 Debug("parser-sygus") << "...process " << sygus_vars
.size() << " variables." << std::endl
;
892 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
893 if( sygus_vars
[i
].getType()==sgt
.d_type
){
894 std::stringstream ss
;
896 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
897 ops
[index
].push_back( sygus_vars
[i
] );
898 cnames
[index
].push_back( ss
.str() );
899 cargs
[index
].push_back( std::vector
< CVC4::Type
>() );
902 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_nested_sort
){
904 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_unresolved
){
906 if( isUnresolvedType(sgt
.d_name
) ){
907 ret
= getSort(sgt
.d_name
);
909 //nested, unresolved symbol...fail
910 std::stringstream ss
;
911 ss
<< "Cannot handle nested unresolved symbol " << sgt
.d_name
<< std::endl
;
912 parseError(ss
.str());
915 //will resolve when adding constructors
916 unresolved_gterm_sym
[index
].push_back(sgt
.d_name
);
918 }else if( sgt
.d_gterm_type
==SygusGTerm::gterm_ignore
){
923 bool Smt2::pushSygusDatatypeDef( Type t
, std::string
& dname
,
924 std::vector
< CVC4::Datatype
>& datatypes
,
925 std::vector
< CVC4::Type
>& sorts
,
926 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
927 std::vector
< std::vector
<std::string
> >& cnames
,
928 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
929 std::vector
< bool >& allow_const
,
930 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
932 datatypes
.push_back(Datatype(dname
));
933 ops
.push_back(std::vector
<Expr
>());
934 cnames
.push_back(std::vector
<std::string
>());
935 cargs
.push_back(std::vector
<std::vector
<CVC4::Type
> >());
936 allow_const
.push_back(false);
937 unresolved_gterm_sym
.push_back(std::vector
< std::string
>());
941 bool Smt2::popSygusDatatypeDef( std::vector
< CVC4::Datatype
>& datatypes
,
942 std::vector
< CVC4::Type
>& sorts
,
943 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
944 std::vector
< std::vector
<std::string
> >& cnames
,
945 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
946 std::vector
< bool >& allow_const
,
947 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
){
949 datatypes
.pop_back();
953 allow_const
.pop_back();
954 unresolved_gterm_sym
.pop_back();
958 Type
Smt2::processSygusNestedGTerm( int sub_dt_index
, std::string
& sub_dname
, std::vector
< CVC4::Datatype
>& datatypes
,
959 std::vector
< CVC4::Type
>& sorts
,
960 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
961 std::vector
< std::vector
<std::string
> >& cnames
,
962 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
963 std::vector
< bool >& allow_const
,
964 std::vector
< std::vector
< std::string
> >& unresolved_gterm_sym
,
965 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
966 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
, Type sub_ret
) {
968 Debug("parser-sygus") << "Argument is ";
970 //then, it is the datatype we constructed, which should have a single constructor
971 t
= mkUnresolvedType(sub_dname
);
972 Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t
<< std::endl
;
973 Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs
[sub_dt_index
].size() << std::endl
;
974 if( cargs
[sub_dt_index
].empty() ){
975 parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
977 Expr sop
= ops
[sub_dt_index
][0];
979 if( sop
.getKind() != kind::BUILTIN
&& ( sop
.isConst() || cargs
[sub_dt_index
][0].empty() ) ){
980 curr_t
= sop
.getType();
981 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
;
982 sygus_to_builtin_expr
[t
] = sop
;
983 //store that term sop has dedicated sygus type t
984 if( d_sygus_bound_var_type
.find( sop
)==d_sygus_bound_var_type
.end() ){
985 d_sygus_bound_var_type
[sop
] = t
;
988 std::vector
< Expr
> children
;
989 if( sop
.getKind() != kind::BUILTIN
){
990 children
.push_back( sop
);
992 for( unsigned i
=0; i
<cargs
[sub_dt_index
][0].size(); i
++ ){
993 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[sub_dt_index
][0][i
] );
994 if( it
==sygus_to_builtin_expr
.end() ){
995 if( sygus_to_builtin
.find( cargs
[sub_dt_index
][0][i
] )==sygus_to_builtin
.end() ){
996 std::stringstream ss
;
997 ss
<< "Missing builtin type for type " << cargs
[sub_dt_index
][0][i
] << "!" << std::endl
;
998 ss
<< "Builtin types are currently : " << std::endl
;
999 for( std::map
< CVC4::Type
, CVC4::Type
>::iterator itb
= sygus_to_builtin
.begin(); itb
!= sygus_to_builtin
.end(); ++itb
){
1000 ss
<< " " << itb
->first
<< " -> " << itb
->second
<< std::endl
;
1002 parseError(ss
.str());
1004 Type bt
= sygus_to_builtin
[cargs
[sub_dt_index
][0][i
]];
1005 Debug("parser-sygus") << ": child " << i
<< " introduce type elem for " << cargs
[sub_dt_index
][0][i
] << " " << bt
<< std::endl
;
1006 std::stringstream ss
;
1007 ss
<< t
<< "_x_" << i
;
1008 Expr bv
= mkBoundVar(ss
.str(), bt
);
1009 children
.push_back( bv
);
1010 d_sygus_bound_var_type
[bv
] = cargs
[sub_dt_index
][0][i
];
1012 Debug("parser-sygus") << ": child " << i
<< " existing sygus to builtin expr : " << it
->second
<< std::endl
;
1013 children
.push_back( it
->second
);
1016 Kind sk
= sop
.getKind() != kind::BUILTIN
? kind::APPLY
: getExprManager()->operatorToKind(sop
);
1017 Debug("parser-sygus") << ": operator " << sop
<< " with " << sop
.getKind() << " " << sk
<< std::endl
;
1018 Expr e
= getExprManager()->mkExpr( sk
, children
);
1019 Debug("parser-sygus") << ": constructed " << e
<< ", which has type " << e
.getType() << std::endl
;
1020 curr_t
= e
.getType();
1021 sygus_to_builtin_expr
[t
] = e
;
1023 sorts
[sub_dt_index
] = curr_t
;
1024 sygus_to_builtin
[t
] = curr_t
;
1026 Debug("parser-sygus") << "simple argument " << t
<< std::endl
;
1027 Debug("parser-sygus") << "...removing " << datatypes
.back().getName() << std::endl
;
1028 //otherwise, datatype was unecessary
1029 //pop argument datatype definition
1030 popSygusDatatypeDef( datatypes
, sorts
, ops
, cnames
, cargs
, allow_const
, unresolved_gterm_sym
);
1035 void Smt2::processSygusLetConstructor( std::vector
< CVC4::Expr
>& let_vars
,
1037 std::vector
< CVC4::Datatype
>& datatypes
,
1038 std::vector
< CVC4::Type
>& sorts
,
1039 std::vector
< std::vector
<CVC4::Expr
> >& ops
,
1040 std::vector
< std::vector
<std::string
> >& cnames
,
1041 std::vector
< std::vector
< std::vector
< CVC4::Type
> > >& cargs
,
1042 std::vector
<CVC4::Expr
>& sygus_vars
,
1043 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
,
1044 std::map
< CVC4::Type
, CVC4::Expr
>& sygus_to_builtin_expr
) {
1045 std::vector
< CVC4::Expr
> let_define_args
;
1047 int dindex
= cargs
[index
].size()-1;
1048 Debug("parser-sygus") << "Process let constructor for datatype " << datatypes
[index
].getName() << ", #subtypes = " << cargs
[index
][dindex
].size() << std::endl
;
1049 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
1050 Debug("parser-sygus") << " " << i
<< " : " << cargs
[index
][dindex
][i
] << std::endl
;
1051 if( i
+1==cargs
[index
][dindex
].size() ){
1052 std::map
< CVC4::Type
, CVC4::Expr
>::iterator it
= sygus_to_builtin_expr
.find( cargs
[index
][dindex
][i
] );
1053 if( it
!=sygus_to_builtin_expr
.end() ){
1054 let_body
= it
->second
;
1056 std::stringstream ss
;
1057 ss
<< datatypes
[index
].getName() << "_body";
1058 let_body
= mkBoundVar(ss
.str(), sygus_to_builtin
[cargs
[index
][dindex
][i
]]);
1059 d_sygus_bound_var_type
[let_body
] = cargs
[index
][dindex
][i
];
1063 Debug("parser-sygus") << std::endl
;
1064 Debug("parser-sygus") << "Body is " << let_body
<< std::endl
;
1065 Debug("parser-sygus") << "# let vars = " << let_vars
.size() << std::endl
;
1066 for( unsigned i
=0; i
<let_vars
.size(); i
++ ){
1067 Debug("parser-sygus") << " let var " << i
<< " : " << let_vars
[i
] << " " << let_vars
[i
].getType() << std::endl
;
1068 let_define_args
.push_back( let_vars
[i
] );
1071 Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
1072 for( unsigned i=start_index; i<datatypes.size(); i++ ){
1073 Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
1074 if( !cargs[i].empty() ){
1075 Debug("parser-sygus") << " operator 0 is " << ops[i][0] << std::endl;
1076 Debug("parser-sygus") << " cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
1077 for( unsigned j=0; j<cargs[i][0].size(); j++ ){
1078 Type bt = sygus_to_builtin[cargs[i][0][j]];
1079 Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
1084 //last argument is the return, pop
1085 cargs
[index
][dindex
].pop_back();
1086 collectSygusLetArgs( let_body
, cargs
[index
][dindex
], let_define_args
);
1088 Debug("parser-sygus") << "Make define-fun with " << cargs
[index
][dindex
].size() << " arguments..." << std::endl
;
1089 std::vector
<CVC4::Type
> fsorts
;
1090 for( unsigned i
=0; i
<cargs
[index
][dindex
].size(); i
++ ){
1091 Debug("parser-sygus") << " " << i
<< " : " << let_define_args
[i
] << " " << let_define_args
[i
].getType() << " " << cargs
[index
][dindex
][i
] << std::endl
;
1092 fsorts
.push_back(let_define_args
[i
].getType());
1095 Type ft
= getExprManager()->mkFunctionType(fsorts
, let_body
.getType());
1096 std::stringstream ss
;
1097 ss
<< datatypes
[index
].getName() << "_let";
1098 Expr let_func
= mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
1099 d_sygus_defined_funs
.push_back( let_func
);
1100 preemptCommand( new DefineFunctionCommand(ss
.str(), let_func
, let_define_args
, let_body
) );
1102 ops
[index
].pop_back();
1103 ops
[index
].push_back( let_func
);
1104 cnames
[index
].pop_back();
1105 cnames
[index
].push_back(ss
.str());
1107 //mark function as let constructor
1108 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() );
1109 d_sygus_let_func_to_body
[let_func
] = let_body
;
1110 d_sygus_let_func_to_num_input_vars
[let_func
] = let_vars
.size();
1114 void Smt2::collectSygusLetArgs( CVC4::Expr e
, std::vector
< CVC4::Type
>& sygusArgs
, std::vector
< CVC4::Expr
>& builtinArgs
) {
1115 if( e
.getKind()==kind::BOUND_VARIABLE
){
1116 if( std::find( builtinArgs
.begin(), builtinArgs
.end(), e
)==builtinArgs
.end() ){
1117 builtinArgs
.push_back( e
);
1118 sygusArgs
.push_back( d_sygus_bound_var_type
[e
] );
1119 if( d_sygus_bound_var_type
[e
].isNull() ){
1120 std::stringstream ss
;
1121 ss
<< "While constructing body of let gterm, can't map " << e
<< " to sygus type." << std::endl
;
1122 parseError(ss
.str());
1126 for( unsigned i
=0; i
<e
.getNumChildren(); i
++ ){
1127 collectSygusLetArgs( e
[i
], sygusArgs
, builtinArgs
);
1132 void Smt2::setSygusStartIndex( std::string
& fun
, int startIndex
,
1133 std::vector
< CVC4::Datatype
>& datatypes
,
1134 std::vector
< CVC4::Type
>& sorts
,
1135 std::vector
< std::vector
<CVC4::Expr
> >& ops
) {
1137 CVC4::Datatype tmp_dt
= datatypes
[0];
1138 Type tmp_sort
= sorts
[0];
1139 std::vector
< Expr
> tmp_ops
;
1140 tmp_ops
.insert( tmp_ops
.end(), ops
[0].begin(), ops
[0].end() );
1141 datatypes
[0] = datatypes
[startIndex
];
1142 sorts
[0] = sorts
[startIndex
];
1144 ops
[0].insert( ops
[0].end(), ops
[startIndex
].begin(), ops
[startIndex
].end() );
1145 datatypes
[startIndex
] = tmp_dt
;
1146 sorts
[startIndex
] = tmp_sort
;
1147 ops
[startIndex
].clear();
1148 ops
[startIndex
].insert( ops
[startIndex
].begin(), tmp_ops
.begin(), tmp_ops
.end() );
1149 }else if( startIndex
<0 ){
1150 std::stringstream ss
;
1151 ss
<< "warning: no symbol named Start for synth-fun " << fun
<< std::endl
;
1156 void Smt2::defineSygusFuns() {
1157 // only define each one once
1158 while(d_nextSygusFun
< d_sygusFuns
.size()) {
1159 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
1160 std::string fun
= p
.first
;
1161 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
1162 Expr eval
= p
.second
;
1163 FunctionType evalType
= eval
.getType();
1164 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
1165 Type rangeType
= evalType
.getRangeType();
1166 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
1168 // first make the function type
1169 std::vector
<Expr
> sygusVars
;
1170 std::vector
<Type
> funType
;
1171 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
1172 funType
.push_back(argTypes
[j
]);
1173 std::stringstream ss
;
1174 ss
<< fun
<< "_v_" << j
;
1175 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
1178 if( !funType
.empty() ){
1179 funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
1180 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
1182 // copy the bound vars
1184 std::vector<Expr> sygusVars;
1185 //std::vector<Type> types;
1186 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
1187 std::stringstream ss;
1188 ss << d_sygusVars[i];
1189 Type type = d_sygusVars[i].getType();
1190 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
1191 //types.push_back(type);
1193 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
1196 //Type t = getExprManager()->mkFunctionType(types, rangeType);
1197 //Debug("parser-sygus") << "...function type : " << t << std::endl;
1201 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
1202 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
1203 std::vector
<Expr
> applyv
;
1204 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
1205 d_sygusFunSymbols
.push_back(funbv
);
1206 applyv
.push_back(eval
);
1207 applyv
.push_back(funbv
);
1208 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
1209 applyv
.push_back(sygusVars
[i
]);
1211 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
1212 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
1213 Debug("parser-sygus") << "--> Define " << fun
<< " as " << lambda
<< " " << apply
<< std::endl
;
1214 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
1215 preemptCommand(cmd
);
1221 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
1222 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
,
1223 std::vector
<std::string
>& unresolved_gterm_sym
,
1224 std::map
< CVC4::Type
, CVC4::Type
>& sygus_to_builtin
) {
1225 Debug("parser-sygus") << "Making sygus datatype " << dt
.getName() << std::endl
;
1226 Debug("parser-sygus") << " add constructors..." << std::endl
;
1227 for( int i
=0; i
<(int)cnames
.size(); i
++ ){
1228 bool is_dup
= false;
1229 bool is_dup_op
= false;
1231 std::vector
< Expr
> let_args
;
1232 unsigned let_num_input_args
= 0;
1233 for( int j
=0; j
<i
; j
++ ){
1234 if( ops
[i
]==ops
[j
] ){
1236 if( cargs
[i
].size()==cargs
[j
].size() ){
1238 for( unsigned k
=0; k
<cargs
[i
].size(); k
++ ){
1239 if( cargs
[i
][k
]!=cargs
[j
][k
] ){
1251 Debug("parser-sygus") << "--> Duplicate gterm : " << ops
[i
] << " at " << i
<< std::endl
;
1252 ops
.erase( ops
.begin() + i
, ops
.begin() + i
+ 1 );
1253 cnames
.erase( cnames
.begin() + i
, cnames
.begin() + i
+ 1 );
1254 cargs
.erase( cargs
.begin() + i
, cargs
.begin() + i
+ 1 );
1256 }else if( is_dup_op
){
1257 Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops
[i
] << " at " << i
<< std::endl
;
1258 //make into define-fun
1259 std::vector
<CVC4::Type
> fsorts
;
1260 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
1261 Type bt
= sygus_to_builtin
[cargs
[i
][j
]];
1262 std::stringstream ss
;
1263 ss
<< dt
.getName() << "_x_" << i
<< "_" << j
;
1264 Expr v
= mkBoundVar(ss
.str(), bt
);
1265 let_args
.push_back( v
);
1266 fsorts
.push_back( bt
);
1267 Debug("parser-sygus") << ": var " << i
<< " " << v
<< " with type " << bt
<< " from " << cargs
[i
][j
] << std::endl
;
1270 std::vector
< Expr
> children
;
1271 if( ops
[i
].getKind() != kind::BUILTIN
){
1272 children
.push_back( ops
[i
] );
1274 children
.insert( children
.end(), let_args
.begin(), let_args
.end() );
1275 Kind sk
= ops
[i
].getKind() != kind::BUILTIN
? kind::APPLY
: getExprManager()->operatorToKind(ops
[i
]);
1276 Debug("parser-sygus") << ": replace " << ops
[i
] << " " << ops
[i
].getKind() << " " << sk
<< std::endl
;
1277 let_body
= getExprManager()->mkExpr( sk
, children
);
1278 Debug("parser-sygus") << ": new body of function is " << let_body
<< std::endl
;
1280 Type ft
= getExprManager()->mkFunctionType(fsorts
, let_body
.getType());
1281 Debug("parser-sygus") << ": function type is " << ft
<< std::endl
;
1282 std::stringstream ss
;
1283 ss
<< dt
.getName() << "_df_" << i
;
1284 //replace operator and name
1285 ops
[i
] = mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
1286 cnames
[i
] = ss
.str();
1287 d_sygus_defined_funs
.push_back( ops
[i
] );
1288 preemptCommand( new DefineFunctionCommand(ss
.str(), ops
[i
], let_args
, let_body
) );
1289 addSygusDatatypeConstructor( dt
, ops
[i
], cnames
[i
], cargs
[i
], let_body
, let_args
, 0 );
1291 std::map
< CVC4::Expr
, CVC4::Expr
>::iterator it
= d_sygus_let_func_to_body
.find( ops
[i
] );
1292 if( it
!=d_sygus_let_func_to_body
.end() ){
1293 let_body
= it
->second
;
1294 let_args
.insert( let_args
.end(), d_sygus_let_func_to_vars
[ops
[i
]].begin(), d_sygus_let_func_to_vars
[ops
[i
]].end() );
1295 let_num_input_args
= d_sygus_let_func_to_num_input_vars
[ops
[i
]];
1297 addSygusDatatypeConstructor( dt
, ops
[i
], cnames
[i
], cargs
[i
], let_body
, let_args
, let_num_input_args
);
1300 Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl
;
1301 if( !unresolved_gterm_sym
.empty() ){
1302 std::vector
< Type
> types
;
1303 Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym
.size() << " symbols..." << std::endl
;
1304 for( unsigned i
=0; i
<unresolved_gterm_sym
.size(); i
++ ){
1305 Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym
[i
] << std::endl
;
1306 if( isUnresolvedType(unresolved_gterm_sym
[i
]) ){
1307 Debug("parser-sygus") << " it is an unresolved type." << std::endl
;
1308 Type t
= getSort(unresolved_gterm_sym
[i
]);
1309 if( std::find( types
.begin(), types
.end(), t
)==types
.end() ){
1310 types
.push_back( t
);
1312 Type bt
= dt
.getSygusType();
1313 Debug("parser-sygus") << ": make identity function for " << bt
<< ", argument type " << t
<< std::endl
;
1314 std::stringstream ss
;
1316 Expr let_body
= mkBoundVar(ss
.str(), bt
);
1317 std::vector
< Expr
> let_args
;
1318 let_args
.push_back( let_body
);
1319 //make the identity function
1320 Type ft
= getExprManager()->mkFunctionType(bt
, bt
);
1321 std::stringstream ssid
;
1322 ssid
<< unresolved_gterm_sym
[i
] << "_id";
1323 Expr id_op
= mkFunction(ss
.str(), ft
, ExprManager::VAR_FLAG_DEFINED
);
1324 d_sygus_defined_funs
.push_back( id_op
);
1325 preemptCommand( new DefineFunctionCommand(ssid
.str(), id_op
, let_args
, let_body
) );
1326 //make the sygus argument list
1327 std::vector
< Type
> id_carg
;
1328 id_carg
.push_back( t
);
1329 addSygusDatatypeConstructor( dt
, id_op
, unresolved_gterm_sym
[i
], id_carg
, let_body
, let_args
, 0 );
1331 ops
.push_back( id_op
);
1334 Debug("parser-sygus") << " ignore. (likely a free let variable)" << std::endl
;
1341 void Smt2::addSygusDatatypeConstructor( CVC4::Datatype
& dt
, CVC4::Expr op
, std::string
& cname
, std::vector
< CVC4::Type
>& cargs
,
1342 CVC4::Expr
& let_body
, std::vector
< CVC4::Expr
>& let_args
, unsigned let_num_input_args
) {
1343 Debug("parser-sygus") << "--> Add constructor " << cname
<< " to " << dt
.getName() << std::endl
;
1344 if( !let_body
.isNull() ){
1345 Debug("parser-sygus") << " let body = " << let_body
<< ", args = " << let_args
.size() << "," << let_num_input_args
<< std::endl
;
1346 //TODO : remove arguments not occurring in body
1347 //if this is a self identity function, ignore
1348 if( let_args
.size()==0 && let_args
[0]==let_body
){
1349 Debug("parser-sygus") << " identity function " << cargs
[0] << " to " << dt
.getName() << std::endl
;
1353 std::string name
= dt
.getName() + "_" + cname
;
1354 std::string
testerId("is-");
1355 testerId
.append(name
);
1356 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
1357 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
1358 CVC4::DatatypeConstructor
c(name
, testerId
);
1359 c
.setSygus( op
, let_body
, let_args
, let_num_input_args
);
1360 for( unsigned j
=0; j
<cargs
.size(); j
++ ){
1361 Debug("parser-sygus-debug") << " arg " << j
<< " : " << cargs
[j
] << std::endl
;
1362 std::stringstream sname
;
1363 sname
<< name
<< "_" << j
;
1364 c
.addArg(sname
.str(), cargs
[j
]);
1366 dt
.addConstructor(c
);
1370 // i is index in datatypes/ops
1371 // j is index is datatype
1372 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
1373 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
1374 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
1375 const DatatypeConstructor
& ctor
= dt
[j
];
1376 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
1377 std::vector
<Expr
> bvs
, extraArgs
;
1378 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
1379 std::string vname
= "v_" + ctor
[k
].getName();
1380 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
1382 extraArgs
.push_back(bv
);
1384 if( !terms
[0].isNull() ){
1385 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
1389 bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
1391 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
1392 std::vector
<Expr
> patv
;
1393 patv
.push_back(eval
);
1394 std::vector
<Expr
> applyv
;
1395 applyv
.push_back(ctor
.getConstructor());
1396 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
1397 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
1399 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
1400 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
1401 patv
.push_back(cpatv
);
1402 if( !terms
[0].isNull() ){
1403 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
1405 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
1406 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
1407 std::vector
<Expr
> builtApply
;
1408 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
1409 std::vector
<Expr
> patvb
;
1410 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
1411 patvb
.push_back(extraArgs
[k
]);
1412 if( !terms
[0].isNull() ){
1413 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
1415 Debug("parser-sygus-debug") << "...add to built apply " << evals
[DatatypeType(extraArgs
[k
].getType())] << " " << extraArgs
[k
] << " " << extraArgs
[k
].getType() << std::endl
;
1416 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
1417 Debug("parser-sygus-debug") << "...added " << builtApply
.back() << std::endl
;
1419 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
1422 Debug("parser-sygus") << "...operator is : " << ops
[i
][j
] << ", type = " << ops
[i
][j
].getType() << ", kind = " << ops
[i
][j
].getKind() << ", is defined = " << isDefinedFunction( ops
[i
][j
] ) << std::endl
;
1423 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
1424 Kind ok
= kind::UNDEFINED_KIND
;
1425 if( isDefinedFunction( ops
[i
][j
] ) || std::find( d_sygus_defined_funs
.begin(), d_sygus_defined_funs
.end(), ops
[i
][j
] )!=d_sygus_defined_funs
.end() ){
1428 Type t
= ops
[i
][j
].getType();
1429 if( t
.isConstructor() ){
1430 ok
= kind::APPLY_CONSTRUCTOR
;
1431 }else if( t
.isSelector() ){
1432 ok
= kind::APPLY_SELECTOR
;
1433 }else if( t
.isTester() ){
1434 ok
= kind::APPLY_TESTER
;
1436 ok
= getExprManager()->operatorToKind( ops
[i
][j
] );
1439 Debug("parser-sygus") << "...processed operator kind : " << ok
<< std::endl
;
1440 if( ok
!=kind::UNDEFINED_KIND
){
1441 builtTerm
= getExprManager()->mkExpr(ok
, ops
[i
][j
], builtApply
);
1443 builtTerm
= ops
[i
][j
];
1446 if( !builtApply
.empty() ){
1447 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
1449 builtTerm
= ops
[i
][j
];
1452 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
1453 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
1454 if( !bvl
.isNull() ){
1455 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
1456 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
1457 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
1459 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
1461 //linearize multiplication if possible
1462 if( builtTerm
.getKind()==kind::MULT
){
1463 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
1464 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
1465 if( at
.isDatatype() ){
1466 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
1467 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
1468 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
1469 if( itd
!=datatypeTypes
.end() ){
1470 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
1471 unsigned index
= itd
-datatypeTypes
.begin();
1472 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
1473 bool isConst
= true;
1474 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
1475 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
1476 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
1482 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
1483 const Datatype
& atdd
= atd
.getDatatype();
1484 std::vector
<Expr
> assertions
;
1485 std::vector
<Expr
> nbvs
;
1486 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
1488 nbvs
.push_back( bvl
[a
] );
1491 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
1492 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
1493 //Make new assertion based on partially instantiating existing
1494 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
1495 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
1496 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
1497 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
1499 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
1500 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
1501 builtApply
[k
] = ops
[index
][cc
];
1502 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
1503 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
1504 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
1505 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
1506 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
1507 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
1508 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
1509 assertions
.push_back( eassertion
);
1511 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
1512 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
1521 const void Smt2::getSygusPrimedVars( std::vector
<Expr
>& vars
, bool isPrimed
) {
1522 for( unsigned i
=0; i
<d_sygusVars
.size(); i
++ ){
1523 Expr v
= d_sygusVars
[i
];
1524 std::map
< Expr
, bool >::iterator it
= d_sygusVarPrimed
.find( v
);
1525 if( it
!=d_sygusVarPrimed
.end() ){
1526 if( it
->second
==isPrimed
){
1527 vars
.push_back( v
);
1530 //should never happen
1535 }/* CVC4::parser namespace */
1536 }/* CVC4 namespace */