diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-04 15:52:28 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-04 15:52:28 -0600 |
| commit | 4125891ca0228501775282f6cf15028ab46d24ca (patch) | |
| tree | 431ab1a330be06f66b097c660c8eed1b42773ecc /src/theory/evaluator.h | |
| parent | 42d1c64f7d7af06d988bf4f6bf3f20836c78a8eb (diff) | |
Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492)
Diffstat (limited to 'src/theory/evaluator.h')
| -rw-r--r-- | src/theory/evaluator.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 5c0e9b944..ce19a1f67 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -88,6 +88,9 @@ class Evaluator * `args` and the corresponding values `vals`. The function returns a null * node if there is a subterm that is not constant under the substitution or * if an operator is not supported by the evaluator. + * + * The nodes in the vals must be constant values, that is, they must return + * true for isConst(). */ Node eval(TNode n, const std::vector<Node>& args, |