diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-24 23:50:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-24 23:50:50 -0500 |
| commit | e9c115e82ea1341f1bbc37fb99c005aacec3d7ec (patch) | |
| tree | d274291c8b570e1ff383504e8eeccaafbffd7b15 /src/theory/quantifiers/sygus/cegis_unif.cpp | |
| parent | b9cddd75ada97b4e1808b907125e366c3c03c412 (diff) | |
Allow partial models for multiple sygus enumerators (#2499)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 456f44019..d4926311d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -166,6 +166,13 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, ->toStreamSygus(ss, m_eu); Trace("cegis") << ss.str() << std::endl; } + if (m_eu.isNull()) + { + // A condition enumerator was excluded by symmetry breaking, fail. + // TODO (#2498): either move conditions to getTermList or handle + // partial models in this module. + return false; + } unif_values[index][e].push_back(m_eu); } // inter-enumerator symmetry breaking for return values |