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 addOperator(kind::BITVECTOR_CONCAT
, "concat");
54 addOperator(kind::BITVECTOR_NOT
, "bvnot");
55 addOperator(kind::BITVECTOR_AND
, "bvand");
56 addOperator(kind::BITVECTOR_OR
, "bvor");
57 addOperator(kind::BITVECTOR_NEG
, "bvneg");
58 addOperator(kind::BITVECTOR_PLUS
, "bvadd");
59 addOperator(kind::BITVECTOR_MULT
, "bvmul");
60 addOperator(kind::BITVECTOR_UDIV
, "bvudiv");
61 addOperator(kind::BITVECTOR_UREM
, "bvurem");
62 addOperator(kind::BITVECTOR_SHL
, "bvshl");
63 addOperator(kind::BITVECTOR_LSHR
, "bvlshr");
64 addOperator(kind::BITVECTOR_ULT
, "bvult");
65 addOperator(kind::BITVECTOR_NAND
, "bvnand");
66 addOperator(kind::BITVECTOR_NOR
, "bvnor");
67 addOperator(kind::BITVECTOR_XOR
, "bvxor");
68 addOperator(kind::BITVECTOR_XNOR
, "bvxnor");
69 addOperator(kind::BITVECTOR_COMP
, "bvcomp");
70 addOperator(kind::BITVECTOR_SUB
, "bvsub");
71 addOperator(kind::BITVECTOR_SDIV
, "bvsdiv");
72 addOperator(kind::BITVECTOR_SREM
, "bvsrem");
73 addOperator(kind::BITVECTOR_SMOD
, "bvsmod");
74 addOperator(kind::BITVECTOR_ASHR
, "bvashr");
75 addOperator(kind::BITVECTOR_ULE
, "bvule");
76 addOperator(kind::BITVECTOR_UGT
, "bvugt");
77 addOperator(kind::BITVECTOR_UGE
, "bvuge");
78 addOperator(kind::BITVECTOR_SLT
, "bvslt");
79 addOperator(kind::BITVECTOR_SLE
, "bvsle");
80 addOperator(kind::BITVECTOR_SGT
, "bvsgt");
81 addOperator(kind::BITVECTOR_SGE
, "bvsge");
83 Parser::addOperator(kind::BITVECTOR_BITOF
);
84 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
85 Parser::addOperator(kind::BITVECTOR_REPEAT
);
86 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
87 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
88 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
89 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
91 Parser::addOperator(kind::INT_TO_BITVECTOR
);
92 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
95 void Smt2::addStringOperators() {
96 Parser::addOperator(kind::STRING_CONCAT
);
97 Parser::addOperator(kind::STRING_LENGTH
);
100 void Smt2::addFloatingPointOperators() {
101 Parser::addOperator(kind::FLOATINGPOINT_FP
);
102 Parser::addOperator(kind::FLOATINGPOINT_EQ
);
103 Parser::addOperator(kind::FLOATINGPOINT_ABS
);
104 Parser::addOperator(kind::FLOATINGPOINT_NEG
);
105 Parser::addOperator(kind::FLOATINGPOINT_PLUS
);
106 Parser::addOperator(kind::FLOATINGPOINT_SUB
);
107 Parser::addOperator(kind::FLOATINGPOINT_MULT
);
108 Parser::addOperator(kind::FLOATINGPOINT_DIV
);
109 Parser::addOperator(kind::FLOATINGPOINT_FMA
);
110 Parser::addOperator(kind::FLOATINGPOINT_SQRT
);
111 Parser::addOperator(kind::FLOATINGPOINT_REM
);
112 Parser::addOperator(kind::FLOATINGPOINT_RTI
);
113 Parser::addOperator(kind::FLOATINGPOINT_MIN
);
114 Parser::addOperator(kind::FLOATINGPOINT_MAX
);
115 Parser::addOperator(kind::FLOATINGPOINT_LEQ
);
116 Parser::addOperator(kind::FLOATINGPOINT_LT
);
117 Parser::addOperator(kind::FLOATINGPOINT_GEQ
);
118 Parser::addOperator(kind::FLOATINGPOINT_GT
);
119 Parser::addOperator(kind::FLOATINGPOINT_ISN
);
120 Parser::addOperator(kind::FLOATINGPOINT_ISSN
);
121 Parser::addOperator(kind::FLOATINGPOINT_ISZ
);
122 Parser::addOperator(kind::FLOATINGPOINT_ISINF
);
123 Parser::addOperator(kind::FLOATINGPOINT_ISNAN
);
124 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
125 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
126 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
127 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
128 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
129 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
130 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
131 Parser::addOperator(kind::FLOATINGPOINT_TO_REAL
);
135 void Smt2::addTheory(Theory theory
) {
138 addOperator(kind::SELECT
, "select");
139 addOperator(kind::STORE
, "store");
142 case THEORY_BITVECTORS
:
143 addBitvectorOperators();
147 defineType("Bool", getExprManager()->booleanType());
148 defineVar("true", getExprManager()->mkConst(true));
149 defineVar("false", getExprManager()->mkConst(false));
150 Parser::addOperator(kind::AND
);
151 Parser::addOperator(kind::DISTINCT
);
152 Parser::addOperator(kind::EQUAL
);
153 Parser::addOperator(kind::IFF
);
154 Parser::addOperator(kind::IMPLIES
);
155 Parser::addOperator(kind::ITE
);
156 Parser::addOperator(kind::NOT
);
157 Parser::addOperator(kind::OR
);
158 Parser::addOperator(kind::XOR
);
161 case THEORY_REALS_INTS
:
162 defineType("Real", getExprManager()->realType());
163 Parser::addOperator(kind::DIVISION
);
164 addOperator(kind::TO_INTEGER
, "to_int");
165 addOperator(kind::IS_INTEGER
, "is_int");
166 addOperator(kind::TO_REAL
, "to_real");
167 // falling through on purpose, to add Ints part of Reals_Ints
169 defineType("Int", getExprManager()->integerType());
170 addArithmeticOperators();
171 addOperator(kind::INTS_DIVISION
, "div");
172 addOperator(kind::INTS_MODULUS
, "mod");
173 addOperator(kind::ABS
, "abs");
174 Parser::addOperator(kind::DIVISIBLE
);
178 defineType("Real", getExprManager()->realType());
179 addArithmeticOperators();
180 Parser::addOperator(kind::DIVISION
);
183 case THEORY_QUANTIFIERS
:
187 addOperator(kind::UNION
, "union");
188 addOperator(kind::INTERSECTION
, "intersection");
189 addOperator(kind::SETMINUS
, "setminus");
190 addOperator(kind::SUBSET
, "subset");
191 addOperator(kind::MEMBER
, "member");
192 addOperator(kind::SINGLETON
, "singleton");
193 addOperator(kind::INSERT
, "insert");
196 case THEORY_DATATYPES
:
197 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
198 Parser::addOperator(kind::APPLY_TESTER
);
199 Parser::addOperator(kind::APPLY_SELECTOR
);
200 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
204 defineType("String", getExprManager()->stringType());
205 addStringOperators();
209 Parser::addOperator(kind::APPLY_UF
);
213 defineType("RoundingMode", getExprManager()->roundingModeType());
214 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
215 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
216 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
217 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
218 addFloatingPointOperators();
222 std::stringstream ss
;
223 ss
<< "internal error: unsupported theory " << theory
;
224 throw ParserException(ss
.str());
228 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
229 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
231 Parser::addOperator(kind
);
232 operatorKindMap
[name
] = kind
;
235 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
236 // precondition: isOperatorEnabled(name)
237 return operatorKindMap
.find(name
)->second
;
240 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
241 return operatorKindMap
.find(name
) != operatorKindMap
.end();
244 bool Smt2::isTheoryEnabled(Theory theory
) const {
247 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
248 case THEORY_BITVECTORS
:
249 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
252 case THEORY_DATATYPES
:
253 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
255 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
256 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
258 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
259 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
260 case THEORY_REALS_INTS
:
261 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
262 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
263 case THEORY_QUANTIFIERS
:
264 return d_logic
.isQuantified();
266 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
268 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
270 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
272 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
274 std::stringstream ss
;
275 ss
<< "internal error: unsupported theory " << theory
;
276 throw ParserException(ss
.str());
280 bool Smt2::logicIsSet() {
286 d_logic
= LogicInfo();
287 operatorKindMap
.clear();
288 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
289 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
290 this->Parser::reset();
292 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
293 if( !strictModeEnabled() ) {
294 addTheory(Smt2::THEORY_CORE
);
298 void Smt2::resetAssertions() {
299 this->Parser::reset();
302 void Smt2::setLogic(std::string name
) {
304 if(name
== "Arrays") {
306 } else if(name
== "Reals") {
308 } else if(name
== "LIA") {
310 } else if(name
== "LRA") {
312 } else if(name
== "LIRA") {
314 } else if(name
== "BV") {
317 std::stringstream ss
;
318 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
319 parseError(ss
.str());
324 if(logicIsForced()) {
325 d_logic
= getForcedLogic();
330 // Core theory belongs to every logic
331 addTheory(THEORY_CORE
);
333 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
334 addTheory(THEORY_UF
);
337 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
338 if(d_logic
.areIntegersUsed()) {
339 if(d_logic
.areRealsUsed()) {
340 addTheory(THEORY_REALS_INTS
);
342 addTheory(THEORY_INTS
);
344 } else if(d_logic
.areRealsUsed()) {
345 addTheory(THEORY_REALS
);
349 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
350 addTheory(THEORY_ARRAYS
);
353 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
354 addTheory(THEORY_BITVECTORS
);
357 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
358 addTheory(THEORY_DATATYPES
);
361 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
362 addTheory(THEORY_SETS
);
365 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
366 addTheory(THEORY_STRINGS
);
369 if(d_logic
.isQuantified()) {
370 addTheory(THEORY_QUANTIFIERS
);
373 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
374 addTheory(THEORY_FP
);
377 }/* Smt2::setLogic() */
379 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
383 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
387 void Smt2::checkThatLogicIsSet() {
388 if( ! logicIsSet() ) {
389 if(strictModeEnabled()) {
390 parseError("set-logic must appear before this point.");
395 warning("No set-logic command was given before this point.");
396 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
397 warning("Consider setting a stricter logic for (likely) better performance.");
398 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
400 setLogic("ALL_SUPPORTED");
403 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
410 /* The include are managed in the lexer but called in the parser */
411 // Inspired by http://www.antlr3.org/api/C/interop.html
413 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
414 Debug("parser") << "Including " << filename
<< std::endl
;
415 // Create a new input stream and take advantage of built in stream stacking
416 // in C target runtime.
418 pANTLR3_INPUT_STREAM in
;
419 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
420 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
421 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
422 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
423 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
425 Debug("parser") << "Can't open " << filename
<< std::endl
;
428 // Same thing as the predefined PUSHSTREAM(in);
429 lexer
->pushCharStream(lexer
, in
);
431 //lexer->rec->state->tokenStartCharIndex = -10;
432 //lexer->emit(lexer);
434 // Note that the input stream is not closed when it EOFs, I don't bother
435 // to do it here, but it is up to you to track streams created like this
436 // and destroy them when the whole parse session is complete. Remember that you
437 // don't want to do this until all tokens have been manipulated all the way through
438 // your tree parsers etc as the token does not store the text it just refers
439 // back to the input stream and trying to get the text for it will abort if you
440 // close the input stream too early.
442 //TODO what said before
446 void Smt2::includeFile(const std::string
& filename
) {
447 // security for online version
448 if(!canIncludeFile()) {
449 parseError("include-file feature was disabled for this run.");
453 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
454 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
455 // get the name of the current stream "Does it work inside an include?"
456 const std::string inputName
= ai
->getInputStreamName();
458 // Find the directory of the current input file
460 size_t pos
= inputName
.rfind('/');
461 if(pos
!= std::string::npos
) {
462 path
= std::string(inputName
, 0, pos
+ 1);
464 path
.append(filename
);
465 if(!newInputStream(path
, lexer
)) {
466 parseError("Couldn't open include file `" + path
+ "'");
472 void Smt2::defineSygusFuns() {
473 // only define each one once
474 while(d_nextSygusFun
< d_sygusFuns
.size()) {
475 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
476 std::string fun
= p
.first
;
477 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
478 Expr eval
= p
.second
;
479 FunctionType evalType
= eval
.getType();
480 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
481 Type rangeType
= evalType
.getRangeType();
482 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
484 // first make the function type
485 std::vector
<Expr
> sygusVars
;
486 std::vector
<Type
> funType
;
487 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
488 funType
.push_back(argTypes
[j
]);
489 std::stringstream ss
;
490 ss
<< fun
<< "_v_" << j
;
491 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
493 Type funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
494 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
496 // copy the bound vars
498 std::vector<Expr> sygusVars;
499 //std::vector<Type> types;
500 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
501 std::stringstream ss;
502 ss << d_sygusVars[i];
503 Type type = d_sygusVars[i].getType();
504 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
505 //types.push_back(type);
507 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
510 //Type t = getExprManager()->mkFunctionType(types, rangeType);
511 //Debug("parser-sygus") << "...function type : " << t << std::endl;
513 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
514 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
515 std::vector
<Expr
> applyv
;
516 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
517 d_sygusFunSymbols
.push_back(funbv
);
518 applyv
.push_back(eval
);
519 applyv
.push_back(funbv
);
520 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
521 applyv
.push_back(sygusVars
[i
]);
523 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
524 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
525 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
532 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
533 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
) {
534 for( unsigned i
=0; i
<cnames
.size(); i
++ ){
535 std::string name
= dt
.getName() + "_" + cnames
[i
];
536 std::string
testerId("is-");
537 testerId
.append(name
);
538 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
539 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
540 CVC4::DatatypeConstructor
c(name
, testerId
, ops
[i
] );
541 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
542 std::stringstream sname
;
543 sname
<< name
<< "_" << j
;
544 c
.addArg(sname
.str(), cargs
[i
][j
]);
546 dt
.addConstructor(c
);
550 // i is index in datatypes/ops
551 // j is index is datatype
552 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
553 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
554 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
555 const DatatypeConstructor
& ctor
= dt
[j
];
556 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
557 std::vector
<Expr
> bvs
, extraArgs
;
558 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
559 std::string vname
= "v_" + ctor
[k
].getName();
560 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
562 extraArgs
.push_back(bv
);
564 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
565 Expr bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
566 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
567 std::vector
<Expr
> patv
;
568 patv
.push_back(eval
);
569 std::vector
<Expr
> applyv
;
570 applyv
.push_back(ctor
.getConstructor());
571 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
572 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
574 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
575 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
576 patv
.push_back(cpatv
);
577 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
578 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
579 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
580 std::vector
<Expr
> builtApply
;
581 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
582 std::vector
<Expr
> patvb
;
583 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
584 patvb
.push_back(extraArgs
[k
]);
585 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
586 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
588 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
591 //if( ops[i][j].getKind() == kind::BUILTIN ){
592 if( !builtApply
.empty() ){
593 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
594 builtTerm
= getExprManager()->mkExpr(kind::APPLY
, ops
[i
][j
], builtApply
);
596 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
599 builtTerm
= ops
[i
][j
];
601 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
602 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
603 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
604 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
605 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
606 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
608 //linearize multiplication if possible
609 if( builtTerm
.getKind()==kind::MULT
){
610 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
611 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
612 if( at
.isDatatype() ){
613 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
614 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
615 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
616 if( itd
!=datatypeTypes
.end() ){
617 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
618 unsigned index
= itd
-datatypeTypes
.begin();
619 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
621 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
622 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
623 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
629 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
630 const Datatype
& atdd
= atd
.getDatatype();
631 std::vector
<Expr
> assertions
;
632 std::vector
<Expr
> nbvs
;
633 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
635 nbvs
.push_back( bvl
[a
] );
638 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
639 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
640 //Make new assertion based on partially instantiating existing
641 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
642 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
643 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
644 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
646 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
647 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
648 builtApply
[k
] = ops
[index
][cc
];
649 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
650 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
651 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
652 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
653 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
654 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
655 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
656 assertions
.push_back( eassertion
);
658 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
659 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
669 }/* CVC4::parser namespace */
670 }/* CVC4 namespace */