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 #include "util/bitvector.h"
26 // ANTLR defines these, which is really bad!
33 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
34 Parser(exprManager
,input
,strictMode
,parseOnly
),
37 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
38 if( !strictModeEnabled() ) {
39 addTheory(Smt2::THEORY_CORE
);
43 void Smt2::addArithmeticOperators() {
44 Parser::addOperator(kind::PLUS
);
45 Parser::addOperator(kind::MINUS
);
46 Parser::addOperator(kind::UMINUS
);
47 Parser::addOperator(kind::MULT
);
48 Parser::addOperator(kind::LT
);
49 Parser::addOperator(kind::LEQ
);
50 Parser::addOperator(kind::GT
);
51 Parser::addOperator(kind::GEQ
);
54 void Smt2::addBitvectorOperators() {
55 addOperator(kind::BITVECTOR_CONCAT
, "concat");
56 addOperator(kind::BITVECTOR_NOT
, "bvnot");
57 addOperator(kind::BITVECTOR_AND
, "bvand");
58 addOperator(kind::BITVECTOR_OR
, "bvor");
59 addOperator(kind::BITVECTOR_NEG
, "bvneg");
60 addOperator(kind::BITVECTOR_PLUS
, "bvadd");
61 addOperator(kind::BITVECTOR_MULT
, "bvmul");
62 addOperator(kind::BITVECTOR_UDIV
, "bvudiv");
63 addOperator(kind::BITVECTOR_UREM
, "bvurem");
64 addOperator(kind::BITVECTOR_SHL
, "bvshl");
65 addOperator(kind::BITVECTOR_LSHR
, "bvlshr");
66 addOperator(kind::BITVECTOR_ULT
, "bvult");
67 addOperator(kind::BITVECTOR_NAND
, "bvnand");
68 addOperator(kind::BITVECTOR_NOR
, "bvnor");
69 addOperator(kind::BITVECTOR_XOR
, "bvxor");
70 addOperator(kind::BITVECTOR_XNOR
, "bvxnor");
71 addOperator(kind::BITVECTOR_COMP
, "bvcomp");
72 addOperator(kind::BITVECTOR_SUB
, "bvsub");
73 addOperator(kind::BITVECTOR_SDIV
, "bvsdiv");
74 addOperator(kind::BITVECTOR_SREM
, "bvsrem");
75 addOperator(kind::BITVECTOR_SMOD
, "bvsmod");
76 addOperator(kind::BITVECTOR_ASHR
, "bvashr");
77 addOperator(kind::BITVECTOR_ULE
, "bvule");
78 addOperator(kind::BITVECTOR_UGT
, "bvugt");
79 addOperator(kind::BITVECTOR_UGE
, "bvuge");
80 addOperator(kind::BITVECTOR_SLT
, "bvslt");
81 addOperator(kind::BITVECTOR_SLE
, "bvsle");
82 addOperator(kind::BITVECTOR_SGT
, "bvsgt");
83 addOperator(kind::BITVECTOR_SGE
, "bvsge");
85 Parser::addOperator(kind::BITVECTOR_BITOF
);
86 Parser::addOperator(kind::BITVECTOR_EXTRACT
);
87 Parser::addOperator(kind::BITVECTOR_REPEAT
);
88 Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND
);
89 Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND
);
90 Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT
);
91 Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
93 Parser::addOperator(kind::INT_TO_BITVECTOR
);
94 Parser::addOperator(kind::BITVECTOR_TO_NAT
);
97 void Smt2::addStringOperators() {
98 addOperator(kind::STRING_CONCAT
, "str.++");
99 addOperator(kind::STRING_LENGTH
, "str.len");
100 addOperator(kind::STRING_SUBSTR
, "str.substr" );
101 addOperator(kind::STRING_STRCTN
, "str.contains" );
102 addOperator(kind::STRING_CHARAT
, "str.at" );
103 addOperator(kind::STRING_STRIDOF
, "str.indexof" );
104 addOperator(kind::STRING_STRREPL
, "str.replace" );
105 addOperator(kind::STRING_PREFIX
, "str.prefixof" );
106 addOperator(kind::STRING_SUFFIX
, "str.suffixof" );
107 addOperator(kind::STRING_ITOS
, "int.to.str" );
108 addOperator(kind::STRING_STOI
, "str.to.int" );
109 addOperator(kind::STRING_U16TOS
, "u16.to.str" );
110 addOperator(kind::STRING_STOU16
, "str.to.u16" );
111 addOperator(kind::STRING_U32TOS
, "u32.to.str" );
112 addOperator(kind::STRING_STOU32
, "str.to.u32" );
113 addOperator(kind::STRING_IN_REGEXP
, "str.in.re");
114 addOperator(kind::STRING_TO_REGEXP
, "str.to.re");
115 addOperator(kind::REGEXP_CONCAT
, "re.++");
116 addOperator(kind::REGEXP_UNION
, "re.union");
117 addOperator(kind::REGEXP_INTER
, "re.inter");
118 addOperator(kind::REGEXP_STAR
, "re.*");
119 addOperator(kind::REGEXP_PLUS
, "re.+");
120 addOperator(kind::REGEXP_OPT
, "re.opt");
121 addOperator(kind::REGEXP_RANGE
, "re.range");
122 addOperator(kind::REGEXP_LOOP
, "re.loop");
125 void Smt2::addFloatingPointOperators() {
126 addOperator(kind::FLOATINGPOINT_FP
, "fp");
127 addOperator(kind::FLOATINGPOINT_EQ
, "fp.eq");
128 addOperator(kind::FLOATINGPOINT_ABS
, "fp.abs");
129 addOperator(kind::FLOATINGPOINT_NEG
, "fp.neg");
130 addOperator(kind::FLOATINGPOINT_PLUS
, "fp.add");
131 addOperator(kind::FLOATINGPOINT_SUB
, "fp.sub");
132 addOperator(kind::FLOATINGPOINT_MULT
, "fp.mul");
133 addOperator(kind::FLOATINGPOINT_DIV
, "fp.div");
134 addOperator(kind::FLOATINGPOINT_FMA
, "fp.fma");
135 addOperator(kind::FLOATINGPOINT_SQRT
, "fp.sqrt");
136 addOperator(kind::FLOATINGPOINT_REM
, "fp.rem");
137 addOperator(kind::FLOATINGPOINT_RTI
, "fp.roundToIntegral");
138 addOperator(kind::FLOATINGPOINT_MIN
, "fp.min");
139 addOperator(kind::FLOATINGPOINT_MAX
, "fp.max");
140 addOperator(kind::FLOATINGPOINT_LEQ
, "fp.leq");
141 addOperator(kind::FLOATINGPOINT_LT
, "fp.lt");
142 addOperator(kind::FLOATINGPOINT_GEQ
, "fp.geq");
143 addOperator(kind::FLOATINGPOINT_GT
, "fp.gt");
144 addOperator(kind::FLOATINGPOINT_ISN
, "fp.isNormal");
145 addOperator(kind::FLOATINGPOINT_ISSN
, "fp.isSubnormal");
146 addOperator(kind::FLOATINGPOINT_ISZ
, "fp.isZero");
147 addOperator(kind::FLOATINGPOINT_ISINF
, "fp.isInfinite");
148 addOperator(kind::FLOATINGPOINT_ISNAN
, "fp.isNaN");
149 addOperator(kind::FLOATINGPOINT_ISNEG
, "fp.isNegative");
150 addOperator(kind::FLOATINGPOINT_ISPOS
, "fp.isPositive");
151 addOperator(kind::FLOATINGPOINT_TO_REAL
, "fp.to_real");
153 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
);
154 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
);
155 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL
);
156 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
);
157 Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
);
158 Parser::addOperator(kind::FLOATINGPOINT_TO_UBV
);
159 Parser::addOperator(kind::FLOATINGPOINT_TO_SBV
);
163 void Smt2::addTheory(Theory theory
) {
166 addOperator(kind::SELECT
, "select");
167 addOperator(kind::STORE
, "store");
170 case THEORY_BITVECTORS
:
171 addBitvectorOperators();
175 defineType("Bool", getExprManager()->booleanType());
176 defineVar("true", getExprManager()->mkConst(true));
177 defineVar("false", getExprManager()->mkConst(false));
178 Parser::addOperator(kind::AND
);
179 Parser::addOperator(kind::DISTINCT
);
180 Parser::addOperator(kind::EQUAL
);
181 Parser::addOperator(kind::IFF
);
182 Parser::addOperator(kind::IMPLIES
);
183 Parser::addOperator(kind::ITE
);
184 Parser::addOperator(kind::NOT
);
185 Parser::addOperator(kind::OR
);
186 Parser::addOperator(kind::XOR
);
189 case THEORY_REALS_INTS
:
190 defineType("Real", getExprManager()->realType());
191 Parser::addOperator(kind::DIVISION
);
192 addOperator(kind::TO_INTEGER
, "to_int");
193 addOperator(kind::IS_INTEGER
, "is_int");
194 addOperator(kind::TO_REAL
, "to_real");
195 // falling through on purpose, to add Ints part of Reals_Ints
197 defineType("Int", getExprManager()->integerType());
198 addArithmeticOperators();
199 addOperator(kind::INTS_DIVISION
, "div");
200 addOperator(kind::INTS_MODULUS
, "mod");
201 addOperator(kind::ABS
, "abs");
202 Parser::addOperator(kind::DIVISIBLE
);
206 defineType("Real", getExprManager()->realType());
207 addArithmeticOperators();
208 Parser::addOperator(kind::DIVISION
);
211 case THEORY_QUANTIFIERS
:
215 addOperator(kind::UNION
, "union");
216 addOperator(kind::INTERSECTION
, "intersection");
217 addOperator(kind::SETMINUS
, "setminus");
218 addOperator(kind::SUBSET
, "subset");
219 addOperator(kind::MEMBER
, "member");
220 addOperator(kind::SINGLETON
, "singleton");
221 addOperator(kind::INSERT
, "insert");
224 case THEORY_DATATYPES
:
225 Parser::addOperator(kind::APPLY_CONSTRUCTOR
);
226 Parser::addOperator(kind::APPLY_TESTER
);
227 Parser::addOperator(kind::APPLY_SELECTOR
);
228 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL
);
232 defineType("String", getExprManager()->stringType());
233 defineType("Int", getExprManager()->integerType());
234 addStringOperators();
238 Parser::addOperator(kind::APPLY_UF
);
242 defineType("RoundingMode", getExprManager()->roundingModeType());
243 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
244 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
245 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
246 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
247 addFloatingPointOperators();
251 std::stringstream ss
;
252 ss
<< "internal error: unsupported theory " << theory
;
253 throw ParserException(ss
.str());
257 void Smt2::addOperator(Kind kind
, const std::string
& name
) {
258 Debug("parser") << "Smt2::addOperator( " << kind
<< ", " << name
<< " )"
260 Parser::addOperator(kind
);
261 operatorKindMap
[name
] = kind
;
264 Kind
Smt2::getOperatorKind(const std::string
& name
) const {
265 // precondition: isOperatorEnabled(name)
266 return operatorKindMap
.find(name
)->second
;
269 bool Smt2::isOperatorEnabled(const std::string
& name
) const {
270 return operatorKindMap
.find(name
) != operatorKindMap
.end();
273 bool Smt2::isTheoryEnabled(Theory theory
) const {
276 return d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
);
277 case THEORY_BITVECTORS
:
278 return d_logic
.isTheoryEnabled(theory::THEORY_BV
);
281 case THEORY_DATATYPES
:
282 return d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
);
284 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
285 d_logic
.areIntegersUsed() && ( !d_logic
.areRealsUsed() );
287 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
288 ( !d_logic
.areIntegersUsed() ) && d_logic
.areRealsUsed();
289 case THEORY_REALS_INTS
:
290 return d_logic
.isTheoryEnabled(theory::THEORY_ARITH
) &&
291 d_logic
.areIntegersUsed() && d_logic
.areRealsUsed();
292 case THEORY_QUANTIFIERS
:
293 return d_logic
.isQuantified();
295 return d_logic
.isTheoryEnabled(theory::THEORY_SETS
);
297 return d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
);
299 return d_logic
.isTheoryEnabled(theory::THEORY_UF
);
301 return d_logic
.isTheoryEnabled(theory::THEORY_FP
);
303 std::stringstream ss
;
304 ss
<< "internal error: unsupported theory " << theory
;
305 throw ParserException(ss
.str());
309 bool Smt2::logicIsSet() {
315 d_logic
= LogicInfo();
316 operatorKindMap
.clear();
317 d_lastNamedTerm
= std::pair
<Expr
, std::string
>();
318 d_unsatCoreNames
= std::stack
< std::map
<Expr
, std::string
> >();
319 this->Parser::reset();
321 d_unsatCoreNames
.push(std::map
<Expr
, std::string
>());
322 if( !strictModeEnabled() ) {
323 addTheory(Smt2::THEORY_CORE
);
327 void Smt2::resetAssertions() {
328 this->Parser::reset();
331 void Smt2::setLogic(std::string name
) {
333 if(name
== "Arrays") {
335 } else if(name
== "Reals") {
337 } else if(name
== "LIA") {
339 } else if(name
== "LRA") {
341 } else if(name
== "LIRA") {
343 } else if(name
== "BV") {
346 std::stringstream ss
;
347 ss
<< "Unknown SyGuS background logic `" << name
<< "'";
348 parseError(ss
.str());
353 if(logicIsForced()) {
354 d_logic
= getForcedLogic();
359 // Core theory belongs to every logic
360 addTheory(THEORY_CORE
);
362 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
363 addTheory(THEORY_UF
);
366 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
367 if(d_logic
.areIntegersUsed()) {
368 if(d_logic
.areRealsUsed()) {
369 addTheory(THEORY_REALS_INTS
);
371 addTheory(THEORY_INTS
);
373 } else if(d_logic
.areRealsUsed()) {
374 addTheory(THEORY_REALS
);
378 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
379 addTheory(THEORY_ARRAYS
);
382 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
383 addTheory(THEORY_BITVECTORS
);
386 if(d_logic
.isTheoryEnabled(theory::THEORY_DATATYPES
)) {
387 addTheory(THEORY_DATATYPES
);
390 if(d_logic
.isTheoryEnabled(theory::THEORY_SETS
)) {
391 addTheory(THEORY_SETS
);
394 if(d_logic
.isTheoryEnabled(theory::THEORY_STRINGS
)) {
395 addTheory(THEORY_STRINGS
);
398 if(d_logic
.isQuantified()) {
399 addTheory(THEORY_QUANTIFIERS
);
402 if (d_logic
.isTheoryEnabled(theory::THEORY_FP
)) {
403 addTheory(THEORY_FP
);
406 }/* Smt2::setLogic() */
408 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
412 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
416 void Smt2::checkThatLogicIsSet() {
417 if( ! logicIsSet() ) {
418 if(strictModeEnabled()) {
419 parseError("set-logic must appear before this point.");
424 warning("No set-logic command was given before this point.");
425 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
426 warning("Consider setting a stricter logic for (likely) better performance.");
427 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
429 setLogic("ALL_SUPPORTED");
432 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
439 /* The include are managed in the lexer but called in the parser */
440 // Inspired by http://www.antlr3.org/api/C/interop.html
442 static bool newInputStream(const std::string
& filename
, pANTLR3_LEXER lexer
) {
443 Debug("parser") << "Including " << filename
<< std::endl
;
444 // Create a new input stream and take advantage of built in stream stacking
445 // in C target runtime.
447 pANTLR3_INPUT_STREAM in
;
448 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
449 in
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) filename
.c_str());
450 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
451 in
= antlr3FileStreamNew((pANTLR3_UINT8
) filename
.c_str(), ANTLR3_ENC_8BIT
);
452 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
454 Debug("parser") << "Can't open " << filename
<< std::endl
;
457 // Same thing as the predefined PUSHSTREAM(in);
458 lexer
->pushCharStream(lexer
, in
);
460 //lexer->rec->state->tokenStartCharIndex = -10;
461 //lexer->emit(lexer);
463 // Note that the input stream is not closed when it EOFs, I don't bother
464 // to do it here, but it is up to you to track streams created like this
465 // and destroy them when the whole parse session is complete. Remember that you
466 // don't want to do this until all tokens have been manipulated all the way through
467 // your tree parsers etc as the token does not store the text it just refers
468 // back to the input stream and trying to get the text for it will abort if you
469 // close the input stream too early.
471 //TODO what said before
475 void Smt2::includeFile(const std::string
& filename
) {
476 // security for online version
477 if(!canIncludeFile()) {
478 parseError("include-file feature was disabled for this run.");
482 AntlrInput
* ai
= static_cast<AntlrInput
*>(getInput());
483 pANTLR3_LEXER lexer
= ai
->getAntlr3Lexer();
484 // get the name of the current stream "Does it work inside an include?"
485 const std::string inputName
= ai
->getInputStreamName();
487 // Find the directory of the current input file
489 size_t pos
= inputName
.rfind('/');
490 if(pos
!= std::string::npos
) {
491 path
= std::string(inputName
, 0, pos
+ 1);
493 path
.append(filename
);
494 if(!newInputStream(path
, lexer
)) {
495 parseError("Couldn't open include file `" + path
+ "'");
499 void Smt2::mkSygusDefaultGrammar( const Type
& range
, Expr
& bvl
, const std::string
& fun
, std::vector
<CVC4::Datatype
>& datatypes
,
500 std::vector
<Type
>& sorts
, std::vector
< std::vector
<Expr
> >& ops
, std::vector
<Expr
> sygus_vars
) {
502 Debug("parser-sygus") << "Construct default grammar for " << fun
<< " " << range
<< std::endl
;
504 std::stringstream ssb
;
505 ssb
<< fun
<< "_Bool";
506 std::string dbname
= ssb
.str();
508 std::stringstream ss
;
509 ss
<< fun
<< "_" << range
;
510 std::string dname
= ss
.str();
511 datatypes
.push_back(Datatype(dname
));
512 ops
.push_back(std::vector
<Expr
>());
513 std::vector
<std::string
> cnames
;
514 std::vector
<std::vector
<CVC4::Type
> > cargs
;
516 for( unsigned i
=0; i
<sygus_vars
.size(); i
++ ){
517 if( sygus_vars
[i
].getType()==range
){
518 std::stringstream ss
;
520 Debug("parser-sygus") << "...add for variable " << ss
.str() << std::endl
;
521 ops
.back().push_back( sygus_vars
[i
] );
522 cnames
.push_back( ss
.str() );
523 cargs
.push_back( std::vector
< CVC4::Type
>() );
527 std::vector
< Expr
> consts
;
528 mkSygusConstantsForType( range
, consts
);
529 for( unsigned i
=0; i
<consts
.size(); i
++ ){
530 std::stringstream ss
;
532 Debug("parser-sygus") << "...add for constant " << ss
.str() << std::endl
;
533 ops
.back().push_back( consts
[i
] );
534 cnames
.push_back( ss
.str() );
535 cargs
.push_back( std::vector
< CVC4::Type
>() );
538 CVC4::Kind k
= kind::ITE
;
539 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
540 ops
.back().push_back(getExprManager()->operatorOf(k
));
541 cnames
.push_back( kind::kindToString(k
) );
542 cargs
.push_back( std::vector
< CVC4::Type
>() );
543 cargs
.back().push_back(mkUnresolvedType(ssb
.str()));
544 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
545 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
547 if( range
.isInteger() ){
548 for( unsigned i
=0; i
<2; i
++ ){
549 CVC4::Kind k
= i
==0 ? kind::PLUS
: kind::MINUS
;
550 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
551 ops
.back().push_back(getExprManager()->operatorOf(k
));
552 cnames
.push_back(kind::kindToString(k
));
553 cargs
.push_back( std::vector
< CVC4::Type
>() );
554 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
555 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
558 std::stringstream sserr
;
559 sserr
<< "Don't know default Sygus grammar for type " << range
<< std::endl
;
560 parseError(sserr
.str());
562 Debug("parser-sygus") << "...make datatype " << datatypes
.back() << std::endl
;
563 datatypes
.back().setSygus( range
, bvl
, true, true );
564 mkSygusDatatype( datatypes
.back(), ops
.back(), cnames
, cargs
);
565 sorts
.push_back( range
);
568 datatypes
.push_back(Datatype(dbname
));
569 ops
.push_back(std::vector
<Expr
>());
572 for( unsigned i
=0; i
<4; i
++ ){
573 CVC4::Kind k
= i
==0 ? kind::NOT
: ( i
==1 ? kind::AND
: ( i
==2 ? kind::OR
: kind::EQUAL
) );
574 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
575 ops
.back().push_back(getExprManager()->operatorOf(k
));
576 cnames
.push_back(kind::kindToString(k
));
577 cargs
.push_back( std::vector
< CVC4::Type
>() );
579 cargs
.back().push_back(mkUnresolvedType(ssb
.str()));
580 }else if( k
==kind::AND
|| k
==kind::OR
){
581 cargs
.back().push_back(mkUnresolvedType(ssb
.str()));
582 cargs
.back().push_back(mkUnresolvedType(ssb
.str()));
583 }else if( k
==kind::EQUAL
){
584 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
585 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
588 if( range
.isInteger() ){
589 CVC4::Kind k
= kind::LEQ
;
590 Debug("parser-sygus") << "...add for " << k
<< std::endl
;
591 ops
.back().push_back(getExprManager()->operatorOf(k
));
592 cnames
.push_back(kind::kindToString(k
));
593 cargs
.push_back( std::vector
< CVC4::Type
>() );
594 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
595 cargs
.back().push_back(mkUnresolvedType(ss
.str()));
597 Debug("parser-sygus") << "...make datatype " << datatypes
.back() << std::endl
;
598 Type btype
= getExprManager()->booleanType();
599 datatypes
.back().setSygus( btype
, bvl
, true, true );
600 mkSygusDatatype( datatypes
.back(), ops
.back(), cnames
, cargs
);
601 sorts
.push_back( btype
);
603 Debug("parser-sygus") << "...finished make default grammar for " << fun
<< " " << range
<< std::endl
;
606 void Smt2::mkSygusConstantsForType( const Type
& type
, std::vector
<CVC4::Expr
>& ops
) {
607 if( type
.isInteger() ){
608 ops
.push_back(getExprManager()->mkConst(Rational(0)));
609 ops
.push_back(getExprManager()->mkConst(Rational(1)));
610 }else if( type
.isBitVector() ){
611 unsigned sz
= ((BitVectorType
)type
).getSize();
612 BitVector
bval0(sz
, (unsigned int)0);
613 ops
.push_back( getExprManager()->mkConst(bval0
) );
614 BitVector
bval1(sz
, (unsigned int)1);
615 ops
.push_back( getExprManager()->mkConst(bval1
) );
620 void Smt2::defineSygusFuns() {
621 // only define each one once
622 while(d_nextSygusFun
< d_sygusFuns
.size()) {
623 std::pair
<std::string
, Expr
> p
= d_sygusFuns
[d_nextSygusFun
];
624 std::string fun
= p
.first
;
625 Debug("parser-sygus") << "Sygus : define fun " << fun
<< std::endl
;
626 Expr eval
= p
.second
;
627 FunctionType evalType
= eval
.getType();
628 std::vector
<Type
> argTypes
= evalType
.getArgTypes();
629 Type rangeType
= evalType
.getRangeType();
630 Debug("parser-sygus") << "...eval type : " << evalType
<< ", #args=" << argTypes
.size() << std::endl
;
632 // first make the function type
633 std::vector
<Expr
> sygusVars
;
634 std::vector
<Type
> funType
;
635 for(size_t j
= 1; j
< argTypes
.size(); ++j
) {
636 funType
.push_back(argTypes
[j
]);
637 std::stringstream ss
;
638 ss
<< fun
<< "_v_" << j
;
639 sygusVars
.push_back(getExprManager()->mkBoundVar(ss
.str(), argTypes
[j
]));
642 if( !funType
.empty() ){
643 funt
= getExprManager()->mkFunctionType(funType
, rangeType
);
644 Debug("parser-sygus") << "...eval function type : " << funt
<< std::endl
;
646 // copy the bound vars
648 std::vector<Expr> sygusVars;
649 //std::vector<Type> types;
650 for(size_t i = 0; i < d_sygusVars.size(); ++i) {
651 std::stringstream ss;
652 ss << d_sygusVars[i];
653 Type type = d_sygusVars[i].getType();
654 sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
655 //types.push_back(type);
657 Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
660 //Type t = getExprManager()->mkFunctionType(types, rangeType);
661 //Debug("parser-sygus") << "...function type : " << t << std::endl;
665 Expr lambda
= mkFunction(fun
, funt
, ExprManager::VAR_FLAG_DEFINED
);
666 Debug("parser-sygus") << "...made function : " << lambda
<< std::endl
;
667 std::vector
<Expr
> applyv
;
668 Expr funbv
= getExprManager()->mkBoundVar(std::string("f") + fun
, argTypes
[0]);
669 d_sygusFunSymbols
.push_back(funbv
);
670 applyv
.push_back(eval
);
671 applyv
.push_back(funbv
);
672 for(size_t i
= 0; i
< sygusVars
.size(); ++i
) {
673 applyv
.push_back(sygusVars
[i
]);
675 Expr apply
= getExprManager()->mkExpr(kind::APPLY_UF
, applyv
);
676 Debug("parser-sygus") << "...made apply " << apply
<< std::endl
;
677 Command
* cmd
= new DefineFunctionCommand(fun
, lambda
, sygusVars
, apply
);
684 void Smt2::mkSygusDatatype( CVC4::Datatype
& dt
, std::vector
<CVC4::Expr
>& ops
,
685 std::vector
<std::string
>& cnames
, std::vector
< std::vector
< CVC4::Type
> >& cargs
) {
686 for( unsigned i
=0; i
<cnames
.size(); i
++ ){
687 std::string name
= dt
.getName() + "_" + cnames
[i
];
688 std::string
testerId("is-");
689 testerId
.append(name
);
690 checkDeclaration(name
, CHECK_UNDECLARED
, SYM_VARIABLE
);
691 checkDeclaration(testerId
, CHECK_UNDECLARED
, SYM_VARIABLE
);
692 CVC4::DatatypeConstructor
c(name
, testerId
, ops
[i
] );
693 for( unsigned j
=0; j
<cargs
[i
].size(); j
++ ){
694 std::stringstream sname
;
695 sname
<< name
<< "_" << j
;
696 c
.addArg(sname
.str(), cargs
[i
][j
]);
698 dt
.addConstructor(c
);
702 // i is index in datatypes/ops
703 // j is index is datatype
704 Expr
Smt2::getSygusAssertion( std::vector
<DatatypeType
>& datatypeTypes
, std::vector
< std::vector
<Expr
> >& ops
,
705 std::map
<DatatypeType
, Expr
>& evals
, std::vector
<Expr
>& terms
,
706 Expr eval
, const Datatype
& dt
, size_t i
, size_t j
) {
707 const DatatypeConstructor
& ctor
= dt
[j
];
708 Debug("parser-sygus") << "Sygus : process constructor " << j
<< " : " << dt
[j
] << std::endl
;
709 std::vector
<Expr
> bvs
, extraArgs
;
710 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
711 std::string vname
= "v_" + ctor
[k
].getName();
712 Expr bv
= getExprManager()->mkBoundVar(vname
, SelectorType(ctor
[k
].getType()).getRangeType());
714 extraArgs
.push_back(bv
);
716 if( !terms
[0].isNull() ){
717 bvs
.insert(bvs
.end(), terms
[0].begin(), terms
[0].end());
721 bvl
= getExprManager()->mkExpr(kind::BOUND_VAR_LIST
, bvs
);
723 Debug("parser-sygus") << "...made bv list " << bvl
<< std::endl
;
724 std::vector
<Expr
> patv
;
725 patv
.push_back(eval
);
726 std::vector
<Expr
> applyv
;
727 applyv
.push_back(ctor
.getConstructor());
728 applyv
.insert(applyv
.end(), extraArgs
.begin(), extraArgs
.end());
729 for(size_t k
= 0; k
< applyv
.size(); ++k
) {
731 Expr cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
732 Debug("parser-sygus") << "...made eval ctor apply " << cpatv
<< std::endl
;
733 patv
.push_back(cpatv
);
734 if( !terms
[0].isNull() ){
735 patv
.insert(patv
.end(), terms
[0].begin(), terms
[0].end());
737 Expr evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
738 Debug("parser-sygus") << "...made eval apply " << evalApply
<< std::endl
;
739 std::vector
<Expr
> builtApply
;
740 for(size_t k
= 0; k
< extraArgs
.size(); ++k
) {
741 std::vector
<Expr
> patvb
;
742 patvb
.push_back(evals
[DatatypeType(extraArgs
[k
].getType())]);
743 patvb
.push_back(extraArgs
[k
]);
744 if( !terms
[0].isNull() ){
745 patvb
.insert(patvb
.end(), terms
[0].begin(), terms
[0].end());
747 builtApply
.push_back(getExprManager()->mkExpr(kind::APPLY_UF
, patvb
));
749 for(size_t k
= 0; k
< builtApply
.size(); ++k
) {
752 //if( ops[i][j].getKind() == kind::BUILTIN ){
753 if( !builtApply
.empty() ){
754 if( ops
[i
][j
].getKind() != kind::BUILTIN
){
755 builtTerm
= getExprManager()->mkExpr(kind::APPLY
, ops
[i
][j
], builtApply
);
757 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
760 builtTerm
= ops
[i
][j
];
762 Debug("parser-sygus") << "...made built term " << builtTerm
<< std::endl
;
763 Expr assertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
765 Expr pattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
766 pattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, pattern
);
767 assertion
= getExprManager()->mkExpr(kind::FORALL
, bvl
, assertion
, pattern
);
769 Debug("parser-sygus") << "...made assertion " << assertion
<< std::endl
;
771 //linearize multiplication if possible
772 if( builtTerm
.getKind()==kind::MULT
){
773 for(size_t k
= 0; k
< ctor
.getNumArgs(); ++k
) {
774 Type at
= SelectorType(ctor
[k
].getType()).getRangeType();
775 if( at
.isDatatype() ){
776 DatatypeType atd
= (DatatypeType
)SelectorType(ctor
[k
].getType()).getRangeType();
777 Debug("parser-sygus") << "Argument " << k
<< " " << atd
<< std::endl
;
778 std::vector
<DatatypeType
>::iterator itd
= std::find( datatypeTypes
.begin(), datatypeTypes
.end(), atd
);
779 if( itd
!=datatypeTypes
.end() ){
780 Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl
;
781 unsigned index
= itd
-datatypeTypes
.begin();
782 Debug("parser-sygus2") << "index = " << index
<< std::endl
;
784 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
785 Debug("parser-sygus2") << "ops[" << cc
<< "]=" << ops
[index
][cc
] << std::endl
;
786 if( ops
[index
][cc
].getKind() != kind::CONST_RATIONAL
){
792 Debug("parser-sygus") << "Linearize multiplication " << ctor
<< " based on argument " << k
<< std::endl
;
793 const Datatype
& atdd
= atd
.getDatatype();
794 std::vector
<Expr
> assertions
;
795 std::vector
<Expr
> nbvs
;
796 for( unsigned a
=0; a
<bvl
.getNumChildren(); a
++ ){
798 nbvs
.push_back( bvl
[a
] );
801 Expr nbvl
= getExprManager()->mkExpr( kind::BOUND_VAR_LIST
, nbvs
);
802 for( unsigned cc
= 0; cc
< ops
[index
].size(); cc
++ ){
803 //Make new assertion based on partially instantiating existing
804 applyv
[k
+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, atdd
[cc
].getConstructor());
805 Debug("parser-sygus") << "applyv " << applyv
[k
+1] << std::endl
;
806 cpatv
= getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR
, applyv
);
807 Debug("parser-sygus") << "cpatv " << cpatv
<< std::endl
;
809 evalApply
= getExprManager()->mkExpr(kind::APPLY_UF
, patv
);
810 Debug("parser-sygus") << "evalApply " << evalApply
<< std::endl
;
811 builtApply
[k
] = ops
[index
][cc
];
812 Debug("parser-sygus") << "builtApply " << builtApply
[k
] << std::endl
;
813 builtTerm
= getExprManager()->mkExpr(ops
[i
][j
], builtApply
);
814 Debug("parser-sygus") << "builtTerm " << builtTerm
<< std::endl
;
815 Expr eassertion
= getExprManager()->mkExpr(evalApply
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, evalApply
, builtTerm
);
816 Expr epattern
= getExprManager()->mkExpr(kind::INST_PATTERN
, evalApply
);
817 epattern
= getExprManager()->mkExpr(kind::INST_PATTERN_LIST
, epattern
);
818 eassertion
= getExprManager()->mkExpr(kind::FORALL
, nbvl
, eassertion
, epattern
);
819 assertions
.push_back( eassertion
);
821 assertion
= assertions
.size()==1 ? assertions
[0] : getExprManager()->mkExpr( kind::AND
, assertions
);
822 Debug("parser-sygus") << "...(linearized) assertion is: " << assertion
<< std::endl
;
832 }/* CVC4::parser namespace */
833 }/* CVC4 namespace */