0a0176f25b5a28a1b8281b709206d02766783a07
1 /********************* */
2 /*! \file evaluator.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The Evaluator class
14 ** The Evaluator class.
17 #include "theory/evaluator.h"
19 #include "theory/bv/theory_bv_utils.h"
20 #include "theory/theory.h"
21 #include "util/integer.h"
26 EvalResult::EvalResult(const EvalResult
& other
)
31 case BOOL
: d_bool
= other
.d_bool
; break;
33 new (&d_bv
) BitVector
;
37 new (&d_rat
) Rational
;
48 EvalResult
& EvalResult::operator=(const EvalResult
& other
)
55 case BOOL
: d_bool
= other
.d_bool
; break;
57 new (&d_bv
) BitVector
;
61 new (&d_rat
) Rational
;
74 EvalResult::~EvalResult()
98 Node
EvalResult::toNode() const
100 NodeManager
* nm
= NodeManager::currentNM();
103 case EvalResult::BOOL
: return nm
->mkConst(d_bool
);
104 case EvalResult::BITVECTOR
: return nm
->mkConst(d_bv
);
105 case EvalResult::RATIONAL
: return nm
->mkConst(d_rat
);
106 case EvalResult::STRING
: return nm
->mkConst(d_str
);
109 Trace("evaluator") << "Missing conversion from " << d_tag
<< " to node"
116 Node
Evaluator::eval(TNode n
,
117 const std::vector
<Node
>& args
,
118 const std::vector
<Node
>& vals
)
120 Trace("evaluator") << "Evaluating " << n
<< " under substitution " << args
121 << " " << vals
<< std::endl
;
122 return evalInternal(n
, args
, vals
).toNode();
125 EvalResult
Evaluator::evalInternal(TNode n
,
126 const std::vector
<Node
>& args
,
127 const std::vector
<Node
>& vals
)
129 std::unordered_map
<TNode
, EvalResult
, TNodeHashFunction
> results
;
130 std::vector
<TNode
> queue
;
131 queue
.emplace_back(n
);
133 while (queue
.size() != 0)
135 TNode currNode
= queue
.back();
137 if (results
.find(currNode
) != results
.end())
144 for (const auto& currNodeChild
: currNode
)
146 if (results
.find(currNodeChild
) == results
.end())
148 queue
.emplace_back(currNodeChild
);
157 Node currNodeVal
= currNode
;
158 if (currNode
.isVar())
160 const auto& it
= std::find(args
.begin(), args
.end(), currNode
);
162 if (it
== args
.end())
167 ptrdiff_t pos
= std::distance(args
.begin(), it
);
168 currNodeVal
= vals
[pos
];
170 else if (currNode
.getKind() == kind::APPLY_UF
171 && currNode
.getOperator().getKind() == kind::LAMBDA
)
173 // Create a copy of the current substitutions
174 std::vector
<Node
> lambdaArgs(args
);
175 std::vector
<Node
> lambdaVals(vals
);
177 // Add the values for the arguments of the lambda as substitutions at
178 // the beginning of the vector to shadow variables from outer scopes
179 // with the same name
180 Node op
= currNode
.getOperator();
181 for (const auto& lambdaArg
: op
[0])
183 lambdaArgs
.insert(lambdaArgs
.begin(), lambdaArg
);
186 for (const auto& lambdaVal
: currNode
)
188 lambdaVals
.insert(lambdaVals
.begin(), results
[lambdaVal
].toNode());
191 // Lambdas are evaluated in a recursive fashion because each evaluation
192 // requires different substitutions
193 results
[currNode
] = evalInternal(op
[1], lambdaArgs
, lambdaVals
);
194 if (results
[currNode
].d_tag
== EvalResult::INVALID
)
196 // evaluation was invalid, we fail
197 return results
[currNode
];
202 switch (currNodeVal
.getKind())
204 case kind::CONST_BOOLEAN
:
205 results
[currNode
] = EvalResult(currNodeVal
.getConst
<bool>());
210 results
[currNode
] = EvalResult(!(results
[currNode
[0]].d_bool
));
216 bool res
= results
[currNode
[0]].d_bool
;
217 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
219 res
= res
&& results
[currNode
[i
]].d_bool
;
221 results
[currNode
] = EvalResult(res
);
227 bool res
= results
[currNode
[0]].d_bool
;
228 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
230 res
= res
|| results
[currNode
[i
]].d_bool
;
232 results
[currNode
] = EvalResult(res
);
236 case kind::CONST_RATIONAL
:
238 const Rational
& r
= currNodeVal
.getConst
<Rational
>();
239 results
[currNode
] = EvalResult(r
);
245 Rational res
= results
[currNode
[0]].d_rat
;
246 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
248 res
= res
+ results
[currNode
[i
]].d_rat
;
250 results
[currNode
] = EvalResult(res
);
256 const Rational
& x
= results
[currNode
[0]].d_rat
;
257 const Rational
& y
= results
[currNode
[1]].d_rat
;
258 results
[currNode
] = EvalResult(x
- y
);
264 Rational res
= results
[currNode
[0]].d_rat
;
265 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
267 res
= res
* results
[currNode
[i
]].d_rat
;
269 results
[currNode
] = EvalResult(res
);
275 const Rational
& x
= results
[currNode
[0]].d_rat
;
276 const Rational
& y
= results
[currNode
[1]].d_rat
;
277 results
[currNode
] = EvalResult(x
>= y
);
281 case kind::CONST_STRING
:
282 results
[currNode
] = EvalResult(currNodeVal
.getConst
<String
>());
285 case kind::STRING_CONCAT
:
287 String res
= results
[currNode
[0]].d_str
;
288 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
290 res
= res
.concat(results
[currNode
[i
]].d_str
);
292 results
[currNode
] = EvalResult(res
);
296 case kind::STRING_LENGTH
:
298 const String
& s
= results
[currNode
[0]].d_str
;
299 results
[currNode
] = EvalResult(Rational(s
.size()));
303 case kind::STRING_SUBSTR
:
305 const String
& s
= results
[currNode
[0]].d_str
;
306 Integer
s_len(s
.size());
307 Integer i
= results
[currNode
[1]].d_rat
.getNumerator();
308 Integer j
= results
[currNode
[2]].d_rat
.getNumerator();
310 if (i
.strictlyNegative() || j
.strictlyNegative() || i
>= s_len
)
312 results
[currNode
] = EvalResult(String(""));
314 else if (i
+ j
> s_len
)
317 EvalResult(s
.suffix((s_len
- i
).toUnsignedInt()));
322 EvalResult(s
.substr(i
.toUnsignedInt(), j
.toUnsignedInt()));
327 case kind::STRING_CHARAT
:
329 const String
& s
= results
[currNode
[0]].d_str
;
330 Integer
s_len(s
.size());
331 Integer i
= results
[currNode
[1]].d_rat
.getNumerator();
332 if (i
.strictlyNegative() || i
>= s_len
)
334 results
[currNode
] = EvalResult(String(""));
338 results
[currNode
] = EvalResult(s
.substr(i
.toUnsignedInt(), 1));
343 case kind::STRING_STRCTN
:
345 const String
& s
= results
[currNode
[0]].d_str
;
346 const String
& t
= results
[currNode
[1]].d_str
;
347 results
[currNode
] = EvalResult(s
.find(t
) != std::string::npos
);
351 case kind::STRING_STRIDOF
:
353 const String
& s
= results
[currNode
[0]].d_str
;
354 Integer
s_len(s
.size());
355 const String
& x
= results
[currNode
[1]].d_str
;
356 Integer i
= results
[currNode
[2]].d_rat
.getNumerator();
358 if (i
.strictlyNegative())
360 results
[currNode
] = EvalResult(Rational(-1));
364 size_t r
= s
.find(x
, i
.toUnsignedInt());
365 if (r
== std::string::npos
)
367 results
[currNode
] = EvalResult(Rational(-1));
371 results
[currNode
] = EvalResult(Rational(r
));
377 case kind::STRING_STRREPL
:
379 const String
& s
= results
[currNode
[0]].d_str
;
380 const String
& x
= results
[currNode
[1]].d_str
;
381 const String
& y
= results
[currNode
[2]].d_str
;
382 results
[currNode
] = EvalResult(s
.replace(x
, y
));
386 case kind::STRING_PREFIX
:
388 const String
& t
= results
[currNode
[0]].d_str
;
389 const String
& s
= results
[currNode
[1]].d_str
;
390 if (s
.size() < t
.size())
392 results
[currNode
] = EvalResult(false);
396 results
[currNode
] = EvalResult(s
.prefix(t
.size()) == t
);
401 case kind::STRING_SUFFIX
:
403 const String
& t
= results
[currNode
[0]].d_str
;
404 const String
& s
= results
[currNode
[1]].d_str
;
405 if (s
.size() < t
.size())
407 results
[currNode
] = EvalResult(false);
411 results
[currNode
] = EvalResult(s
.suffix(t
.size()) == t
);
416 case kind::STRING_ITOS
:
418 Integer i
= results
[currNode
[0]].d_rat
.getNumerator();
419 if (i
.strictlyNegative())
421 results
[currNode
] = EvalResult(String(""));
425 results
[currNode
] = EvalResult(String(i
.toString()));
430 case kind::STRING_STOI
:
432 const String
& s
= results
[currNode
[0]].d_str
;
435 results
[currNode
] = EvalResult(Rational(s
.toNumber()));
439 results
[currNode
] = EvalResult(Rational(-1));
444 case kind::STRING_CODE
:
446 const String
& s
= results
[currNode
[0]].d_str
;
449 results
[currNode
] = EvalResult(
450 Rational(String::convertUnsignedIntToCode(s
.getVec()[0])));
454 results
[currNode
] = EvalResult(Rational(-1));
459 case kind::CONST_BITVECTOR
:
460 results
[currNode
] = EvalResult(currNodeVal
.getConst
<BitVector
>());
463 case kind::BITVECTOR_NOT
:
464 results
[currNode
] = EvalResult(~results
[currNode
[0]].d_bv
);
467 case kind::BITVECTOR_NEG
:
468 results
[currNode
] = EvalResult(-results
[currNode
[0]].d_bv
);
471 case kind::BITVECTOR_EXTRACT
:
473 unsigned lo
= bv::utils::getExtractLow(currNodeVal
);
474 unsigned hi
= bv::utils::getExtractHigh(currNodeVal
);
476 EvalResult(results
[currNode
[0]].d_bv
.extract(hi
, lo
));
480 case kind::BITVECTOR_CONCAT
:
482 BitVector res
= results
[currNode
[0]].d_bv
;
483 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
485 res
= res
.concat(results
[currNode
[i
]].d_bv
);
487 results
[currNode
] = EvalResult(res
);
491 case kind::BITVECTOR_PLUS
:
493 BitVector res
= results
[currNode
[0]].d_bv
;
494 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
496 res
= res
+ results
[currNode
[i
]].d_bv
;
498 results
[currNode
] = EvalResult(res
);
502 case kind::BITVECTOR_MULT
:
504 BitVector res
= results
[currNode
[0]].d_bv
;
505 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
507 res
= res
* results
[currNode
[i
]].d_bv
;
509 results
[currNode
] = EvalResult(res
);
512 case kind::BITVECTOR_AND
:
514 BitVector res
= results
[currNode
[0]].d_bv
;
515 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
517 res
= res
& results
[currNode
[i
]].d_bv
;
519 results
[currNode
] = EvalResult(res
);
523 case kind::BITVECTOR_OR
:
525 BitVector res
= results
[currNode
[0]].d_bv
;
526 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
528 res
= res
| results
[currNode
[i
]].d_bv
;
530 results
[currNode
] = EvalResult(res
);
534 case kind::BITVECTOR_XOR
:
536 BitVector res
= results
[currNode
[0]].d_bv
;
537 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
539 res
= res
^ results
[currNode
[i
]].d_bv
;
541 results
[currNode
] = EvalResult(res
);
547 EvalResult lhs
= results
[currNode
[0]];
548 EvalResult rhs
= results
[currNode
[1]];
552 case EvalResult::BOOL
:
554 results
[currNode
] = EvalResult(lhs
.d_bool
== rhs
.d_bool
);
558 case EvalResult::BITVECTOR
:
560 results
[currNode
] = EvalResult(lhs
.d_bv
== rhs
.d_bv
);
564 case EvalResult::RATIONAL
:
566 results
[currNode
] = EvalResult(lhs
.d_rat
== rhs
.d_rat
);
570 case EvalResult::STRING
:
572 results
[currNode
] = EvalResult(lhs
.d_str
== rhs
.d_str
);
578 Trace("evaluator") << "Theory " << Theory::theoryOf(currNode
[0])
579 << " not supported" << std::endl
;
590 if (results
[currNode
[0]].d_bool
)
592 results
[currNode
] = results
[currNode
[1]];
596 results
[currNode
] = results
[currNode
[2]];
603 Trace("evaluator") << "Kind " << currNodeVal
.getKind()
604 << " not supported" << std::endl
;
614 } // namespace theory