diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_explain.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index b1baed9cb..cf1993efb 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -189,8 +189,13 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, TypeNode ntn = n.getType(); if (!ntn.isDatatype()) { - // sygus datatype fields that are not sygus datatypes are treated as - // abstractions only, hence we disregard this field + // SyGuS datatype fields that are not sygus datatypes are treated as + // abstractions only, hence we disregard this field. It is important + // that users of this method pay special attention to any constants, + // otherwise the explanation n.eqNode(vn) is necessary here. For example, + // any lemma schema that blocks the current value of an enumerator should + // not make any assumptions about the value of the arguments of its any + // constant constructors, since their explanation is not included here. return; } Assert(vn.getKind() == APPLY_CONSTRUCTOR); |