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"
118 Node
Evaluator::eval(TNode n
,
119 const std::vector
<Node
>& args
,
120 const std::vector
<Node
>& vals
)
122 Trace("evaluator") << "Evaluating " << n
<< " under substitution " << args
123 << " " << vals
<< std::endl
;
124 return evalInternal(n
, args
, vals
).toNode();
127 EvalResult
Evaluator::evalInternal(TNode n
,
128 const std::vector
<Node
>& args
,
129 const std::vector
<Node
>& vals
)
131 std::unordered_map
<TNode
, EvalResult
, TNodeHashFunction
> results
;
132 std::vector
<TNode
> queue
;
133 queue
.emplace_back(n
);
135 while (queue
.size() != 0)
137 TNode currNode
= queue
.back();
139 if (results
.find(currNode
) != results
.end())
146 for (const auto& currNodeChild
: currNode
)
148 if (results
.find(currNodeChild
) == results
.end())
150 queue
.emplace_back(currNodeChild
);
159 Node currNodeVal
= currNode
;
160 if (currNode
.isVar())
162 const auto& it
= std::find(args
.begin(), args
.end(), currNode
);
164 if (it
== args
.end())
169 ptrdiff_t pos
= std::distance(args
.begin(), it
);
170 currNodeVal
= vals
[pos
];
172 else if (currNode
.getKind() == kind::APPLY_UF
173 && currNode
.getOperator().getKind() == kind::LAMBDA
)
175 // Create a copy of the current substitutions
176 std::vector
<Node
> lambdaArgs(args
);
177 std::vector
<Node
> lambdaVals(vals
);
179 // Add the values for the arguments of the lambda as substitutions at
180 // the beginning of the vector to shadow variables from outer scopes
181 // with the same name
182 Node op
= currNode
.getOperator();
183 for (const auto& lambdaArg
: op
[0])
185 lambdaArgs
.insert(lambdaArgs
.begin(), lambdaArg
);
188 for (const auto& lambdaVal
: currNode
)
190 lambdaVals
.insert(lambdaVals
.begin(), results
[lambdaVal
].toNode());
193 // Lambdas are evaluated in a recursive fashion because each evaluation
194 // requires different substitutions
195 results
[currNode
] = evalInternal(op
[1], lambdaArgs
, lambdaVals
);
196 if (results
[currNode
].d_tag
== EvalResult::INVALID
)
198 // evaluation was invalid, we fail
199 return results
[currNode
];
204 switch (currNodeVal
.getKind())
206 case kind::CONST_BOOLEAN
:
207 results
[currNode
] = EvalResult(currNodeVal
.getConst
<bool>());
212 results
[currNode
] = EvalResult(!(results
[currNode
[0]].d_bool
));
218 bool res
= results
[currNode
[0]].d_bool
;
219 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
221 res
= res
&& results
[currNode
[i
]].d_bool
;
223 results
[currNode
] = EvalResult(res
);
229 bool res
= results
[currNode
[0]].d_bool
;
230 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
232 res
= res
|| results
[currNode
[i
]].d_bool
;
234 results
[currNode
] = EvalResult(res
);
238 case kind::CONST_RATIONAL
:
240 const Rational
& r
= currNodeVal
.getConst
<Rational
>();
241 results
[currNode
] = EvalResult(r
);
247 Rational res
= results
[currNode
[0]].d_rat
;
248 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
250 res
= res
+ results
[currNode
[i
]].d_rat
;
252 results
[currNode
] = EvalResult(res
);
258 const Rational
& x
= results
[currNode
[0]].d_rat
;
259 const Rational
& y
= results
[currNode
[1]].d_rat
;
260 results
[currNode
] = EvalResult(x
- y
);
266 Rational res
= results
[currNode
[0]].d_rat
;
267 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
269 res
= res
* results
[currNode
[i
]].d_rat
;
271 results
[currNode
] = EvalResult(res
);
277 const Rational
& x
= results
[currNode
[0]].d_rat
;
278 const Rational
& y
= results
[currNode
[1]].d_rat
;
279 results
[currNode
] = EvalResult(x
>= y
);
283 case kind::CONST_STRING
:
284 results
[currNode
] = EvalResult(currNodeVal
.getConst
<String
>());
287 case kind::STRING_CONCAT
:
289 String res
= results
[currNode
[0]].d_str
;
290 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
292 res
= res
.concat(results
[currNode
[i
]].d_str
);
294 results
[currNode
] = EvalResult(res
);
298 case kind::STRING_LENGTH
:
300 const String
& s
= results
[currNode
[0]].d_str
;
301 results
[currNode
] = EvalResult(Rational(s
.size()));
305 case kind::STRING_SUBSTR
:
307 const String
& s
= results
[currNode
[0]].d_str
;
308 Integer
s_len(s
.size());
309 Integer i
= results
[currNode
[1]].d_rat
.getNumerator();
310 Integer j
= results
[currNode
[2]].d_rat
.getNumerator();
312 if (i
.strictlyNegative() || j
.strictlyNegative() || i
>= s_len
)
314 results
[currNode
] = EvalResult(String(""));
316 else if (i
+ j
> s_len
)
319 EvalResult(s
.suffix((s_len
- i
).toUnsignedInt()));
324 EvalResult(s
.substr(i
.toUnsignedInt(), j
.toUnsignedInt()));
329 case kind::STRING_CHARAT
:
331 const String
& s
= results
[currNode
[0]].d_str
;
332 Integer
s_len(s
.size());
333 Integer i
= results
[currNode
[1]].d_rat
.getNumerator();
334 if (i
.strictlyNegative() || i
>= s_len
)
336 results
[currNode
] = EvalResult(String(""));
340 results
[currNode
] = EvalResult(s
.substr(i
.toUnsignedInt(), 1));
345 case kind::STRING_STRCTN
:
347 const String
& s
= results
[currNode
[0]].d_str
;
348 const String
& t
= results
[currNode
[1]].d_str
;
349 results
[currNode
] = EvalResult(s
.find(t
) != std::string::npos
);
353 case kind::STRING_STRIDOF
:
355 const String
& s
= results
[currNode
[0]].d_str
;
356 Integer
s_len(s
.size());
357 const String
& x
= results
[currNode
[1]].d_str
;
358 Integer i
= results
[currNode
[2]].d_rat
.getNumerator();
360 if (i
.strictlyNegative() || i
>= s_len
)
362 results
[currNode
] = EvalResult(Rational(-1));
366 size_t r
= s
.find(x
, i
.toUnsignedInt());
367 if (r
== std::string::npos
)
369 results
[currNode
] = EvalResult(Rational(-1));
373 results
[currNode
] = EvalResult(Rational(r
));
379 case kind::STRING_STRREPL
:
381 const String
& s
= results
[currNode
[0]].d_str
;
382 const String
& x
= results
[currNode
[1]].d_str
;
383 const String
& y
= results
[currNode
[2]].d_str
;
384 results
[currNode
] = EvalResult(s
.replace(x
, y
));
388 case kind::STRING_PREFIX
:
390 const String
& t
= results
[currNode
[0]].d_str
;
391 const String
& s
= results
[currNode
[1]].d_str
;
392 if (s
.size() < t
.size())
394 results
[currNode
] = EvalResult(false);
398 results
[currNode
] = EvalResult(s
.prefix(t
.size()) == t
);
403 case kind::STRING_SUFFIX
:
405 const String
& t
= results
[currNode
[0]].d_str
;
406 const String
& s
= results
[currNode
[1]].d_str
;
407 if (s
.size() < t
.size())
409 results
[currNode
] = EvalResult(false);
413 results
[currNode
] = EvalResult(s
.suffix(t
.size()) == t
);
418 case kind::STRING_ITOS
:
420 Integer i
= results
[currNode
[0]].d_rat
.getNumerator();
421 if (i
.strictlyNegative())
423 results
[currNode
] = EvalResult(String(""));
427 results
[currNode
] = EvalResult(String(i
.toString()));
432 case kind::STRING_STOI
:
434 const String
& s
= results
[currNode
[0]].d_str
;
437 results
[currNode
] = EvalResult(Rational(-1));
441 results
[currNode
] = EvalResult(Rational(s
.toNumber()));
446 case kind::CONST_BITVECTOR
:
447 results
[currNode
] = EvalResult(currNodeVal
.getConst
<BitVector
>());
450 case kind::BITVECTOR_NOT
:
451 results
[currNode
] = EvalResult(~results
[currNode
[0]].d_bv
);
454 case kind::BITVECTOR_NEG
:
455 results
[currNode
] = EvalResult(-results
[currNode
[0]].d_bv
);
458 case kind::BITVECTOR_EXTRACT
:
460 unsigned lo
= bv::utils::getExtractLow(currNodeVal
);
461 unsigned hi
= bv::utils::getExtractHigh(currNodeVal
);
463 EvalResult(results
[currNode
[0]].d_bv
.extract(hi
, lo
));
467 case kind::BITVECTOR_CONCAT
:
469 BitVector res
= results
[currNode
[0]].d_bv
;
470 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
472 res
= res
.concat(results
[currNode
[i
]].d_bv
);
474 results
[currNode
] = EvalResult(res
);
478 case kind::BITVECTOR_PLUS
:
480 BitVector res
= results
[currNode
[0]].d_bv
;
481 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
483 res
= res
+ results
[currNode
[i
]].d_bv
;
485 results
[currNode
] = EvalResult(res
);
489 case kind::BITVECTOR_MULT
:
491 BitVector res
= results
[currNode
[0]].d_bv
;
492 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
494 res
= res
* results
[currNode
[i
]].d_bv
;
496 results
[currNode
] = EvalResult(res
);
499 case kind::BITVECTOR_AND
:
501 BitVector res
= results
[currNode
[0]].d_bv
;
502 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
504 res
= res
& results
[currNode
[i
]].d_bv
;
506 results
[currNode
] = EvalResult(res
);
510 case kind::BITVECTOR_OR
:
512 BitVector res
= results
[currNode
[0]].d_bv
;
513 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
515 res
= res
| results
[currNode
[i
]].d_bv
;
517 results
[currNode
] = EvalResult(res
);
521 case kind::BITVECTOR_XOR
:
523 BitVector res
= results
[currNode
[0]].d_bv
;
524 for (size_t i
= 1, end
= currNode
.getNumChildren(); i
< end
; i
++)
526 res
= res
^ results
[currNode
[i
]].d_bv
;
528 results
[currNode
] = EvalResult(res
);
534 EvalResult lhs
= results
[currNode
[0]];
535 EvalResult rhs
= results
[currNode
[1]];
539 case EvalResult::BOOL
:
541 results
[currNode
] = EvalResult(lhs
.d_bool
== rhs
.d_bool
);
545 case EvalResult::BITVECTOR
:
547 results
[currNode
] = EvalResult(lhs
.d_bv
== rhs
.d_bv
);
551 case EvalResult::RATIONAL
:
553 results
[currNode
] = EvalResult(lhs
.d_rat
== rhs
.d_rat
);
557 case EvalResult::STRING
:
559 results
[currNode
] = EvalResult(lhs
.d_str
== rhs
.d_str
);
565 Trace("evaluator") << "Theory " << Theory::theoryOf(currNode
[0])
566 << " not supported" << std::endl
;
577 if (results
[currNode
[0]].d_bool
)
579 results
[currNode
] = results
[currNode
[1]];
583 results
[currNode
] = results
[currNode
[2]];
590 Trace("evaluator") << "Kind " << currNodeVal
.getKind()
591 << " not supported" << std::endl
;
601 } // namespace theory