1 /********************* */
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Kshitij Bansal, Morgan Deters
6 ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tianyi Liang
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Definitions of SMT2 constants.
14 ** Definitions of SMT2 constants.
17 #include "expr/type.h"
18 #include "expr/command.h"
19 #include "parser/parser.h"
20 #include "parser/smt1/smt1.h"
21 #include "parser/smt2/smt2.h"
22 #include "parser/antlr_input.h"
24 // ANTLR defines these, which is really bad!
31 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
32 Parser(exprManager
,input
,strictMode
,parseOnly
),
35 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
36 if( !strictModeEnabled() ) {
37 addTheory(Smt2::THEORY_CORE
);
41 void Smt2::addArithmeticOperators() {
42 Parser::addOperator(kind::PLUS
);
43 Parser::addOperator(kind::MINUS
);
44 Parser::addOperator(kind::UMINUS
);
45 Parser::addOperator(kind::MULT
);
46 Parser::addOperator(kind::LT
);
47 Parser::addOperator(kind::LEQ
);
48 Parser::addOperator(kind::GT
);
49 Parser::addOperator(kind::GEQ
);
52 void Smt2::addBitvectorOperators() {
53 Parser::addOperator(kind::BITVECTOR_CONCAT
);
54 Parser::addOperator(kind::BITVECTOR_AND
);
55 Parser::addOperator(kind::BITVECTOR_OR
);
56 Parser::addOperator(kind::BITVECTOR_XOR
);
57 Parser::addOperator(kind::BITVECTOR_NOT
);
58 Parser::addOperator(kind::BITVECTOR_NAND
);
59 Parser::addOperator(kind::BITVECTOR_NOR
);
60 Parser::addOperator(kind::BITVECTOR_XNOR
);
61 Parser::addOperator(kind::BITVECTOR_COMP
);
62 Parser::addOperator(kind::BITVECTOR_MULT
);
63 Parser::addOperator(kind::BITVECTOR_PLUS
);
64 Parser::addOperator(kind::BITVECTOR_SUB
);
65 Parser::addOperator(kind::BITVECTOR_NEG
);
66 Parser::addOperator(kind::BITVECTOR_UDIV
);
67 Parser::addOperator(kind::BITVECTOR_UREM
);
68 Parser::addOperator(kind::BITVECTOR_SDIV
);
69 Parser::addOperator(kind::BITVECTOR_SREM
);
70 Parser::addOperator(kind::BITVECTOR_SMOD
);
71 Parser::addOperator(kind::BITVECTOR_SHL
);
72 Parser::addOperator(kind::BITVECTOR_LSHR
);
73 Parser::addOperator(kind::BITVECTOR_ASHR
);
74 Parser::addOperator(kind::BITVECTOR_ULT
);
75 Parser::addOperator(kind::BITVECTOR_ULE
);
76 Parser::addOperator(kind::BITVECTOR_UGT
);
77 Parser::addOperator(kind::BITVECTOR_UGE
);
78 Parser::addOperator(kind::BITVECTOR_SLT
);
79 Parser::addOperator(kind::BITVECTOR_SLE
);
80 Parser::addOperator(kind::BITVECTOR_SGT
);
81 Parser::addOperator(kind::BITVECTOR_SGE
);
82 Parser::addOperator(kind::BITVECTOR_BITOF
);
83 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
84 Parser::addOperator(kind::BITVECTOR_REPEAT
);
85 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
86 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
87 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
88 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
90 Parser::addOperator(kind::INT_TO_BITVECTOR
);
91 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
94 void Smt2::addStringOperators() {
95 Parser::addOperator(kind::STRING_CONCAT
);
96 Parser::addOperator(kind::STRING_LENGTH
);
99 void Smt2::addFloatingPointOperators() {
100 Parser::addOperator(kind::FLOATINGPOINT_FP
);
101 Parser::addOperator(kind::FLOATINGPOINT_EQ
);
102 Parser::addOperator(kind::FLOATINGPOINT_ABS
);
103 Parser::addOperator(kind::FLOATINGPOINT_NEG
);
104 Parser::addOperator(kind::FLOATINGPOINT_PLUS
);
105 Parser::addOperator(kind::FLOATINGPOINT_SUB
);
106 Parser::addOperator(kind::FLOATINGPOINT_MULT
);
107 Parser::addOperator(kind::FLOATINGPOINT_DIV
);
108 Parser::addOperator(kind::FLOATINGPOINT_FMA
);
109 Parser::addOperator(kind::FLOATINGPOINT_SQRT
);
110 Parser::addOperator(kind::FLOATINGPOINT_REM
);
111 Parser::addOperator(kind::FLOATINGPOINT_RTI
);
112 Parser::addOperator(kind::FLOATINGPOINT_MIN
);
113 Parser::addOperator(kind::FLOATINGPOINT_MAX
);
114 Parser::addOperator(kind::FLOATINGPOINT_LEQ
);
115 Parser::addOperator(kind::FLOATINGPOINT_LT
);
116 Parser::addOperator(kind::FLOATINGPOINT_GEQ
);
117 Parser::addOperator(kind::FLOATINGPOINT_GT
);
118 Parser::addOperator(kind::FLOATINGPOINT_ISN
);
119 Parser::addOperator(kind::FLOATINGPOINT_ISSN
);
120 Parser::addOperator(kind::FLOATINGPOINT_ISZ
);
121 Parser::addOperator(kind::FLOATINGPOINT_ISINF
);
122 Parser::addOperator(kind::FLOATINGPOINT_ISNAN
);
123 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
124 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
125 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
126 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
127 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
128 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
129 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
130 Parser::addOperator(kind::FLOATINGPOINT_TO_REAL
);
134 void Smt2::addTheory(Theory theory
) {
137 Parser::addOperator(kind::SELECT
);
138 Parser::addOperator(kind::STORE
);
141 case THEORY_BITVECTORS
:
142 addBitvectorOperators();
146 defineType("Bool", getExprManager()->booleanType());
147 defineVar("true", getExprManager()->mkConst(true));
148 defineVar("false", getExprManager()->mkConst(false));
149 Parser::addOperator(kind::AND
);
150 Parser::addOperator(kind::DISTINCT
);
151 Parser::addOperator(kind::EQUAL
);
152 Parser::addOperator(kind::IFF
);
153 Parser::addOperator(kind::IMPLIES
);
154 Parser::addOperator(kind::ITE
);
155 Parser::addOperator(kind::NOT
);
156 Parser::addOperator(kind::OR
);
157 Parser::addOperator(kind::XOR
);
160 case THEORY_REALS_INTS
:
161 defineType("Real", getExprManager()->realType());
162 Parser::addOperator(kind::DIVISION
);
163 Parser::addOperator(kind::TO_INTEGER
);
164 Parser::addOperator(kind::IS_INTEGER
);
165 Parser::addOperator(kind::TO_REAL
);
166 // falling through on purpose, to add Ints part of Reals_Ints
168 defineType("Int", getExprManager()->integerType());
169 addArithmeticOperators();
170 Parser::addOperator(kind::INTS_DIVISION
);
171 Parser::addOperator(kind::INTS_MODULUS
);
172 Parser::addOperator(kind::ABS
);
173 Parser::addOperator(kind::DIVISIBLE
);
177 defineType("Real", getExprManager()->realType());
178 addArithmeticOperators();
179 Parser::addOperator(kind::DIVISION
);
182 case THEORY_QUANTIFIERS
:
186 addOperator(kind::UNION
, "union");
187 addOperator(kind::INTERSECTION
, "intersection");
188 addOperator(kind::SETMINUS
, "setminus");
189 addOperator(kind::SUBSET
, "subset");
190 addOperator(kind::MEMBER
, "member");
191 addOperator(kind::SINGLETON
, "singleton");
192 addOperator(kind::INSERT
, "insert");
195 case THEORY_DATATYPES
:
196 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
197 Parser::addOperator(kind::APPLY_TESTER
);
198 Parser::addOperator(kind::APPLY_SELECTOR
);
199 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
203 defineType("String", getExprManager()->stringType());
204 addStringOperators();
208 Parser::addOperator(kind::APPLY_UF
);
212 defineType("RoundingMode", getExprManager()->roundingModeType());
213 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
214 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
215 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
216 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
217 addFloatingPointOperators();
221 std::stringstream ss
;
222 ss
<< "internal error: unsupported theory " << theory
;
223 throw ParserException(ss
.str());
227 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
228 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
230 Parser::addOperator(kind
);
231 operatorKindMap
[name
] = kind
;
234 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
235 // precondition: isOperatorEnabled(name)
236 return operatorKindMap
.find(name
)->second
;
239 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
240 return operatorKindMap
.find(name
) != operatorKindMap
.end();
243 bool Smt2::isTheoryEnabled(Theory theory
) const {
246 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
247 case THEORY_BITVECTORS
:
248 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
251 case THEORY_DATATYPES
:
252 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
254 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
255 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
257 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
258 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
259 case THEORY_REALS_INTS
:
260 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
261 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
262 case THEORY_QUANTIFIERS
:
263 return d_logic
.isQuantified();
265 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
267 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
269 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
271 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
273 std::stringstream ss
;
274 ss
<< "internal error: unsupported theory " << theory
;
275 throw ParserException(ss
.str());
279 bool Smt2::logicIsSet() {
285 d_logic
= LogicInfo();
286 operatorKindMap
.clear();
287 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
288 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
289 this->Parser::reset();
291 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
292 if( !strictModeEnabled() ) {
293 addTheory(Smt2::THEORY_CORE
);
297 void Smt2::resetAssertions() {
298 this->Parser::reset();
301 void Smt2::setLogic(std::string name
) {
303 if(name
== "Arrays") {
305 } else if(name
== "Reals") {
307 } else if(name
== "LIA") {
309 } else if(name
== "LRA") {
311 } else if(name
== "LIRA") {
313 } else if(name
== "BV") {
316 std::stringstream ss
;
317 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
318 parseError(ss
.str());
323 if(logicIsForced()) {
324 d_logic
= getForcedLogic();
329 // Core theory belongs to every logic
330 addTheory(THEORY_CORE
);
332 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
333 addTheory(THEORY_UF
);
336 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
337 if(d_logic
.areIntegersUsed()) {
338 if(d_logic
.areRealsUsed()) {
339 addTheory(THEORY_REALS_INTS
);
341 addTheory(THEORY_INTS
);
343 } else if(d_logic
.areRealsUsed()) {
344 addTheory(THEORY_REALS
);
348 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
349 addTheory(THEORY_ARRAYS
);
352 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
353 addTheory(THEORY_BITVECTORS
);
356 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
357 addTheory(THEORY_DATATYPES
);
360 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
361 addTheory(THEORY_SETS
);
364 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
365 addTheory(THEORY_STRINGS
);
368 if(d_logic
.isQuantified()) {
369 addTheory(THEORY_QUANTIFIERS
);
372 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
373 addTheory(THEORY_FP
);
376 }/* Smt2::setLogic() */
378 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
382 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
386 void Smt2::checkThatLogicIsSet() {
387 if( ! logicIsSet() ) {
388 if(strictModeEnabled()) {
389 parseError("set-logic must appear before this point.");
394 warning("No set-logic command was given before this point.");
395 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
396 warning("Consider setting a stricter logic for (likely) better performance.");
397 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
399 setLogic("ALL_SUPPORTED");
402 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
409 /* The include are managed in the lexer but called in the parser */
410 // Inspired by http://www.antlr3.org/api/C/interop.html
412 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
413 Debug("parser") << "Including " << filename
<< std::endl
;
414 // Create a new input stream and take advantage of built in stream stacking
415 // in C target runtime.
417 pANTLR3_INPUT_STREAM in
;
418 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
419 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
420 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
421 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
422 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
424 Debug("parser") << "Can't open " << filename
<< std::endl
;
427 // Same thing as the predefined PUSHSTREAM(in);
428 lexer
->pushCharStream(lexer
, in
);
430 //lexer->rec->state->tokenStartCharIndex = -10;
431 //lexer->emit(lexer);
433 // Note that the input stream is not closed when it EOFs, I don't bother
434 // to do it here, but it is up to you to track streams created like this
435 // and destroy them when the whole parse session is complete. Remember that you
436 // don't want to do this until all tokens have been manipulated all the way through
437 // your tree parsers etc as the token does not store the text it just refers
438 // back to the input stream and trying to get the text for it will abort if you
439 // close the input stream too early.
441 //TODO what said before
445 void Smt2::includeFile(const std::string
& filename
) {
446 // security for online version
447 if(!canIncludeFile()) {
448 parseError("include-file feature was disabled for this run.");
452 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
453 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
454 // get the name of the current stream "Does it work inside an include?"
455 const std::string inputName
= ai
->getInputStreamName();
457 // Find the directory of the current input file
459 size_t pos
= inputName
.rfind('/');
460 if(pos
!= std::string::npos
) {
461 path
= std::string(inputName
, 0, pos
+ 1);
463 path
.append(filename
);
464 if(!newInputStream(path
, lexer
)) {
465 parseError("Couldn't open include file `" + path
+ "'");
471 void Smt2::defineSygusFuns() {
472 // only define each one once
473 while(d_nextSygusFun
< d_sygusFuns
.size()) {
474 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
475 std::string fun
= p
.first
;
476 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
477 Expr eval
= p
.second
;
478 FunctionType evalType
= eval
.getType();
479 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
480 Type rangeType
= evalType
.getRangeType();
481 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
483 // first make the function type
484 std::vector
<Expr
> sygusVars
;
485 std::vector
<Type
> funType
;
486 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
487 funType
.push_back(argTypes
[j
]);
488 std::stringstream ss
;
489 ss
<< fun
<< "_v_" << j
;
490 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
493 if( !funType
.empty() ){
494 funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
495 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
497 // copy the bound vars
499 std::vector<Expr> sygusVars;
500 //std::vector<Type> types;
501 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
502 std::stringstream ss;
503 ss << d_sygusVars[i];
504 Type type = d_sygusVars[i].getType();
505 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
506 //types.push_back(type);
508 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
511 //Type t = getExprManager()->mkFunctionType(types, rangeType);
512 //Debug("parser-sygus") << "...function type : " << t << std::endl;
516 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
517 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
518 std::vector
<Expr
> applyv
;
519 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
520 d_sygusFunSymbols
.push_back(funbv
);
521 applyv
.push_back(eval
);
522 applyv
.push_back(funbv
);
523 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
524 applyv
.push_back(sygusVars
[i
]);
526 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
527 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
528 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
535 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
536 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
) {
537 for( unsigned i
=0; i
<cnames
.size(); i
++ ){
538 std::string name
= dt
.getName() + "_" + cnames
[i
];
539 std::string
testerId("is-");
540 testerId
.append(name
);
541 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
542 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
543 CVC4::DatatypeConstructor
c(name
, testerId
, ops
[i
] );
544 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
545 std::stringstream sname
;
546 sname
<< name
<< "_" << j
;
547 c
.addArg(sname
.str(), cargs
[i
][j
]);
549 dt
.addConstructor(c
);
553 // i is index in datatypes/ops
554 // j is index is datatype
555 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
556 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
557 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
558 const DatatypeConstructor
& ctor
= dt
[j
];
559 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
560 std::vector
<Expr
> bvs
, extraArgs
;
561 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
562 std::string vname
= "v_" + ctor
[k
].getName();
563 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
565 extraArgs
.push_back(bv
);
567 if( !terms
[0].isNull() ){
568 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
572 bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
574 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
575 std::vector
<Expr
> patv
;
576 patv
.push_back(eval
);
577 std::vector
<Expr
> applyv
;
578 applyv
.push_back(ctor
.getConstructor());
579 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
580 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
582 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
583 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
584 patv
.push_back(cpatv
);
585 if( !terms
[0].isNull() ){
586 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
588 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
589 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
590 std::vector
<Expr
> builtApply
;
591 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
592 std::vector
<Expr
> patvb
;
593 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
594 patvb
.push_back(extraArgs
[k
]);
595 if( !terms
[0].isNull() ){
596 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
598 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
600 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
603 //if( ops[i][j].getKind() == kind::BUILTIN ){
604 if( !builtApply
.empty() ){
605 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
606 builtTerm
= getExprManager()->mkExpr(kind::APPLY
, ops
[i
][j
], builtApply
);
608 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
611 builtTerm
= ops
[i
][j
];
613 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
614 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
616 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
617 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
618 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
620 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
622 //linearize multiplication if possible
623 if( builtTerm
.getKind()==kind::MULT
){
624 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
625 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
626 if( at
.isDatatype() ){
627 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
628 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
629 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
630 if( itd
!=datatypeTypes
.end() ){
631 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
632 unsigned index
= itd
-datatypeTypes
.begin();
633 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
635 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
636 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
637 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
643 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
644 const Datatype
& atdd
= atd
.getDatatype();
645 std::vector
<Expr
> assertions
;
646 std::vector
<Expr
> nbvs
;
647 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
649 nbvs
.push_back( bvl
[a
] );
652 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
653 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
654 //Make new assertion based on partially instantiating existing
655 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
656 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
657 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
658 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
660 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
661 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
662 builtApply
[k
] = ops
[index
][cc
];
663 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
664 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
665 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
666 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
667 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
668 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
669 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
670 assertions
.push_back( eassertion
);
672 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
673 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
683 }/* CVC4::parser namespace */
684 }/* CVC4 namespace */