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 addOperator(kind::STRING_CONCAT
, "str.++");
97 addOperator(kind::STRING_LENGTH
, "str.len");
98 addOperator(kind::STRING_SUBSTR
, "str.substr" );
99 addOperator(kind::STRING_STRCTN
, "str.contains" );
100 addOperator(kind::STRING_CHARAT
, "str.at" );
101 addOperator(kind::STRING_STRIDOF
, "str.indexof" );
102 addOperator(kind::STRING_STRREPL
, "str.replace" );
103 addOperator(kind::STRING_PREFIX
, "str.prefixof" );
104 addOperator(kind::STRING_SUFFIX
, "str.suffixof" );
105 addOperator(kind::STRING_ITOS
, "int.to.str" );
106 addOperator(kind::STRING_STOI
, "str.to.int" );
107 addOperator(kind::STRING_U16TOS
, "u16.to.str" );
108 addOperator(kind::STRING_STOU16
, "str.to.u16" );
109 addOperator(kind::STRING_U32TOS
, "u32.to.str" );
110 addOperator(kind::STRING_STOU32
, "str.to.u32" );
111 addOperator(kind::STRING_IN_REGEXP
, "str.in.re");
112 addOperator(kind::STRING_TO_REGEXP
, "str.to.re");
113 addOperator(kind::REGEXP_CONCAT
, "re.++");
114 addOperator(kind::REGEXP_UNION
, "re.union");
115 addOperator(kind::REGEXP_INTER
, "re.inter");
116 addOperator(kind::REGEXP_STAR
, "re.*");
117 addOperator(kind::REGEXP_PLUS
, "re.+");
118 addOperator(kind::REGEXP_OPT
, "re.opt");
119 addOperator(kind::REGEXP_RANGE
, "re.range");
120 addOperator(kind::REGEXP_LOOP
, "re.loop");
123 void Smt2::addFloatingPointOperators() {
124 addOperator(kind::FLOATINGPOINT_FP
, "fp");
125 addOperator(kind::FLOATINGPOINT_EQ
, "fp.eq");
126 addOperator(kind::FLOATINGPOINT_ABS
, "fp.abs");
127 addOperator(kind::FLOATINGPOINT_NEG
, "fp.neg");
128 addOperator(kind::FLOATINGPOINT_PLUS
, "fp.add");
129 addOperator(kind::FLOATINGPOINT_SUB
, "fp.sub");
130 addOperator(kind::FLOATINGPOINT_MULT
, "fp.mul");
131 addOperator(kind::FLOATINGPOINT_DIV
, "fp.div");
132 addOperator(kind::FLOATINGPOINT_FMA
, "fp.fma");
133 addOperator(kind::FLOATINGPOINT_SQRT
, "fp.sqrt");
134 addOperator(kind::FLOATINGPOINT_REM
, "fp.rem");
135 addOperator(kind::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
136 addOperator(kind::FLOATINGPOINT_MIN
, "fp.min");
137 addOperator(kind::FLOATINGPOINT_MAX
, "fp.max");
138 addOperator(kind::FLOATINGPOINT_LEQ
, "fp.leq");
139 addOperator(kind::FLOATINGPOINT_LT
, "fp.lt");
140 addOperator(kind::FLOATINGPOINT_GEQ
, "fp.geq");
141 addOperator(kind::FLOATINGPOINT_GT
, "fp.gt");
142 addOperator(kind::FLOATINGPOINT_ISN
, "fp.isNormal");
143 addOperator(kind::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
144 addOperator(kind::FLOATINGPOINT_ISZ
, "fp.isZero");
145 addOperator(kind::FLOATINGPOINT_ISINF
, "fp.isInfinite");
146 addOperator(kind::FLOATINGPOINT_ISNAN
, "fp.isNaN");
147 addOperator(kind::FLOATINGPOINT_ISNEG
, "fp.isNegative");
148 addOperator(kind::FLOATINGPOINT_ISPOS
, "fp.isPositive");
149 addOperator(kind::FLOATINGPOINT_TO_REAL
, "fp.to_real");
151 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
152 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
153 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
154 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
155 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
156 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
157 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
161 void Smt2::addTheory(Theory theory
) {
164 addOperator(kind::SELECT
, "select");
165 addOperator(kind::STORE
, "store");
168 case THEORY_BITVECTORS
:
169 addBitvectorOperators();
173 defineType("Bool", getExprManager()->booleanType());
174 defineVar("true", getExprManager()->mkConst(true));
175 defineVar("false", getExprManager()->mkConst(false));
176 Parser::addOperator(kind::AND
);
177 Parser::addOperator(kind::DISTINCT
);
178 Parser::addOperator(kind::EQUAL
);
179 Parser::addOperator(kind::IFF
);
180 Parser::addOperator(kind::IMPLIES
);
181 Parser::addOperator(kind::ITE
);
182 Parser::addOperator(kind::NOT
);
183 Parser::addOperator(kind::OR
);
184 Parser::addOperator(kind::XOR
);
187 case THEORY_REALS_INTS
:
188 defineType("Real", getExprManager()->realType());
189 Parser::addOperator(kind::DIVISION
);
190 addOperator(kind::TO_INTEGER
, "to_int");
191 addOperator(kind::IS_INTEGER
, "is_int");
192 addOperator(kind::TO_REAL
, "to_real");
193 // falling through on purpose, to add Ints part of Reals_Ints
195 defineType("Int", getExprManager()->integerType());
196 addArithmeticOperators();
197 addOperator(kind::INTS_DIVISION
, "div");
198 addOperator(kind::INTS_MODULUS
, "mod");
199 addOperator(kind::ABS
, "abs");
200 Parser::addOperator(kind::DIVISIBLE
);
204 defineType("Real", getExprManager()->realType());
205 addArithmeticOperators();
206 Parser::addOperator(kind::DIVISION
);
209 case THEORY_QUANTIFIERS
:
213 addOperator(kind::UNION
, "union");
214 addOperator(kind::INTERSECTION
, "intersection");
215 addOperator(kind::SETMINUS
, "setminus");
216 addOperator(kind::SUBSET
, "subset");
217 addOperator(kind::MEMBER
, "member");
218 addOperator(kind::SINGLETON
, "singleton");
219 addOperator(kind::INSERT
, "insert");
222 case THEORY_DATATYPES
:
223 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
224 Parser::addOperator(kind::APPLY_TESTER
);
225 Parser::addOperator(kind::APPLY_SELECTOR
);
226 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
230 defineType("String", getExprManager()->stringType());
231 addStringOperators();
235 Parser::addOperator(kind::APPLY_UF
);
239 defineType("RoundingMode", getExprManager()->roundingModeType());
240 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
241 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
242 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
243 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
244 addFloatingPointOperators();
248 std::stringstream ss
;
249 ss
<< "internal error: unsupported theory " << theory
;
250 throw ParserException(ss
.str());
254 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
255 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
257 Parser::addOperator(kind
);
258 operatorKindMap
[name
] = kind
;
261 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
262 // precondition: isOperatorEnabled(name)
263 return operatorKindMap
.find(name
)->second
;
266 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
267 return operatorKindMap
.find(name
) != operatorKindMap
.end();
270 bool Smt2::isTheoryEnabled(Theory theory
) const {
273 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
274 case THEORY_BITVECTORS
:
275 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
278 case THEORY_DATATYPES
:
279 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
281 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
282 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
284 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
285 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
286 case THEORY_REALS_INTS
:
287 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
288 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
289 case THEORY_QUANTIFIERS
:
290 return d_logic
.isQuantified();
292 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
294 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
296 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
298 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
300 std::stringstream ss
;
301 ss
<< "internal error: unsupported theory " << theory
;
302 throw ParserException(ss
.str());
306 bool Smt2::logicIsSet() {
312 d_logic
= LogicInfo();
313 operatorKindMap
.clear();
314 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
315 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
316 this->Parser::reset();
318 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
319 if( !strictModeEnabled() ) {
320 addTheory(Smt2::THEORY_CORE
);
324 void Smt2::resetAssertions() {
325 this->Parser::reset();
328 void Smt2::setLogic(std::string name
) {
330 if(name
== "Arrays") {
332 } else if(name
== "Reals") {
334 } else if(name
== "LIA") {
336 } else if(name
== "LRA") {
338 } else if(name
== "LIRA") {
340 } else if(name
== "BV") {
343 std::stringstream ss
;
344 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
345 parseError(ss
.str());
350 if(logicIsForced()) {
351 d_logic
= getForcedLogic();
356 // Core theory belongs to every logic
357 addTheory(THEORY_CORE
);
359 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
360 addTheory(THEORY_UF
);
363 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
364 if(d_logic
.areIntegersUsed()) {
365 if(d_logic
.areRealsUsed()) {
366 addTheory(THEORY_REALS_INTS
);
368 addTheory(THEORY_INTS
);
370 } else if(d_logic
.areRealsUsed()) {
371 addTheory(THEORY_REALS
);
375 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
376 addTheory(THEORY_ARRAYS
);
379 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
380 addTheory(THEORY_BITVECTORS
);
383 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
384 addTheory(THEORY_DATATYPES
);
387 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
388 addTheory(THEORY_SETS
);
391 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
392 addTheory(THEORY_STRINGS
);
395 if(d_logic
.isQuantified()) {
396 addTheory(THEORY_QUANTIFIERS
);
399 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
400 addTheory(THEORY_FP
);
403 }/* Smt2::setLogic() */
405 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
409 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
413 void Smt2::checkThatLogicIsSet() {
414 if( ! logicIsSet() ) {
415 if(strictModeEnabled()) {
416 parseError("set-logic must appear before this point.");
421 warning("No set-logic command was given before this point.");
422 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
423 warning("Consider setting a stricter logic for (likely) better performance.");
424 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
426 setLogic("ALL_SUPPORTED");
429 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
436 /* The include are managed in the lexer but called in the parser */
437 // Inspired by http://www.antlr3.org/api/C/interop.html
439 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
440 Debug("parser") << "Including " << filename
<< std::endl
;
441 // Create a new input stream and take advantage of built in stream stacking
442 // in C target runtime.
444 pANTLR3_INPUT_STREAM in
;
445 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
446 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
447 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
448 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
449 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
451 Debug("parser") << "Can't open " << filename
<< std::endl
;
454 // Same thing as the predefined PUSHSTREAM(in);
455 lexer
->pushCharStream(lexer
, in
);
457 //lexer->rec->state->tokenStartCharIndex = -10;
458 //lexer->emit(lexer);
460 // Note that the input stream is not closed when it EOFs, I don't bother
461 // to do it here, but it is up to you to track streams created like this
462 // and destroy them when the whole parse session is complete. Remember that you
463 // don't want to do this until all tokens have been manipulated all the way through
464 // your tree parsers etc as the token does not store the text it just refers
465 // back to the input stream and trying to get the text for it will abort if you
466 // close the input stream too early.
468 //TODO what said before
472 void Smt2::includeFile(const std::string
& filename
) {
473 // security for online version
474 if(!canIncludeFile()) {
475 parseError("include-file feature was disabled for this run.");
479 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
480 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
481 // get the name of the current stream "Does it work inside an include?"
482 const std::string inputName
= ai
->getInputStreamName();
484 // Find the directory of the current input file
486 size_t pos
= inputName
.rfind('/');
487 if(pos
!= std::string::npos
) {
488 path
= std::string(inputName
, 0, pos
+ 1);
490 path
.append(filename
);
491 if(!newInputStream(path
, lexer
)) {
492 parseError("Couldn't open include file `" + path
+ "'");
498 void Smt2::defineSygusFuns() {
499 // only define each one once
500 while(d_nextSygusFun
< d_sygusFuns
.size()) {
501 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
502 std::string fun
= p
.first
;
503 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
504 Expr eval
= p
.second
;
505 FunctionType evalType
= eval
.getType();
506 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
507 Type rangeType
= evalType
.getRangeType();
508 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
510 // first make the function type
511 std::vector
<Expr
> sygusVars
;
512 std::vector
<Type
> funType
;
513 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
514 funType
.push_back(argTypes
[j
]);
515 std::stringstream ss
;
516 ss
<< fun
<< "_v_" << j
;
517 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
519 Type funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
520 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
522 // copy the bound vars
524 std::vector<Expr> sygusVars;
525 //std::vector<Type> types;
526 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
527 std::stringstream ss;
528 ss << d_sygusVars[i];
529 Type type = d_sygusVars[i].getType();
530 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
531 //types.push_back(type);
533 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
536 //Type t = getExprManager()->mkFunctionType(types, rangeType);
537 //Debug("parser-sygus") << "...function type : " << t << std::endl;
539 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
540 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
541 std::vector
<Expr
> applyv
;
542 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
543 d_sygusFunSymbols
.push_back(funbv
);
544 applyv
.push_back(eval
);
545 applyv
.push_back(funbv
);
546 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
547 applyv
.push_back(sygusVars
[i
]);
549 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
550 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
551 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
558 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
559 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
) {
560 for( unsigned i
=0; i
<cnames
.size(); i
++ ){
561 std::string name
= dt
.getName() + "_" + cnames
[i
];
562 std::string
testerId("is-");
563 testerId
.append(name
);
564 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
565 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
566 CVC4::DatatypeConstructor
c(name
, testerId
, ops
[i
] );
567 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
568 std::stringstream sname
;
569 sname
<< name
<< "_" << j
;
570 c
.addArg(sname
.str(), cargs
[i
][j
]);
572 dt
.addConstructor(c
);
576 // i is index in datatypes/ops
577 // j is index is datatype
578 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
579 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
580 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
581 const DatatypeConstructor
& ctor
= dt
[j
];
582 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
583 std::vector
<Expr
> bvs
, extraArgs
;
584 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
585 std::string vname
= "v_" + ctor
[k
].getName();
586 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
588 extraArgs
.push_back(bv
);
590 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
591 Expr bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
592 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
593 std::vector
<Expr
> patv
;
594 patv
.push_back(eval
);
595 std::vector
<Expr
> applyv
;
596 applyv
.push_back(ctor
.getConstructor());
597 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
598 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
600 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
601 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
602 patv
.push_back(cpatv
);
603 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
604 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
605 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
606 std::vector
<Expr
> builtApply
;
607 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
608 std::vector
<Expr
> patvb
;
609 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
610 patvb
.push_back(extraArgs
[k
]);
611 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
612 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
614 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
617 //if( ops[i][j].getKind() == kind::BUILTIN ){
618 if( !builtApply
.empty() ){
619 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
620 builtTerm
= getExprManager()->mkExpr(kind::APPLY
, ops
[i
][j
], builtApply
);
622 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
625 builtTerm
= ops
[i
][j
];
627 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
628 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
629 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
630 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
631 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
632 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
634 //linearize multiplication if possible
635 if( builtTerm
.getKind()==kind::MULT
){
636 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
637 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
638 if( at
.isDatatype() ){
639 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
640 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
641 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
642 if( itd
!=datatypeTypes
.end() ){
643 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
644 unsigned index
= itd
-datatypeTypes
.begin();
645 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
647 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
648 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
649 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
655 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
656 const Datatype
& atdd
= atd
.getDatatype();
657 std::vector
<Expr
> assertions
;
658 std::vector
<Expr
> nbvs
;
659 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
661 nbvs
.push_back( bvl
[a
] );
664 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
665 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
666 //Make new assertion based on partially instantiating existing
667 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
668 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
669 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
670 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
672 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
673 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
674 builtApply
[k
] = ops
[index
][cc
];
675 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
676 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
677 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
678 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
679 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
680 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
681 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
682 assertions
.push_back( eassertion
);
684 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
685 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
695 }/* CVC4::parser namespace */
696 }/* CVC4 namespace */