4285a65cf209aaa83b615a869e679d6657df0904
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() || i
>= s_len
)
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::CONST_BITVECTOR
:
445 results
[currNode
] = EvalResult(currNodeVal
.getConst
<BitVector
>());
448 case kind::BITVECTOR_NOT
:
449 results
[currNode
] = EvalResult(~results
[currNode
[0]].d_bv
);
452 case kind::BITVECTOR_NEG
:
453 results
[currNode
] = EvalResult(-results
[currNode
[0]].d_bv
);
456 case kind::BITVECTOR_EXTRACT
:
458 unsigned lo
= bv::utils::getExtractLow(currNodeVal
);
459 unsigned hi
= bv::utils::getExtractHigh(currNodeVal
);
461 EvalResult(results
[currNode
[0]].d_bv
.extract(hi
, lo
));
465 case kind::BITVECTOR_CONCAT
:
467 BitVector res
= results
[currNode
[0]].d_bv
;
468 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
470 res
= res
.concat(results
[currNode
[i
]].d_bv
);
472 results
[currNode
] = EvalResult(res
);
476 case kind::BITVECTOR_PLUS
:
478 BitVector res
= results
[currNode
[0]].d_bv
;
479 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
481 res
= res
+ results
[currNode
[i
]].d_bv
;
483 results
[currNode
] = EvalResult(res
);
487 case kind::BITVECTOR_MULT
:
489 BitVector res
= results
[currNode
[0]].d_bv
;
490 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
492 res
= res
* results
[currNode
[i
]].d_bv
;
494 results
[currNode
] = EvalResult(res
);
497 case kind::BITVECTOR_AND
:
499 BitVector res
= results
[currNode
[0]].d_bv
;
500 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
502 res
= res
& results
[currNode
[i
]].d_bv
;
504 results
[currNode
] = EvalResult(res
);
508 case kind::BITVECTOR_OR
:
510 BitVector res
= results
[currNode
[0]].d_bv
;
511 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
513 res
= res
| results
[currNode
[i
]].d_bv
;
515 results
[currNode
] = EvalResult(res
);
519 case kind::BITVECTOR_XOR
:
521 BitVector res
= results
[currNode
[0]].d_bv
;
522 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
524 res
= res
^ results
[currNode
[i
]].d_bv
;
526 results
[currNode
] = EvalResult(res
);
532 EvalResult lhs
= results
[currNode
[0]];
533 EvalResult rhs
= results
[currNode
[1]];
537 case EvalResult::BOOL
:
539 results
[currNode
] = EvalResult(lhs
.d_bool
== rhs
.d_bool
);
543 case EvalResult::BITVECTOR
:
545 results
[currNode
] = EvalResult(lhs
.d_bv
== rhs
.d_bv
);
549 case EvalResult::RATIONAL
:
551 results
[currNode
] = EvalResult(lhs
.d_rat
== rhs
.d_rat
);
555 case EvalResult::STRING
:
557 results
[currNode
] = EvalResult(lhs
.d_str
== rhs
.d_str
);
563 Trace("evaluator") << "Theory " << Theory::theoryOf(currNode
[0])
564 << " not supported" << std::endl
;
575 if (results
[currNode
[0]].d_bool
)
577 results
[currNode
] = results
[currNode
[1]];
581 results
[currNode
] = results
[currNode
[2]];
588 Trace("evaluator") << "Kind " << currNodeVal
.getKind()
589 << " not supported" << std::endl
;
599 } // namespace theory