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 defineType("Int", getExprManager()->integerType());
232 addStringOperators();
236 Parser::addOperator(kind::APPLY_UF
);
240 defineType("RoundingMode", getExprManager()->roundingModeType());
241 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
242 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
243 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
244 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
245 addFloatingPointOperators();
249 std::stringstream ss
;
250 ss
<< "internal error: unsupported theory " << theory
;
251 throw ParserException(ss
.str());
255 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
256 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
258 Parser::addOperator(kind
);
259 operatorKindMap
[name
] = kind
;
262 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
263 // precondition: isOperatorEnabled(name)
264 return operatorKindMap
.find(name
)->second
;
267 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
268 return operatorKindMap
.find(name
) != operatorKindMap
.end();
271 bool Smt2::isTheoryEnabled(Theory theory
) const {
274 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
275 case THEORY_BITVECTORS
:
276 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
279 case THEORY_DATATYPES
:
280 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
282 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
283 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
285 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
286 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
287 case THEORY_REALS_INTS
:
288 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
289 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
290 case THEORY_QUANTIFIERS
:
291 return d_logic
.isQuantified();
293 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
295 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
297 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
299 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
301 std::stringstream ss
;
302 ss
<< "internal error: unsupported theory " << theory
;
303 throw ParserException(ss
.str());
307 bool Smt2::logicIsSet() {
313 d_logic
= LogicInfo();
314 operatorKindMap
.clear();
315 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
316 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
317 this->Parser::reset();
319 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
320 if( !strictModeEnabled() ) {
321 addTheory(Smt2::THEORY_CORE
);
325 void Smt2::resetAssertions() {
326 this->Parser::reset();
329 void Smt2::setLogic(std::string name
) {
331 if(name
== "Arrays") {
333 } else if(name
== "Reals") {
335 } else if(name
== "LIA") {
337 } else if(name
== "LRA") {
339 } else if(name
== "LIRA") {
341 } else if(name
== "BV") {
344 std::stringstream ss
;
345 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
346 parseError(ss
.str());
351 if(logicIsForced()) {
352 d_logic
= getForcedLogic();
357 // Core theory belongs to every logic
358 addTheory(THEORY_CORE
);
360 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
361 addTheory(THEORY_UF
);
364 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
365 if(d_logic
.areIntegersUsed()) {
366 if(d_logic
.areRealsUsed()) {
367 addTheory(THEORY_REALS_INTS
);
369 addTheory(THEORY_INTS
);
371 } else if(d_logic
.areRealsUsed()) {
372 addTheory(THEORY_REALS
);
376 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
377 addTheory(THEORY_ARRAYS
);
380 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
381 addTheory(THEORY_BITVECTORS
);
384 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
385 addTheory(THEORY_DATATYPES
);
388 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
389 addTheory(THEORY_SETS
);
392 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
393 addTheory(THEORY_STRINGS
);
396 if(d_logic
.isQuantified()) {
397 addTheory(THEORY_QUANTIFIERS
);
400 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
401 addTheory(THEORY_FP
);
404 }/* Smt2::setLogic() */
406 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
410 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
414 void Smt2::checkThatLogicIsSet() {
415 if( ! logicIsSet() ) {
416 if(strictModeEnabled()) {
417 parseError("set-logic must appear before this point.");
422 warning("No set-logic command was given before this point.");
423 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
424 warning("Consider setting a stricter logic for (likely) better performance.");
425 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
427 setLogic("ALL_SUPPORTED");
430 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
437 /* The include are managed in the lexer but called in the parser */
438 // Inspired by http://www.antlr3.org/api/C/interop.html
440 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
441 Debug("parser") << "Including " << filename
<< std::endl
;
442 // Create a new input stream and take advantage of built in stream stacking
443 // in C target runtime.
445 pANTLR3_INPUT_STREAM in
;
446 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
447 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
448 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
449 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
450 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
452 Debug("parser") << "Can't open " << filename
<< std::endl
;
455 // Same thing as the predefined PUSHSTREAM(in);
456 lexer
->pushCharStream(lexer
, in
);
458 //lexer->rec->state->tokenStartCharIndex = -10;
459 //lexer->emit(lexer);
461 // Note that the input stream is not closed when it EOFs, I don't bother
462 // to do it here, but it is up to you to track streams created like this
463 // and destroy them when the whole parse session is complete. Remember that you
464 // don't want to do this until all tokens have been manipulated all the way through
465 // your tree parsers etc as the token does not store the text it just refers
466 // back to the input stream and trying to get the text for it will abort if you
467 // close the input stream too early.
469 //TODO what said before
473 void Smt2::includeFile(const std::string
& filename
) {
474 // security for online version
475 if(!canIncludeFile()) {
476 parseError("include-file feature was disabled for this run.");
480 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
481 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
482 // get the name of the current stream "Does it work inside an include?"
483 const std::string inputName
= ai
->getInputStreamName();
485 // Find the directory of the current input file
487 size_t pos
= inputName
.rfind('/');
488 if(pos
!= std::string::npos
) {
489 path
= std::string(inputName
, 0, pos
+ 1);
491 path
.append(filename
);
492 if(!newInputStream(path
, lexer
)) {
493 parseError("Couldn't open include file `" + path
+ "'");
499 void Smt2::defineSygusFuns() {
500 // only define each one once
501 while(d_nextSygusFun
< d_sygusFuns
.size()) {
502 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
503 std::string fun
= p
.first
;
504 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
505 Expr eval
= p
.second
;
506 FunctionType evalType
= eval
.getType();
507 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
508 Type rangeType
= evalType
.getRangeType();
509 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
511 // first make the function type
512 std::vector
<Expr
> sygusVars
;
513 std::vector
<Type
> funType
;
514 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
515 funType
.push_back(argTypes
[j
]);
516 std::stringstream ss
;
517 ss
<< fun
<< "_v_" << j
;
518 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
521 if( !funType
.empty() ){
522 funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
523 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
525 // copy the bound vars
527 std::vector<Expr> sygusVars;
528 //std::vector<Type> types;
529 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
530 std::stringstream ss;
531 ss << d_sygusVars[i];
532 Type type = d_sygusVars[i].getType();
533 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
534 //types.push_back(type);
536 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
539 //Type t = getExprManager()->mkFunctionType(types, rangeType);
540 //Debug("parser-sygus") << "...function type : " << t << std::endl;
544 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
545 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
546 std::vector
<Expr
> applyv
;
547 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
548 d_sygusFunSymbols
.push_back(funbv
);
549 applyv
.push_back(eval
);
550 applyv
.push_back(funbv
);
551 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
552 applyv
.push_back(sygusVars
[i
]);
554 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
555 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
556 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
563 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
564 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
) {
565 for( unsigned i
=0; i
<cnames
.size(); i
++ ){
566 std::string name
= dt
.getName() + "_" + cnames
[i
];
567 std::string
testerId("is-");
568 testerId
.append(name
);
569 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
570 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
571 CVC4::DatatypeConstructor
c(name
, testerId
, ops
[i
] );
572 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
573 std::stringstream sname
;
574 sname
<< name
<< "_" << j
;
575 c
.addArg(sname
.str(), cargs
[i
][j
]);
577 dt
.addConstructor(c
);
581 // i is index in datatypes/ops
582 // j is index is datatype
583 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
584 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
585 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
586 const DatatypeConstructor
& ctor
= dt
[j
];
587 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
588 std::vector
<Expr
> bvs
, extraArgs
;
589 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
590 std::string vname
= "v_" + ctor
[k
].getName();
591 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
593 extraArgs
.push_back(bv
);
595 if( !terms
[0].isNull() ){
596 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
600 bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
602 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
603 std::vector
<Expr
> patv
;
604 patv
.push_back(eval
);
605 std::vector
<Expr
> applyv
;
606 applyv
.push_back(ctor
.getConstructor());
607 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
608 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
610 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
611 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
612 patv
.push_back(cpatv
);
613 if( !terms
[0].isNull() ){
614 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
616 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
617 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
618 std::vector
<Expr
> builtApply
;
619 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
620 std::vector
<Expr
> patvb
;
621 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
622 patvb
.push_back(extraArgs
[k
]);
623 if( !terms
[0].isNull() ){
624 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
626 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
628 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
631 //if( ops[i][j].getKind() == kind::BUILTIN ){
632 if( !builtApply
.empty() ){
633 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
634 builtTerm
= getExprManager()->mkExpr(kind::APPLY
, ops
[i
][j
], builtApply
);
636 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
639 builtTerm
= ops
[i
][j
];
641 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
642 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
644 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
645 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
646 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
648 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
650 //linearize multiplication if possible
651 if( builtTerm
.getKind()==kind::MULT
){
652 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
653 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
654 if( at
.isDatatype() ){
655 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
656 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
657 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
658 if( itd
!=datatypeTypes
.end() ){
659 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
660 unsigned index
= itd
-datatypeTypes
.begin();
661 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
663 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
664 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
665 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
671 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
672 const Datatype
& atdd
= atd
.getDatatype();
673 std::vector
<Expr
> assertions
;
674 std::vector
<Expr
> nbvs
;
675 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
677 nbvs
.push_back( bvl
[a
] );
680 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
681 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
682 //Make new assertion based on partially instantiating existing
683 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
684 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
685 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
686 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
688 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
689 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
690 builtApply
[k
] = ops
[index
][cc
];
691 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
692 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
693 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
694 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
695 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
696 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
697 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
698 assertions
.push_back( eassertion
);
700 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
701 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
711 }/* CVC4::parser namespace */
712 }/* CVC4 namespace */