diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 12:45:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-02 12:45:48 -0500 |
| commit | f47f7288145e0ae5b40271e105e0f5ec52091a5f (patch) | |
| tree | fb6bcfd2f391f7f27b9f7be34b01f07ca8ef400d /src/theory/quantifiers/cegqi | |
| parent | 02fc64067f5a0e0d1adb5d778562728cace0bdb5 (diff) | |
Modify cegqi heuristic for finite datatypes (#2126)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index af003ce39..4c843606b 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -73,7 +73,7 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status) case CEG_UNHANDLED: os << "unhandled"; break; case CEG_PARTIALLY_HANDLED: os << "partially_handled"; break; case CEG_HANDLED: os << "handled"; break; - case CEG_HANDLED_UNCONDITIONAL: os << "unhandled_unc"; break; + case CEG_HANDLED_UNCONDITIONAL: os << "handled_unc"; break; default: Unreachable(); } return os; @@ -235,9 +235,9 @@ CegHandledStatus CegInstantiator::isCbqiSort( { // recursive calls to this datatype are handlable visited[tn] = CEG_HANDLED; - // if not recursive, it is finite and we can handle it regardless of body - // hence, we initialize ret to CEG_HANDLED_UNCONDITIONAL. - ret = CEG_HANDLED_UNCONDITIONAL; + // we initialize to handled, we remain handled as long as all subfields + // of this datatype are not unhandled. + ret = CEG_HANDLED; const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { |